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.