For those interested in formalizing internal topos-theoretic arguments in a proof assistant, I'd like to make a plug for a newer entry on the usual list of provers, namely the Lean Theorem Prover [1]. In Lean, Prop is impredicative and extensional, and so it functions much like a subobject classifier, allowing a direct encoding of topos-theoretic arguments. As an example, you can look at my formalization [2] of the results from my paper J. Todd Wilson, "An Intuitionistic version of Zermelo's proof that every choice set can be well-ordered", J. Symbolic Logic, 66:3 (2001), 1121-1126. Abstract: We give a proof, valid in any elementary topos, of the theorem of Zermelo that any set possessing a choice function for its set of inhabited subsets can be well-ordered. Our proof is considerably simpler than existing proofs in the literature and moreover can be seen as a direct generalization of Zermelo's own 1908 proof of his theorem. This "elementary" proof, besides being a direct generalization of Zermelo's, makes crucial use of both impredicativity and extensionality of the subobject classifier, and so is a good illustration of these features of Lean when it comes to doing such formalizations. (The "existing proofs in the literature" mentioned in the abstract referred to proofs of Freyd and Axel.) Also, if I can be permitted an additional self-plug, this proof does not appear to be well-known, since there is no reference to it in Section D4.5 of Johnstone's Elephant book or, for example, in the article on the well-ordering theorem in the nLab [3]. [1] https://leanprover.github.io/ [2] https://github.com/lambdacalculator/lean-choice [3] https://ncatlab.org/nlab/show/well-ordering+theorem -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh [For admin and other information see: http://www.mta.ca/~cat-dist/ ]