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
--001a114dd0a63825eb053c4cca13--