Univalence from scratch

["Martín Hötzel Escardó" <"escardo..."@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1349 bytes --]

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.


[-- Attachment #1.2: Type: text/html, Size: 1582 bytes --]