The Coq mailing list

[Cristóbal Camarero Coterillo <nakacristo AT hotmail.com>]

I know very little of the univalence axiom, mainly it implies extensionality (both propositional and functional, I think). Up to which understand it is not a commonly accepted axiom. Does it implies that all non-inhabited types are equal? I suppose it has some sense mathematically, but no so much in programming, where you can use empty classes with different names as identifiers. I have search a little and I haven't found a simple Coq file declaring the univalence axiom.

I got the array example from a library that I made some time ago working with dependent types (using a lot of JMeq, which I denoted by == ).

http://personales.unican.es/camareroc/coq/Array.html

I used in there several times this axiom
Axiom array_typeequality_down: forall (A:Type) (m n:nat),
array A m=array A n->m=n.

I suppose it is not actually necessary and that results like the following could be fixed by adding the hypothesis (m=n).

Lemma array_rewrite_dependent: forall (A B:Type) (m n:nat)
(a:array A m) (b:array A n)
(f:forall n:nat,array A n->B), a==b-> f m a=f n b.

Best regards

--Cristóbal Camarero