From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Mon, 12 Sep 2016 03:07:08 -0700 (PDT)
From: Andrew Polonsky <andrew....@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Cc: jason...@gmail.com
Message-Id: <a616964a-d650-4b95-b395-aa8e8af0f1d8@googlegroups.com>
In-Reply-To: <CABcT7WCAoDsh_Jz_e-JRMEk4E0cLQ=kM2FgsLCPA5SdtURaLjA@mail.gmail.com>
References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com>
 <ca38369f-7691-46f7-8d00-2c944ec6e489@googlegroups.com> <CAKObCaooaVyFoh-Xr5S8gMj--35FQNUGwQZ8t0CejRQhhRnNJA@mail.gmail.com>
 <CABcT7WCAoDsh_Jz_e-JRMEk4E0cLQ=kM2FgsLCPA5SdtURaLjA@mail.gmail.com>
Subject: Re: [HoTT] Re: Meta-conjecture about MLTT
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_8916_923317033.1473674829001"

------=_Part_8916_923317033.1473674829001
Content-Type: multipart/alternative; 
	boundary="----=_Part_8917_1388300779.1473674829001"

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

Hm, the two types are not provably isomorphic... Ok, this is a tricky 
question indeed!

On Monday, September 12, 2016 at 11:55:45 AM UTC+2, Andrew Polonsky wrote:
>
> > I suspect "one of them provably has but the other doesn't" should mean 
> "one 
> > of them provably has but the other provably does not have". 
>
> Type theory with reflection rule usually contains the rule equating 
> all proofs of equality: 
>
>        p : Id(A;x,y) 
> --------------------------- 
>   p == refl : Id(A;x,y) 
>
> If this is admitted, then the following modified example works: 
>
> A = Id(U;Bool,Bool) 
> B = Iso(Bool,Bool) 
> P(X) = Id(U;A,X) 
>
> Clearly, P(A).  Suppose P(B).  By equality reflection, A == B : U. 
> But then, for x : Iso(Bool,Bool), we have x : Id(U;Bool,Bool), whence x == 
> refl. 
> Since this holds for arbitrary x, we have x==y for arbitrary x,y : 
> Iso(Bool,Bool), a contradiction. 
>
> Generally, I think any proof that equality reflection is inconsistent 
> with univalence could be adapted to yield a counterexample as above. 
>
> Cheers, 
> Andrew 
>

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

<div dir=3D"ltr">Hm, the two types are not provably isomorphic... Ok, this =
is a tricky question indeed!<br><br>On Monday, September 12, 2016 at 11:55:=
45 AM UTC+2, Andrew Polonsky wrote:<blockquote class=3D"gmail_quote" style=
=3D"margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: =
1ex;">&gt; I suspect &quot;one of them provably has but the other doesn&#39=
;t&quot; should mean &quot;one
<br>&gt; of them provably has but the other provably does not have&quot;.
<br>
<br>Type theory with reflection rule usually contains the rule equating
<br>all proofs of equality:
<br>
<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0p : Id(A;x,y)
<br>---------------------------
<br>=C2=A0 p =3D=3D refl : Id(A;x,y)
<br>
<br>If this is admitted, then the following modified example works:
<br>
<br>A =3D Id(U;Bool,Bool)
<br>B =3D Iso(Bool,Bool)
<br>P(X) =3D Id(U;A,X)
<br>
<br>Clearly, P(A). =C2=A0Suppose P(B). =C2=A0By equality reflection, A =3D=
=3D B : U.
<br>But then, for x : Iso(Bool,Bool), we have x : Id(U;Bool,Bool), whence x=
 =3D=3D refl.
<br>Since this holds for arbitrary x, we have x=3D=3Dy for arbitrary x,y :
<br>Iso(Bool,Bool), a contradiction.
<br>
<br>Generally, I think any proof that equality reflection is inconsistent
<br>with univalence could be adapted to yield a counterexample as above.
<br>
<br>Cheers,
<br>Andrew
<br></blockquote></div>
------=_Part_8917_1388300779.1473674829001--

------=_Part_8916_923317033.1473674829001--