Proof assistant for working in weaker foundations?

Question

In some of my works I need to prove some results within the internal logic of categories with not much structures (like pretoposes or even just categories with finite limits). The kind of things I want to prove typically involve manipulating inductive type (like a natural number object, a type of binary tree, some W-types etc...) and prove some of their properties in these relatively weak categories.

Let me give some examples of the sort of results I'm interested in:

• If C is a cartesian category (or category with finite limits) with a parametrized natural number objects $N$ then $N \times N \simeq N$.

• If C is a cartesian category with a (parametrized) natural number objects $N$, then $N$ is also a parametrized list object for $N$, and a parametrized finite tree objects.

• If C is a pre-topos with parametrized list objects then essentially any kind of finitary free constructions (like free groups, free monoids, free left exact categories etc...) can be performed.

• Which of these free construction can already be performed in a cartesian category/ a category with finite limits/an extensive category ?

• If C is a a pretopos in which some (non finite) objects are exponentiable, and for which the corresponding W-types exists, then certain free infinitary constructions exists.

etc... those are only examples, most of them are already well known results, but they are very typical of the kind of things I'm trying to do. Note that I want to work with "internal" proof, and not proving results externally directly in terms of such categories.

I believe that this sort of things is typically a good place to try to use a proof assistant as the proof have to be spelled out in a very high level of details anyway and one can easily makes mistake.

So I'm looking for a proof assistant that would be appropriate for this.

I already started experimenting in Coq. My current strategy is to just be careful about what I'm doing: for example, only use induction principle for propositions without quantifier, or only those authorized by the specific framework I'm working in... And of course not use anythings coming from a library, and only use very explicit tactics to avoid hiding possible problems. So I'm not really using the proof assistant as a definitive witness of validity of a proof, but only as somethings that makes every single step of a proof explicit enough so that I can tell immediately if it makes sense or not in the framework I'm interested in.

This already not too bad, but I was hopping to find a more precise/formal way to do this.

• Is there other proof assistant which have more flexible logical background ?

• From my experience (but I'm not very familiar with the precise logical framework that Coq uses, so I can't makes what follows a formal statement, but if someone can confirm it it would be very helpful) everything that I can define in coq can be interpreted in a 'Stack' or 'Sheaves' semantics over the category I'm working in. So the only thing that I need to be careful, is to not apply an induction principle to construct functions into something that is not an object of my category. So would there be a way in Coq, or in any other proof assistant, to say that I have a nice class of sets (which would be the representables), stable under some operations (corresponding to the structure I'm putting on my category) and that when I define inductive operations or use inductions it has to be restricted to things taking values in a set in this class. But I would still like to be able to use the nice machinery of "match" "induction" "fixpoint" that Coq offers. Maybe a way to check afterward what kind of induction does a given proof uses ?

• Any other suggestions on how to do this sort of things ?

PS: I was unsure this question was suitable for MO or not. I had the impression it was "mathematical enough" but I do have too admit that a good answer could be something technical about the inner working of some proof assistant. So If you think there is a better place to ask this question, please tell me.

Answer 1

One possibility that's worth thinking about is to use a "meta-proof-assistant" like Twelf, which implements a meta-theoretic logical framework inside of which you can specify any "object language" you like. It's better-adapted to proving meta-theoretic properties about the object-language, but it can also be used to prove theorems in the object language, although it doesn't have nice syntactic sugar like match and fixpoint or support for tactics.

It might also be possible to implement the type theories you're interested in inside of Isabelle or something like it, which is supposed to be a "generic proof assistant", but I'm not very familiar with that.

Regarding Coq, I don't know of an "after the fact" way to check what kind of induction a proof uses. But if you're willing to call induction principles explicitly rather than using match/fix, you could use a "private inductive type" hack similar to the way that we implement HITs in HoTT. That is, postulate your family of "representable" types and its closure conditions, then define your inductive type as a Private Inductive in a module, prove a version of the induction principle that requires the target to be representable, and then export only that restricted induction principle.