From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.228.66 with SMTP id n63mr13680036ywe.57.1473631713039; Sun, 11 Sep 2016 15:08:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.21.49 with SMTP id u46ls1095779otf.43.gmail; Sun, 11 Sep 2016 15:08:32 -0700 (PDT) X-Received: by 10.129.84.69 with SMTP id i66mr13039812ywb.29.1473631712431; Sun, 11 Sep 2016 15:08:32 -0700 (PDT) Return-Path: Received: from mail-vk0-x22c.google.com (mail-vk0-x22c.google.com. [2607:f8b0:400c:c05::22c]) by gmr-mx.google.com with ESMTPS id v141si962157vke.1.2016.09.11.15.08.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 11 Sep 2016 15:08:32 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22c as permitted sender) client-ip=2607:f8b0:400c:c05::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22c as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x22c.google.com with SMTP id v189so110993549vkv.1 for ; Sun, 11 Sep 2016 15:08:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=tUX0WDKhAE3hpu8brbHPGCGo4TIZdFtKTxQQTeHRRnM=; b=c8jgTf+UvzF/vdseelU+hRlE8/I+anrIU3cun/d7KY7W391RS06t8bzNnyUz2l36Cw Si0qXe/HoIfDqKmOLsB5g0jceMB27e3elo2jxeJ2a6+MIYDOQZfaSYP1Uq8QBpTnfhBu vNcL0SPR0AZSA/E2B2L+lvGzX+JUX6wzfQlRybd12daiZIz9iSCm+z2o/UBNXJub7lbI ILWAi6tXIL38Q4ur7cyTGyygBD/1YrtT39GUmfyjk1fWgb6Kqfxflaq0+ndcGi3d3/hh uBZzZ7D89fH3G5F2BUYroqp5zR+87N5URtguioXbA2cHhq0hijgvNyVQjStjBUF9Trcl XuuA== X-Gm-Message-State: AE9vXwNwsSDOxZ33BSULfBtDJSedKCQgTZHjv+we/0qPopk72bSHgBq9SdsGsRzNxPvv7vrCOd7jwceGq3lvmA== X-Received: by 10.31.60.72 with SMTP id j69mr8223764vka.136.1473631712216; Sun, 11 Sep 2016 15:08:32 -0700 (PDT) MIME-Version: 1.0 Received: by 10.176.1.43 with HTTP; Sun, 11 Sep 2016 15:08:31 -0700 (PDT) In-Reply-To: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> From: Peter LeFanu Lumsdaine Date: Mon, 12 Sep 2016 00:08:31 +0200 Message-ID: Subject: Re: [HoTT] Meta-conjecture about MLTT To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=001a11438472bc8b8e053c429e82 --001a11438472bc8b8e053c429e82 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable As you conjecture, MLTT with equality reflection can=E2=80=99t distinguish = between isomorphic types. Precisely, let MLTT[X] be the extension of MLTT by a single closed base type X. Suppose \C is a model of MLTT =E2=80=94 presented as a CwA with appropriate= extra logical structure =E2=80=94 and A, B are two isomorphic types in it, over t= he empty context. So A, B induce two interpretations of MLTT[X] in \C. Then there=E2=80=99s a CwA \C^\iso, with the category of isomorphisms in \C= , and with a type over an iso =D0=931 <~> =D0=932 being a pair of types A1, A2 ov= er =D0=931, =D0=932 that correspond under reindexing along the isomorphism. Now I claim this carries suitable structure to again model MLTT[X], and furthermore (importantly) such that the two projection maps \C^\iso =E2=80= =94> \C both preserve all the logical structure. For most logical type-formers (Pi=E2=80=99s, Sigma=E2=80=99s, etc), the structure is by showing that thes= e type-formers are provably functorial in isomorphisms. (This uses the equality reflection.) For the universe(s), this just uses the identity iso on the universe(s) of \C. The base type X, we model by the given isomorphism A <~> B. So this induces an interpretation of MLTT[X] in \C^\iso, whose two projections to \C are the two original interpretations in \C. In particular, if P is any type in MLTT[X] =E2=80=94 i.e. a property of an arbitrary type definable in MLTT =E2=80=94 then its interpretation in \C^\i= so is an isomorphism P[A] <~> P[B]. I think this is a reasonable positive answer to your question? I don=E2=80=99t remember anywhere this construction appears in the literatu= re, but I=E2=80=99ve always assumed that it has been noted before. (Actually, I=E2= =80=99d be very glad to hear a reference if anyone remembers seeing this somewhere, even if only in folklore not in print.) Without identity reflection, it no longer works =E2=80=94 since one doesn=E2=80=99t know that the logical structure i= n \C respects isomorphisms between types =E2=80=94 but essentially the same approach work= s once one replaces isomorphisms by equivalences. This is in the work of Chris Kapulkin=E2=80=99s and mine that I presented in Bonn in February, which we = hope to have written up very soon=E2=80=A6 Best, =E2=80=93Peter. On Sun, Sep 11, 2016 at 10:47 PM, 'Martin Escardo' via Homotopy Type Theory wrote: > In MLTT with equality reflection, we cannot distinguish isomorphic types. > > There was some agreement regarding this in previous discussions here in > this list in the past (I think). > > But I don't think we actually saw a proof (have we?). As far as I > understand, we only saw that natural attempts to distinguish examples of > isomorphic types fail. There was some invokation of realizability models = to > try to justify this. But I am not (yet) convinced by the arguments I have > seen so far. > > Nevertheless, I am convinced that equality reflection in MLTT cannot be > used to distinguish any particular pair of isomorphic types. (Prove me > wrong.) > > The meta-task is to either produce two isomorphic types in an empty > context, together with a property that one of them provably has but the > other doesn't, or to show that this is impossible. > > I am strongly inclined to think that this is impossible: that so-called > extensional MLTT cannot distinguish isomorphic types. > > In particular, equality-reflection has nothing whatsoever to do 5with > elementwise equality. > > Of course, what makes this difficult is that MLTT with equality reflectio= n > is inconsistent with univalence. > > > Martin > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --001a11438472bc8b8e053c429e82 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
As you conjecture, MLTT with equality reflection can=E2=80= =99t distinguish between isomorphic types.

