Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proofs in an elementary topos

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proofs in an elementary topos


Chronological Thread 
  • 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

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.



Archive powered by MHonArc 2.6.18.

Top of Page