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.