Precisel= y, let MLTT[X] be the extension of MLTT by a single closed base type X.

Suppose \C is a model of MLTT =E2=80= =94 presented as a CwA with appropriate extra logical structure =E2=80=94 a= nd A, B are two isomorphic types in it, over the empty context.=C2=A0 So A,= B induce two interpretations of MLTT[X] in \C.

Th= en there=E2=80=99s a CwA \C^\iso, with the category of isomorphisms in \C, = and with a type over an iso =D0=931 <~> =D0=932 being a pair of types= A1, A2 over =D0=931, =D0=932 that correspond under reindexing along the is= omorphism.

Now I claim this carries suitable struc= ture to again model MLTT[X], and furthermore (importantly) such that the tw= o projection maps \C^\iso =E2=80=94> \C both preserve all the logical st= ructure.=C2=A0 For most logical type-formers (Pi=E2=80=99s, Sigma=E2=80=99s= , etc), the structure is by showing that these type-formers are provably fu= nctorial in isomorphisms. =C2=A0(This uses the equality reflection.) =C2=A0= For the universe(s), this just uses the identity iso on the universe(s) of = \C.=C2=A0 The base type X, we model by the given isomorphism A <~> B.=

So this induces an interpretation of MLTT[X] in \= C^\iso, whose two projections to \C are the two original interpretations in= \C.

In particular, if P is any type in MLTT[X] = =E2=80=94 i.e. a property of an arbitrary type definable in MLTT =E2=80=94 = then its interpretation in \C^\iso is an isomorphism P[A] <~> P[B].= =C2=A0 I think this is a reasonable positive answer to your question?
=

I don=E2=80=99t remember anywhere this construction app= ears in the literature, but I=E2=80=99ve always assumed that it has been no= ted before. =C2=A0(Actually, I=E2=80=99d be very glad to hear a reference i= f anyone remembers seeing this somewhere, even if only in folklore not in p= rint.) =C2=A0Without identity reflection, it no longer works =E2=80=94 sinc= e one doesn=E2=80=99t know that the logical structure in \C respects isomor= phisms between types =E2=80=94 but essentially the same approach works once= one replaces isomorphisms by equivalences.=C2=A0 This is in the work of Ch= ris Kapulkin=E2=80=99s and mine that I presented in Bonn in February, which= we hope to have written up very soon=E2=80=A6

Bes= t,
=E2=80=93Peter.


On Sun, Sep 11, 2016 at 10= :47 PM, 'Martin Escardo' via Homotopy Type Theory <Hom= otopyT...@googlegroups.com> wrote:
In MLTT with equality reflection, we cannot distinguish isomorphic = types.

There was some agreement regarding this in previous discussions here in thi= s list in the past (I think).

But I don't think we actually saw a proof (have we?). As far as I under= stand, we only saw that natural attempts to distinguish examples of isomorp= hic types fail. There was some invokation of realizability models to try to= justify this. But I am not (yet) convinced by the arguments I have seen so= far.

Nevertheless, I am convinced that equality reflection in MLTT cannot be use= d to distinguish any particular pair of isomorphic types. (Prove me wrong.)=

The meta-task is to either produce two isomorphic types in an empty context= , together with a property that one of them provably has but the other does= n't, or to show that this is impossible.

I am strongly inclined to think that this is impossible: that so-called ext= ensional MLTT cannot distinguish isomorphic types.

In particular, equality-reflection has nothing whatsoever to do 5with eleme= ntwise equality.

Of course, what makes this difficult is that MLTT with equality reflection = is inconsistent with univalence.


Martin


--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a11438472bc8b8e053c429e82--