coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nicola Gambino <N.Gambino AT leeds.ac.uk>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Dependent Type Problem
- Date: Fri, 18 Dec 2015 19:29:45 +0000
- Accept-language: en-GB, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=N.Gambino AT leeds.ac.uk; spf=Pass smtp.mailfrom=N.Gambino AT leeds.ac.uk; spf=Pass smtp.helo=postmaster AT mhost02h.leeds.ac.uk
- Ironport-phdr: 9a23:LLuCxhYUcXwKcCj4xAuDfpf/LSx+4OfEezUN459isYplN5qZpcm/bnLW6fgltlLVR4KTs6sC0LqI9fi4EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35rxj7j60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLVry/dKAlR5RZCi4nOiY7/oej4RLEVE6E4mYWemQQiBtBRQbfukLURJD05w37ve150WG1NMj8TLYzEWCEqYhiTRXpjiAvMzM0/HqRg8c2kaEN80HpnAB234OBONLdD/F5ZK6IJd4=
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:23
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
- [Coq-Club] Dependent Type Problem, Gert Smolka, 12/17/2015
- Re: [Coq-Club] Dependent Type Problem, Abhishek Anand, 12/17/2015
- Re: [Coq-Club] Dependent Type Problem, Gert Smolka, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Abhishek Anand, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Gert Smolka, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Thorsten Altenkirch, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Thorsten Altenkirch, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Jason Gross, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Bruno Barras, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Nicola Gambino, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Thorsten Altenkirch, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Bruno Barras, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Jason Gross, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Thorsten Altenkirch, 12/18/2015
- Re: [Coq-Club] Dependent Type Problem, Abhishek Anand, 12/17/2015
Archive powered by MHonArc 2.6.18.