The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

I am not entirely sure what you want.

1. In line with Benedict's answer: If you want the axioms of a predicative, or PiW-pretopos, then using hSets in the univalent library would be a good idea.
Have a look at Ch10 of the HoTT book and the related library.
https://github.com/HoTT/HoTT/
We have some more explanation here.
http://www.cs.ru.nl/~spitters/hsets.pdf

One would need to add the propositional resizing axiom (impredicativity). As Daniel says this would give you some extra axioms, not only the NNO, but also the universe.

They may be harmless, depending on what you want to achieve.

2. There is also the work on IZF in Coq by Bruno Barras, and the references therein.
http://jfr.unibo.it/article/view/1695
There is also work on importing HOL-light in Coq, by Pierre Corbineau which I cannot find currently:
http://hal.archives-ouvertes.fr/docs/00/52/06/04/PDF/itp10.pdf
http://www.cs.ru.nl/~freek/notes/holl2coq.pdf

One would need to remove the excluded middle, but I understand this should not be very difficult.

On Tue, Mar 18, 2014 at 8:22 AM, Benedikt Ahrens <benedikt.ahrens AT gmx.net> wrote:

Hi,

I have been thinking about implementing toposes in Coq augmented by the Univalence Axiom (i.e. in the Univalent Foundations).
The basic examples of toposes are, in particular, univalent categories (see [1], there just called "categories"), which are categories where isomorphism of objects coincides with their equality, thus it would make sense to define a topos to be univalent in that context.
One could then use Coq's notation mechanism and tactics language to get a kind of internal language of a topos in Coq.

Starting out with just the necessary properties of a topos and deducing the rest would probably take quite a long time, but if you are willing to define a topos to have all these properties, you could get started quite quickly going this way. One could replace the axioms by proofs of those properties later.

Best,
Benedikt

[1] http://arxiv.org/abs/1303.0584

On 03/17/2014 08:26 PM, Todd Wilson wrote:

Hi, all:

Does anyone have a library or set-up that exactly captures the logic
of elementary toposes? I'm looking for a way to prove theorems in an
interactive environment, ideally Coq, so that I'd know that all of the
theorems I'd proven are true in every elementary topos. Even better
would be to have the ability to extract terms in any one of the
several equivalent languages of elementary topos theory witnessing the
theorems I prove. Thanks!