Implementing "Internal" Languages One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured category.

For instance, Synthetic Differential Geometry has models in topoi that contain and embedding of the category of smooth manifolds, so you can use higher-order logic to construct smooth functions and solve differential equations.

As another example, in this paper, they notice that "step-indexing" is really just working with presheaves over the naturals (another topos), so you can use the syntax of higher order logic to define step-indexed logical relations without the tedious manipulation of steps.

Finally, Andrej Bauer shows in this MO question that you can do a lot with the "internal language" of the topos of graphs.

My question is, has anyone realized this vision literally in a theorem prover?
For instance, if I show that a category I care about is Cartesian Closed, I could then move to "internal mode" where I write lambda-calculus syntax (with some model-specific axioms) and then can move back to "external mode" and manipulate them as objects in my model?

In the extreme I would even want topos theory and higher-order logic, so I could write my step-indexed logical relations without steps, or teach classical mechanics with a theorem prover using SDG. This seems to me to be a very powerful idea as someone could implement extensional dependent type theory once and provide nice tooling and then use it with wildly different applications as described above.
In Extending Type Theory with Forcing by  Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, implemented as a type-preserving translation in the style of Bernardy and Lasson's parametricity translation.

This means that you can define terms in your usual type theory, and then "translate them" into a "forcing layer" where they are interpreted as translations at a different translation type. For example, the translation induced by indexing over decreasing natural numbers lets you use your usual terms in a post-translation theory where a later modality is definable. This sounds rather close to your idea of working internally in the topos of trees.

It seems that they have a new, simpler Coq plugin implementing these ideas at CoqHott/coq-forcing, and in particular SI.v builds this forcing translation for step-indexing. Unfortunately, while it does the work of building the model, there is no example of using it for step-indexed definitions in practice (the only thing translated instead of defined in the forcing layer is Forcing Translate eq, which isn't terribly informative). You could try to experiment to see how (in)convenient this is to use.