11
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ This question is exactly what I have been wondering about for a while. Looks like there isn't just a lot literature on it. $\endgroup$
    – xuq01
    Jan 25, 2021 at 20:13

1 Answer 1

12
$\begingroup$

(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.

$\endgroup$
4
  • 1
    $\begingroup$ Thank you for your answer. I wonder if there is specific literature where someone is considering such a theory. What you describe seems to be a custom combination of dependent type theory assumptions. I wonder if you could recommend literature for a newbie to type theory, to be able to understand how to setup what you describe in (1). Should I read the Hott book, or `practical foundations of mathematics', or something else ? I also wonder if there are particular projects underway where people are developing proof assistants in these kind of topos theory directions. $\endgroup$ Aug 25, 2020 at 17:35
  • 2
    $\begingroup$ Unfortunately, most of the literature on topos theory uses higher-order logic instead of dependent type theory. The best reference I know of for dependent type theory as an internal language of toposes is Maietti's Modular correspondence between dependenttype theories and categories includingpretopoi and topoi. It's more of a research paper than a textbook introduction, though. For a newbie you could do worse than the HoTT Book. $\endgroup$ Aug 26, 2020 at 1:25
  • $\begingroup$ But if you only consider one universe, then you are in trouble to formalize category theory, right? $\endgroup$
    – Bob
    Aug 26, 2020 at 8:36
  • 1
    $\begingroup$ @Bob Yes, that's true. Semantically, you can solve that problem by working in the 2-topos of indexed categories or stacks over your 1-topos, which has one more universe (the self-indexing). Its internal logic is a "2-truncated" form of HoTT. Unfortunately, the only reference I know of for that is a paper on my own "to-write" list... (-:O $\endgroup$ Aug 26, 2020 at 12:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .