To cite nlab:
The Mitchell–Bénabou language, like the internal logic of any category, is a powerful way to describe various objects in a topos as if they were sets. It can be viewed as making the topos into a generalized set theory or a type theory, so that we can write and prove statements in a topos, and properties of a topos, using first order intuitionistic predicate logic.
I am interested in examples of (references to) the aforementioned process. I suppose that ideally it has to look as follows:
- A mathematical statement is converted into a formula by means of, say, Kripke-Joyal semantics. Then it is proved by purely formal means of predicate logic.
- Such an approach has a visible advantage over alternative proofs.