The Coq mailing list

[Nicola Gambino <N.Gambino AT leeds.ac.uk>]

Hello,

The issue of characterising types that are equivalent (in the sense of 
Univalent Foundations) to standard inductive types (such as Bool, Nat, and 
W-types) is discussed also in the paper “Homotopy-initial algebras in type 
theory”, written with S. Awodey and K. Sojakova 
(http://arxiv.org/abs/1504.05531). The relevant notion is that of 
homotopy-initiality. 

With best wishes,
Nicola


> On 18 Dec 2015, at 19:10, Bruno Barras 
> <bruno.barras AT inria.fr>
>  wrote:
> 
> 
> Hi,
> 
> I'd think so. You can define a constant PE' with the same type as PE that 
> is based on EP, and prove this PE' commutes with EP:
> 
> Definition PE' n : P (E n) = n.
> rewrite <- (PE n).
> apply (f_equal P).
> apply EP.
> Defined.
> 
> Lemma comm x : f_equal P (EP x) = PE' (P x).
> <proof not trivial but doable>
> 
> So we get the good notion of equivalence.
> If you replace PE by PE' in the rest of scripts, you should be able to 
> finish the proof, which I haven't checked.
> 
> Bruno.
> 
> 
> De: "Jason Gross" 
> <jasongross9 AT gmail.com>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Vendredi 18 Décembre 2015 17:57:25
> Objet: Re: [Coq-Club] Dependent Type Problem
> 
> You should be able to do it for other (non-hset) types by "adjusting" the 
> isomorphism into a good notion of equivalence, and using that instead, 
> right?
> 
> -Jason
> 
> 

===
Dr Nicola Gambino
School of Mathematics
University of Leeds
E-mail: 
n.gambino AT leeds.ac.uk