From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.33.196 with SMTP id s62mr13739517otb.8.1473675391942; Mon, 12 Sep 2016 03:16:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.29.35 with SMTP id m32ls10150907otm.7.gmail; Mon, 12 Sep 2016 03:16:31 -0700 (PDT) X-Received: by 10.129.161.14 with SMTP id y14mr15470778ywg.7.1473675391601; Mon, 12 Sep 2016 03:16:31 -0700 (PDT) Return-Path: Received: from mail-vk0-x232.google.com (mail-vk0-x232.google.com. [2607:f8b0:400c:c05::232]) by gmr-mx.google.com with ESMTPS id k69si1029012vkd.3.2016.09.12.03.16.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 12 Sep 2016 03:16:31 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) client-ip=2607:f8b0:400c:c05::232; 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::232 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x232.google.com with SMTP id f76so126737991vke.0 for ; Mon, 12 Sep 2016 03:16:31 -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=CvHVZ3yWEMCPJK+tySsSOeKhmtYVfSMMtVvygguIYSA=; b=pSh7QRsHeVT0dLJILt/qT7FQ2UFxb6xrby6uz/e8Gz4JLUCfDofdXMQ9Y3Mra3+JVN pYLqm2tPfEXXS9AkQM6Xb9J24YZluEa03RudinGHFF09wsV6/pN/bssNEy1ztU8h/YeM MwGsNQeAYf3sZOY59bUFYljWyTUlg8wbNqs3YysqT4UDzzhbZxoYR+CbpoXiCOzOvV60 LW3HYdLHqbmr5AMkeEhi9Sv9Wp+/YNmwnoPH8Zvq1HAOgE+asCDTrK1qKU6s8TGJ35+d BPVC3lIR2Sv1bh//rrHZXAaa4sw8CI/bJgPDcmHOqDj0xBydW7xbf5VqrglzwckYMARh 8CrA== X-Gm-Message-State: AE9vXwPNh8a0t6vb/3IizQBj2hO4hXEyPtzyjJwZJOhkuceRqwQGCOjdvMCRhR4V+R+uvzNhI3GbXUgOe3loLw== X-Received: by 10.31.72.134 with SMTP id v128mr11580493vka.77.1473675391409; Mon, 12 Sep 2016 03:16:31 -0700 (PDT) MIME-Version: 1.0 Received: by 10.176.1.43 with HTTP; Mon, 12 Sep 2016 03:16:30 -0700 (PDT) In-Reply-To: References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> From: Peter LeFanu Lumsdaine Date: Mon, 12 Sep 2016 12:16:30 +0200 Message-ID: Subject: Re: [HoTT] Re: Meta-conjecture about MLTT To: Andrew Polonsky Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a114dd0a63825eb053c4cca13 --001a114dd0a63825eb053c4cca13 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Mon, Sep 12, 2016 at 7:20 AM, Andrew Polonsky wrote: > 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. >> > > What do you mean by a "property", exactly? > There=E2=80=99s also a difference in what you mean by a =E2=80=9Ctype=E2=80= =9D, which is I think the key difference between the argument I gave, and Andrew=E2=80=99s counte= rexample (and others=E2=80=99). The counterexamples show that there can be properties of *small* types, i.e. type families [ X : U |=E2=80=94 P(X) Type ], which can distinguish is= omorphic (small) types. The construction I described shows that no property of *all* types =E2=80= =94 i.e. no type [ . |=E2=80=94 P(X) Type ], where X is a new base type, so any clos= ed type can be substituted for X =E2=80=94 can distinguish isomorphic types. =E2=80=93p. --001a114dd0a63825eb053c4cca13 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On Mon, Sep 12, 2016 at 7:20 AM, Andrew Polonsky <andr= ew....@gmail.com> wrote:
The meta-task is to eith= er produce two isomorphic types in an empty=20
context, together with a property that one of them provably has but the= =20
other doesn't, or to show that this is impossible.

What do you mean by a "propert= y", exactly?

There=E2=80= =99s also a difference in what you mean by a =E2=80=9Ctype=E2=80=9D, which = is I think the key difference between the argument I gave, and Andrew=E2=80= =99s counterexample (and others=E2=80=99).

The cou= nterexamples show that there can be properties of *small* types, i.e. type = families [ X : U |=E2=80=94 P(X) Type ], which can distinguish isomorphic (= small) types.

The construction I described shows t= hat no property of *all* types =E2=80=94 i.e. no type [ . |=E2=80=94 P(X) T= ype ], where X is a new base type, so any closed type can be substituted fo= r X =E2=80=94 can distinguish isomorphic types.

= =E2=80=93p.
--001a114dd0a63825eb053c4cca13--