From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Wed, 7 Mar 2018 13:10:53 -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: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com>
Subject: Univalence from scratch
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_2_116165467.1520457053924"

------=_Part_2_116165467.1520457053924
Content-Type: multipart/alternative; 
	boundary="----=_Part_3_1821685984.1520457053924"

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

I have often seen competent mathematicians and logicians, outside our 
circle, making technically erroneous comments about the univalence axiom, 
in conversations, in talks, and even in public material, in journals or the 
web. 

For some time I was a bit upset about this. But maybe this is our fault, by 
often trying to explain univalence only imprecisely, mixing the explanation 
of the models with the explanation of the underlying theory (MLTT, identity 
types, universe), with none of the two explained sufficiently precisely. 

There are long, precise explanations such as the HoTT book, for example, 
or, the formalizations in Coq, Agda and Lean.

But perhaps we don't have publicly available material with a 
self-contained, brief and complete formulation of univalence, so that 
interested mathematicians and logicians can try to contemplate the axiom in 
a fully defined form.

Here is an attempt to rectify this:

  https://arxiv.org/abs/1803.02294

This also has an ancillary Agda file with univalence defined from scratch 
(without the use of any library at all). Perhaps somebody should add a Coq 
"version from scratch" of this. 

There is also a web version of this 
(http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html) to try 
to make this as accessible as possible, with the text and the Agda code 
together.

M.


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

<div dir=3D"ltr">I have often seen competent mathematicians and logicians, =
outside our circle, making technically erroneous comments about the univale=
nce axiom, in conversations, in talks, and even in public material, in jour=
nals or the web.=C2=A0<div><br></div><div>For some time I was a bit upset a=
bout this. But maybe this is our fault, by often trying to explain univalen=
ce only imprecisely, mixing the explanation of the models with the explanat=
ion of the underlying theory (MLTT, identity types, universe), with none of=
 the two explained sufficiently precisely.=C2=A0</div><div><br></div><div>T=
here are long, precise explanations such as the HoTT book, for example, or,=
 the formalizations in Coq, Agda and Lean.</div><div><br></div><div>But per=
haps we don&#39;t have publicly available material with a self-contained, b=
rief and complete formulation of univalence, so that interested mathematici=
ans and logicians can try to contemplate the axiom in a fully defined form.=
</div><div><br></div><div>Here is an attempt to rectify this:<div><br></div=
><div>=C2=A0 https://arxiv.org/abs/1803.02294<br></div><div><br></div><div>=
This also has an ancillary Agda file with univalence defined from scratch (=
without the use of any library at all). Perhaps somebody should add a Coq &=
quot;version from scratch&quot; of this.=C2=A0</div><div><br></div><div>The=
re is also a web version of this (http://www.cs.bham.ac.uk/~mhe/agda-new/Un=
ivalenceFromScratch.html) to try to make this as accessible as possible, wi=
th the text and the Agda code together.</div><div><br></div><div>M.</div><d=
iv><br></div></div></div>
------=_Part_3_1821685984.1520457053924--

------=_Part_2_116165467.1520457053924--