Univalent foundations

Very briefly, the basic idea of the univalence axiom can be explained as follows. In type theory, one can have a universe $\mathcal{U}$ , the terms of which are themselves types, $A:\mathcal{U}$ , etc. Those types that are terms of $\mathcal{U}$ are commonly called small types. Like any type, $\mathcal{U}$ has an identity type $\mathsf{Id}_{\mathcal{U}}$ , which expresses the identity relation $A=B$ between small types. Thinking of types as spaces, $\mathcal{U}$ is a space, the points of which are spaces; to understand its identity type, we must ask, what is a path $p:A\leadsto B$ between spaces in $\mathcal{U}$ ? The univalence axiom says that such paths correspond to homotopy equivalences $A\simeq B$ , (roughly) as explained above. A bit more precisely, given any (small) types $A$ and $B$ , in addition to the primitive type $\mathsf{Id}_{\mathcal{U}}(A,B)$ of identifications of $A$ with $B$ , there is the defined type $\mathsf{Equiv}(A,B)$ of equivalences from $A$ to $B$ . Since the identity map on any object is an equivalence, there is a canonical map,

\mathsf{Id}_{\mathcal{U}}(A,B)\to\mathsf{Equiv}(A,B).

The univalence axiom states that this map is itself an equivalence. At the risk of oversimplifying, we can state this succinctly as follows:

Univalence Axiom:: $(A=B)\;\simeq\;(A\simeq B)$ .

In other words, identity is equivalent to equivalence. In particular, one may say that “equivalent types are identical”. However, this phrase is somewhat misleading, since it may sound like a sort of “skeletality” condition which collapses the notion of equivalence to coincide with identity, whereas in fact univalence is about expanding the notion of identity so as to coincide with the (unchanged) notion of equivalence.

From the homotopical point of view, univalence implies that spaces of the same homotopy type are connected by a path in the universe $\mathcal{U}$ , in accord with the intuition of a classifying space for (small) spaces. From the logical point of view, however, it is a radically new idea: it says that isomorphic things can be identified! Mathematicians are of course used to identifying isomorphic structures in practice, but they generally do so by “abuse of notation”, or some other informal device, knowing that the objects involved are not “really” identical. But in this new foundational scheme, such structures can be formally identified, in the logical sense that every property or construction involving one also applies to the other. Indeed, the identification is now made explicit, and properties and constructions can be systematically transported along it. Moreover, the different ways in which such identifications may be made themselves form a structure that one can (and should!) take into account.

Thus in sum, for points $A$ and $B$ of the universe $\mathcal{U}$ (i.e., small types), the univalence axiom identifies the following three notions:

•

(logical) an identification $p:A=B$ of $A$ and $B$
•

(topological) a path $p:A\leadsto B$ from $A$ to $B$ in $\mathcal{U}$
•

(homotopical) an equivalence $p:A\simeq B$ between $A$ and $B$ .

References

Title	Univalent foundations
\metatable