The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

On Tue, Mar 30, 2010 at 11:35:40AM -0600, Michael Shulman wrote:
> 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.

I had recently the chance to attend a talk by Thomas Streicher on the
equivalence axiom. I have been convinced by the "any two types in
bijective correspondence are equal" part of the axiom but I'm unsure I
have understood what the "two different bijections between types map
to two different proofs of equality of these types" part of the axiom
(the part which contradicts axiom K if I'm correct) exactly might
provide in practice.

Hugo Herbelin