coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Yet another dependent type question

From: Michael Shulman <viritrilbia AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Yet another dependent type question
Date: Tue, 30 Mar 2010 11:35:40 -0600
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=TPYzW2oslYE8ANONlctRjFF/QhdFA/fiJUQCWXA4PjDLBnxff0CBfCjf3rT2z4aEPb krM4ovd9/k0canRd81RNcOuzA7E50XctqpUOMhmweBXr4kGzjXP7n5vS8O355/lLOxDD DSo28yeC782P6jdpVoB43ULKAU4The3ltuFYc=

On Mon, Mar 29, 2010 at 3:59 AM, Hugo Herbelin
<Hugo.Herbelin AT inria.fr>
wrote:
> Do you then mean that you are interested in using Coq with axioms
> incompatible with the uniqueness of reflexive identity proofs?

Potentially, yes.  One possible such axiom is the "equivalence axiom"
proposed by Vladimir Voevodsky, which I believe can be found at his
web site.  Another possiblility is an adaptation of "quotient types"
to groupoid or homotopical models.  I think this area is in a very early
stage of development, though.

Mike

Re: [Coq-Club] finite sets in proofs, (continued)