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

Question

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.

Answer 1

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.

Answer 2

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.