My question is basically, what approaches have been made to make computer proof assistants which can handle the internal logic of a topos ?
To explain: while learning topos theory I was struck by the elegance of Mitchell-Bénabou language (the internal language of a topos). I was more delighted when I read Toposes and local set theories, by Bell, and found out that it is possible to build up the topos logic axiomatically, and use it to describe topos theory. Although I have not read it yet, I gather Lambek and Scott have a similar approach towards describing toposes (this time ones with natural number objects), using what they call intuitionistic type theories (but I am not sure about this). I have also heard there is dependent type theory, and homotopy type theory, but I do not really know about them.
Before I set off trying to build a proof assistant for local set theory independently, I wanted to understand what has been done before. So I have the following questions:
(1) Are dependent type theory, and/or homotopy type theory descriptive enough to handle the internal logic of a topos ? Are they at least as general as intuitionistic type theory / local set theory, in the sense that they can handle non-binary truth values etc. ?
(2) What is the state of the art type theory approach to handling topos logic ?
(3) What practical software exists for doing proofs in such type theories ? Should I be looking to agda, Coq, idris ? Do I have to write my own ?
I hope my lack of type theory knowledge does not make my questions sound too silly. I am just trying to find out which theory I should learn, for my goal of automating proofs in topos theory in a way which is acceptable by the communities of people doing computer assisted proofs, and type theory.
Best Answer
(1) Yes. The particular dependent type theory one wants to use has UIP (Uniqueness of Identity Proofs), one universe of all propositions (in the homotopy-type-theory sense, i.e. subsingletons) satisfying propositional extensionality, pushouts (a kind of higher inductive type), and propositional truncations. This is a sort of truncated version of homotopy type theory.
(2) The type theory described above is one state of the art. Alternatively, one can use higher-order logic as described, for instance, in Sketches of an Elephant. I tend to prefer dependent type theory, since dependent types occur naturally in mathematics; but the semantics and metatheory are more difficult in that case (and filling in some of their details is a problem of current research).
(3) Agda, Coq, Idris can all manage this type theory easily, when suitably augmented by axioms (for UIP, propositional extensionality, etc.). The main wrinkle is that they all have a tower of universes, which an arbitrary elementary topos may not; but you can just ignore the larger universes. You can also reason in higher-order logic inside such a proof assistant by simply not making use of the dependent types.