coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
- To: Michael Shulman <viritrilbia AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Yet another dependent type question
- Date: Mon, 29 Mar 2010 11:59:12 +0200
Hi,
> Anyway, as long as I'm commenting on this, let me say that I hope that
> if Coq is eventually extended in some way which makes axiom K or its
> equivalents provable, that it will at least be possible to turn off
> such an extension. Since my interest is largely in models such as
> groupoids and homotopy theory, I would not want uniqueness of
> reflexive identity proofs to be built into the system unavoidably.
A few people mentioned these models to me.
Do you then mean that you are interested in using Coq with axioms
incompatible with the uniqueness of reflexive identity proofs?
Hugo Herbelin
- Re: [Coq-Club] finite sets in proofs, (continued)
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
- Re: [Coq-Club] finite sets in proofs, Thomas Braibant
- Re: [Coq-Club] finite sets in proofs,
Stéphane Lescuyer
- Re: [Coq-Club] finite sets in proofs, Pierre Letouzey
- Re: [Coq-Club] finite sets in proofs, Chantal Keller
- [Coq-Club] Yet another dependent type question,
Pierre-Marie Pédrot
- Re: [Coq-Club] Yet another dependent type question,
Adam Chlipala
- Re: [Coq-Club] Yet another dependent type question,
Pierre Corbineau
- Re: [Coq-Club] Yet another dependent type question, Pierre-Marie Pédrot
- Re: [Coq-Club] Yet another dependent type question, Michael Shulman
- Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin
- Re: [Coq-Club] Yet another dependent type question, Michael Shulman
- Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin
- Re: [Coq-Club] Yet another dependent type question,
Pierre Corbineau
- Re: [Coq-Club] Yet another dependent type question,
Adam Chlipala
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
Archive powered by MhonArc 2.6.16.