From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Sun, 11 Sep 2016 22:20:09 -0700 (PDT)
From: Andrew Polonsky <andrew....@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <ca38369f-7691-46f7-8d00-2c944ec6e489@googlegroups.com>
In-Reply-To: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com>
References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com>
Subject: Re: Meta-conjecture about MLTT
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_2047_2019767314.1473657609808"

------=_Part_2047_2019767314.1473657609808
Content-Type: multipart/alternative; 
	boundary="----=_Part_2048_148110370.1473657609808"

------=_Part_2048_148110370.1473657609808
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit


>
> 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?

If you mean a type family, e.g.,

    X : U |-  P(X) : Type

then a counterexample is

A = Nat x Bool
B = Bool x Nat
P(X) = Id(U;X,A)

Cheers,
Andrew

------=_Part_2048_148110370.1473657609808
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><blockquote class=3D"gmail_quote" style=3D"margin: 0;margi=
n-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">The meta-task=
 is to either produce two isomorphic types in an empty=20
<br>context, together with a property that one of them provably has but the=
=20
<br>other doesn&#39;t, or to show that this is impossible.
<br>
</blockquote><div><br></div><div>What do you mean by a &quot;property&quot;=
, exactly?</div><div><br></div><div>If you mean a type family, e.g.,</div><=
div><br></div><div>=C2=A0 =C2=A0 X : U |- =C2=A0P(X) : Type</div><div><br><=
/div><div>then a counterexample is</div><div><br></div><div>A =3D Nat x Boo=
l</div><div>B =3D Bool x Nat</div><div>P(X) =3D Id(U;X,A)</div><div><br></d=
iv><div>Cheers,</div><div>Andrew</div></div>
------=_Part_2048_148110370.1473657609808--

------=_Part_2047_2019767314.1473657609808--