The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi Cristobal,

The tension between structural and nominal typing is an old one. I would always use structural typing in my core language and view nominal typing as an extension which can be explained by saying that a nominal type is a type with a name (or a stamp) and that there is an implicit coercion between nominal types and types. This doesn’t only handle the uses of the empty type you mention but also situations where different nominal types like age and salary are represented by integers. 

Regarding univalence: it should be commonly accepted because it tells you what is the equality of types which is otherwise left open.

I haven’t got enough time to study your library. Could you point out where you need injectivity of array?

Cheers,

Thorsten

From: <coq-club-request AT inria.fr> on behalf of Cristóbal Camarero Coterillo <nakacristo AT hotmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Thursday, 2 March 2017 at 08:33
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] injectivity of inductive type implies False

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
Axiomarray_typeequality_down:forall(A:Type)(mn:nat),
arrayAm=arrayAn->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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.