Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Dependent Type Problem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependent Type Problem


Chronological Thread 
  • 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







Archive powered by MHonArc 2.6.18.

Top of Page