How to use a proof assistant to reason in a topos?

I would like to use a proof assistant to reason in the internal language of a topos. More specifically, I would like to (be able to) formalise informal arguments such as in Ingo Blechschmidt's PhD Thesis. As I understand it, many proof assistants (such as Lean) are designed with the purpose of formalising standard mathematics (i.e. their intended models are in $$\mathtt {Set}$$). They have, at least Lean, many hard-coded features that I do not like.

Is there a proof assistants which implements a dependent type theory that is meant to be used in a topos, such as for example the dependent type theories in the last chapter of B. Jacobs book Categorical Logic and Type Theory? Or can I just use a subset of the language of CoQ, Lean, or Agda? If so, which subset I am allowed to use, and has someone checked carefully that it is sound?

I have read in some places that people use proof assistants to reason internally. How do you do that? Do you change the source code of existing proof assistants to get a type theory of which you are sure that it has a sound semantic? Or do you just start and hope for the best, not checking all the details? Are there examples of projects at which I can look?

I am familiar with the main ideas, and I believe that arguments such as in Ingos thesis can be checked formally. But for once I would like to see (or write) one or two non-trivial proofs with all the details.

• @Guy Coder: Sure, I can do it this evening.
– Nico
Feb 13 at 13:31
• Did you ask the author of the PhD thesis? He seems to be working with proof assistants now, see github.com/iblech Feb 13 at 13:44
• I assume "topos" means Grothendieck topos. I don't think Lean has any hard-coded features that aren't valid in a topos (you can avoid choice and check you did so with #print axioms, and then add back the missing "axiom of unique choice") except for universes, which will be the main issue with any attempt at doing this. But then mathlib may be of limited use, as it makes little effort to avoid choice. Feb 13 at 16:55
• @ReidBarton: Lean tactics pull in excluded middle while you're not watching. I would expect that to be quite annoying. Feb 13 at 17:56
• Related question on MO: mathoverflow.net/q/294651/49 Feb 14 at 18:37

2 Answers

If I may offer a bit of general advice to all who are asking “where do I find a proof assistant whose foundation precisely matches the one I need“: you do not need an exact match, just one that is compatible with your foundation. And even if it is not 100% compatible, you should still go ahead and use whatever is available. With a bit of lack it will not be difficult to manually check that your formalization is within the desired fragment.

In a typical situation the proof assistant available to you will mismatch the desired foundation in two ways:

1. It will be too powerful in some respects (assumes excluded middle, has many universes but you have none, supports inductive-recursive types but a topos does not, etc.)

2. It will be too weak in some respects (does not assume function extensionality, does not have a subobject classifier).

With regards to the first mismatch: if avoiding the forbidden features is relatively easy, then they might not be a deal breaker. For example, in Agda it is not too difficult to make sure that you're working inside a single universe all the time. However, as soon as you start using libraries that were not designed for your purpose, it will be difficult to track what got used: did Lean use excluded middle, did Agda use an inductive-recursive type, did Coq use more universes than it was suppoed to?

With regards to the second mismatch: you can often just postulate the stuff that is missing. Even better, try to formalize as much as you can without postulating the missing stuff – that will make your work more general!

Here are some concrete possibilities on how to do the internal language of a topos in Agda and Coq. It is not perfect, but is probably good enough at least for some initial experiments.

Agda

Since in Agda universes are explicit, it is not too difficult to work in a single universe: just make sure every type you ever mention is in Set.

You will have to axiomatize the subobject classifier $$\Omega$$. This can be done in two steps:

1. Define a proposition to be a type all of whose elements are equal.
2. Postulate a type Ω that classifies all propositions.

I would expect there to be very few places where you need the full power of Ω, so you should attempt to avoid it altogether. Many arguments that one carries out in a topos work equally well in a predicative setting that has a hierarchy of subobject classifiers, with the $$n$$-th subobject classifier $$\Omega_n$$ living in the $$(n+1)$$-st universe and classifying propositions in the $$n$$-universe.

You will want to postulate function extensionality, though.

And since a topos validates extensional type theory, you can safely use Agda's axiom K.

Coq

To stay in a single universe, declare every type you ever use to be in Set. You do not have to postulate Ω because Coq's Prop is already impredicative and is compatible with it being the subobject classifier. If you want to actually state that it is the subobject classifier, you will need further postulates (as remarked below) that state the elements of Prop are (homotopy) propositions.

You will likely want Axiom K, function extensionality, and unique choice.

• Can you explain "Lean tactics sneak in excluded middle behind your back"? Feb 13 at 18:17
• Here's one that bit me the other day. The Prop.linear_order instance uses classical. The instance got used behind my back somehow when I used simple_graph.max_degree. Feb 13 at 22:50
• Mathlib is a classical library. We do not support constructivist users. Constructivism holds us back from our goals. Constructivists have tried to use mathlib before and do sometimes complain about things like this, but it's wontfix right now. Feb 13 at 23:08
• First of all, I am not a constructivist, as I think I pointed out to you a couple of times before. The problem with the above snippet has nothing to do with constructivism. The problem is, that while trying to develop a computable function, for the purpose of enriching Lean with some graph-theoretic goodies, Lean used classical and suddenly made a function noncomputable. Do you know how I can tell Lean "I really, really want this function to be computable, don't do anything that will ruin that?" I need the function to compute because we'll run it on concrete graphs. Feb 13 at 23:16
• Let me also explain why I made the remark in the first place. The OP asked for a PA for the internal logic of a topos, which is intuitionistic (and this has nothing to do with constructivism either). It is conceivable that one would use a classical PA and try to avoid using excluded middle (analogously to using Agda and limiting everything to a single universe). 1/2 Feb 13 at 23:27

You also asked about example projects which use proof assistants to reason internally in a topos. In the context of HoTT, Orton and Pitts have used (standard extensional) Agda to investigate operations on the interval in cubical type theory. This approach has also been used to study modal cubical type theories by Licata, Orton, Pitts and Spitters.

Chapter 4 of Orton's PhD thesis discusses the approach in a bit more detail. In particular, he weighs up some tensions between the theorem prover and the intended model, which will inevitably occur as Andrej discusses.