### Univalence From Scratch

#### Posted by Mike Shulman

Martín Escardó has written “a self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom” in English and Agda:

The introduction says:

In introductions to the subject for a general audience of mathematicians or logicians, the univalence axiom is typically explained by handwaving. This gives rise to several misconceptions, which cannot be properly addressed in the absence of a precise definition.

Unlike most “introductions to the subject”, Martín is *not* trying to introduce homotopy type theory or univalent foundations in general; he’s just taking a geodesic route to a rigorous statement of the univalence axiom. I think this is a good supplement to the existing introductions to the subject: for someone who’s read some of those to get a “feel” for what univalence looks like, here is a fairly short and fully precise reference for *exactly* what it says (and doesn’t say).

## arXiv version

A slightly modified version is now on the arXiv – A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom.