From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 17 Nov 2017 15:53:34 -0800 (PST)
From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?=
 <escardo...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <e15c4ebe-12b3-4069-80d7-4de9ca6ccf80@googlegroups.com>
Subject: Yet another characterization of univalence
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_38_1132474227.1510962814547"

------=_Part_38_1132474227.1510962814547
Content-Type: multipart/alternative; 
	boundary="----=_Part_39_131605669.1510962814547"

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

Consider the identity type former Id of the type X:U in the universe U:

    Id : X -> (X -> U).

I've known for some years that this is an embedding of the type X into the 
type (X->U). This means that the fibers of Id are propositions, or, 
equivalently, that the maps ap Id  : x = y -> Id x = Id y are equivalences 
for all x,y:X.

This depends on univalence. I've just realized that this is actually 
*equivalent* to univalence. Has anybody noticed this before?

Martin


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

<div dir=3D"ltr"><div>Consider the identity type former Id of the type X:U =
in the universe U:</div><div><br></div><div>=C2=A0 =C2=A0 Id : X -&gt; (X -=
&gt; U).</div><div><br></div>I&#39;ve known for some years that this is an =
embedding of the type X into the type (X-&gt;U). This means that the fibers=
 of Id are propositions, or, equivalently, that the maps ap Id=C2=A0 : x =
=3D y -&gt; Id x =3D Id y are equivalences for all x,y:X.<div><br></div><di=
v>This depends on univalence. I&#39;ve just realized that this is actually =
*equivalent* to univalence. Has anybody noticed this before?</div><div><br>=
</div><div>Martin</div><div><br></div></div>
------=_Part_39_131605669.1510962814547--

------=_Part_38_1132474227.1510962814547--