coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bas Spitters <b.a.w.spitters AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>, Bruno Barras <bruno.barras AT inria.fr>, Pierre Corbineau <Pierre.Corbineau AT imag.fr>, Freek Wiedijk <freek AT cs.ru.nl>
- Cc: Todd Wilson <twilson AT csufresno.edu>
- Subject: Re: [Coq-Club] Proofs in an elementary topos
- Date: Tue, 18 Mar 2014 11:12:23 +0100
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
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
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.
- [Coq-Club] Proofs in an elementary topos, Todd Wilson, 03/17/2014
- Re: [Coq-Club] Proofs in an elementary topos, Daniel Schepler, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Ryan Wisnesky, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Benedikt Ahrens, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Bas Spitters, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Bas Spitters, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Vladimir Voevodsky, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Todd Wilson, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Vladimir Voevodsky, 03/19/2014
- Re: [Coq-Club] Proofs in an elementary topos, Victor Porton, 03/19/2014
- Re: [Coq-Club] Proofs in an elementary topos, Vladimir Voevodsky, 03/19/2014
- Re: [Coq-Club] Proofs in an elementary topos, Victor Porton, 03/19/2014
- Re: [Coq-Club] Proofs in an elementary topos, Vladimir Voevodsky, 03/19/2014
- Re: [Coq-Club] Proofs in an elementary topos, Todd Wilson, 03/18/2014
- Re: [Coq-Club] Proofs in an elementary topos, Bas Spitters, 03/18/2014
Archive powered by MHonArc 2.6.18.