From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Thu, 17 May 2018 23:36:44 -0700 (PDT)
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: <4f23688f-af7c-43cb-946c-988f9d476848@googlegroups.com>
Subject: Univalence <-> equivalence induction
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_6102_175721188.1526625404555"

------=_Part_6102_175721188.1526625404555
Content-Type: multipart/alternative; 
	boundary="----=_Part_6103_1953800399.1526625404555"

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

Equivalence induction says that in order to prove something for all 
equivalences, it is enough to prove it for all identity equivalences for 
all types.

This follows from univalence. But also, conversely, univalence follows from 
it:

   http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Univalence.html#JEq

Is this known? Some years ago it was claimed in this list that equivalence 
induction would be strictly weaker than univalence. 

To prove the above, I apply a technique I learned from Peter Lumsdaine, 
that given an abstract identity system (Id, refl , J) with no given 
"computation rule" for J, produces another identity system (Id, refl , J' , 
J'-comp) with
a "propositional computation rule" J'-comp for J'.

   http://www.cs.bham.ac.uk/~mhe/agda-new/Lumsdaine.html

Martin


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

<div dir=3D"ltr">Equivalence induction says that in order to prove somethin=
g for all equivalences, it is enough to prove it for all identity equivalen=
ces for all types.<div><br></div><div>This follows from univalence. But als=
o, conversely, univalence follows from it:</div><div><br></div><div>=C2=A0 =
=C2=A0http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Univalence.html#JEq<br></di=
v><div><br></div><div>Is this known? Some years ago it was claimed in this =
list that equivalence induction would be strictly weaker than univalence.=
=C2=A0</div><div><br></div><div>To prove the above, I apply a technique I l=
earned from Peter Lumsdaine, that given an abstract identity system (Id, re=
fl , J) with no given &quot;computation rule&quot; for J, produces another =
identity system (Id, refl , J&#39; , J&#39;-comp) with</div><div>a &quot;pr=
opositional computation rule&quot; J&#39;-comp for J&#39;.</div><div><br></=
div><div>=C2=A0 =C2=A0http://www.cs.bham.ac.uk/~mhe/agda-new/Lumsdaine.html=
<br></div><div><br></div><div>Martin</div><div><br></div></div>
------=_Part_6103_1953800399.1526625404555--

------=_Part_6102_175721188.1526625404555--