# What is the most transparent, rigorous definition of the Univalence Axiom?

I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers that present the "flavor" of Univalence (i.e. "identity is equivalent to equivalence") but only informally. Obviously the HoTT book has a rigorous definition but it is substantial work getting there, at least to someone new to type theory.

Can anyone give a reference to a paper that develops the minimal amount of machinery to provide a formal definition of the Univalence Axiom?

• You really must understand type theory first – at minimum the notion of identity types. I think it would be enough to read Chapter 1 of the HoTT book, then skip to §2.10. – Zhen Lin Jun 30 '15 at 19:03
• You need at least §2.4 too, for the definition of "equivalence". – Mike Shulman Jul 1 '15 at 3:39
• I think it would help if we knew more about your background. For example, if you are already proficient with model categories (or really, if you just know fibrations very well) then I think there are explanations of the axiom which are more down-to-earth. – David White Jul 1 '15 at 5:33
• Background: Set theory, model theory, homotopy via algebraic topology all at grad level. Fundamental category theory but not specialist. I do not yet know model categories or simplicial sets, though I've glanced at these due to my HoTT investigations. Hope this helps and thanks for any insights! – antianticamper Jul 1 '15 at 17:08

I’ll give first a simplicial definition of univalence, and then a type-theoretic one, and discuss the equivalence between them as we go.

The first thing to know is that univalence is a property that can be defined for any family of types, or in models, for any fibration. The Univalence Axiom then says that a particular family of types — a “universe” — is univalent. I’ll come back to the universe at the end.

So: what is univalence for a fibration? Roughly, a fibration is univalent just when the map from “paths in the base” to “equivalences between fibers” is itself an equivalence.

Precisely: given two fibrations $Y_1, Y_2$ over a common base $X$, write $\newcommand{\Hom}{\mathcal{Hom}}\Hom_X(Y_1,Y_2)$ for the fibred mapping space between them, i.e. the exponential in $\newcommand{\SSet}{\mathbf{SSet}}\SSet/X$, which represents maps between (pullbacks of) $Y_1$ and $Y_2$, and write $\newcommand{\Eqv}{\mathcal{Eqv}}\Eqv_X(Y_1,Y_2)$ for the subobject of $\Hom_X(Y_1,Y_2)$ that represents equivalences between them. So an $n$-simplex of $\Eqv(Y_1,Y_2)$ over a simplex $x \in X_n$ corresponds to an equivalence of fibers $(Y_1)_x \to (Y_2)_x$ over $\Delta[n]$.

Now, given a single fibration $Y$ over $X$, we can consider maps between different fibers of $Y$ by first pulling it back to $X \times X$ along the two projections $\pi_1$, $\pi_2$. So $\pi_1^*(Y)_{(x_1,x_2)} \cong Y_{x_1}$, and $\pi_2^*(Y)_{(x_1,x_2)} \cong Y_{x_2}$. Now consider the fibred space of equivalences between these: $\Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$. So an element of this over $(x_1,x_2)$ represents an equivalence $Y_{x_1} \to Y_{x_2}$ between fibers of $Y$.

There’s always a map $i : X \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$, living over the diagonal $\Delta_X : X \to X \times X$, where $i(x)$ represents the identity map $Y_x \to Y_x$. Then we define: the fibration $Y \to X$ is univalent if this map $i : X \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ is a weak equivalence.

Some easily equivalent forms:

• (in $\SSet$, or anywhere else where cof = mono) $i$ is a trivial cofibration;
• $i$ makes $\Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ a path object for $X$;
• the induced map $P(X) \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ over $X \times X$ is an equivalence (for any other path object $P(X)$).

A slightly-less-trivially equivalent form is the same statement, but using an alternative construction of the object of equivalences — call it $\Eqv'_X(Y_1,Y_2)$ — which represents not just “equivalences from $Y_1$ to $Y_2$”, but “maps $f$ from $Y_1$ to $Y_2$, equipped with a homotopy left inverse $(g_l, \alpha)$ (where $\alpha$ is the homotopy $g_l \cdot f \to 1_{Y_1}$) and a homotopy right inverse $(g_r,\beta)$”. This is equivalent to the other versions just since the evident projection $\Eqv'(Y_1,Y_2) \to \Eqv(Y_1,Y_2)$ is always a trivial fibration.

Now let’s move to type theory. First a couple of notes about language. It’s familiar in homotopy theory to think of a fibration as a family of spaces varying over a base space. In type theory, this is literally the case in the language — you work with a family of types indexed by a variable varying over a base type, just like in traditional settings you work with the family of sets $\newcommand{\R}{\mathbb{R}}\newcommand{\N}{\mathbb{N}}\R^n$ indexed by $n \in \N$ — but such a family will generally behave like a fibration, not just like a discretely indexed family of discrete sets. And in the simplicial model (and other similar models), a family of types gets interpreted as a fibration.

Also, like the HoTT book, I’ll work in prose, not in formal symbolic type theory, just like how when one does maths over a traditional foundation, one writes in prose rather than the formal symbols of first-order set theory. (In fact the gap between prose and formal language is significantly smaller in type theory than in set-theoretic foundations, for most mathematics.)

The only basic notions we need are path types, function types, and $\Sigma$-types (types of tuples of data).

Given two types $Y_1$, $Y_2$, we can define the type $\newcommand{\tyEqv}{\mathsf{Eqv}}\tyEqv(Y_1,Y_2)$ of equivalences between them as the type of tuples $(f,g_l,\alpha,g_r,\beta)$, where $f$ is a function $Y_1 \to Y_2$, $g_l$ is a function back the other way, $\alpha$ is a function giving for each $y \in Y_1$ a path from $g_l(f(y))$ to $y$ (so $(g_l,\alpha)$ together are a homotopy left inverse for $f$), and similarly $(g_r,\beta)$ is a homotopy right inverse. Saying a function $f : Y_1 \to Y_2$ is an equivalence means equipping it with suitable $(g_l,\alpha,g_r,\beta)$.

In general, $Y_1$ and $Y_2$ may have been dependent all along on some variable(s) — say, $Y_1(x)$ and $Y_2(x)$, where $x$ ranges over some other type $X$. Then their interpretations in the simplicial model will be fibrations $[Y_i] \to [X]$; and $\tyEqv(Y_1(x),Y_2(x))$ is itself dependent on $x : X$, so its interpretation is also a fibration $[\tyEqv(Y_1,Y_2)] \to [X]$. And in fact this comes out to be precisely $\Eqv'([Y_1],[Y_2])$ as defined above, since path-types are modelled by (fibred) path-objects and function types by (fibred) mapping objects.

Now for a type $Y(x)$ depending on $x:X$, and for any $x_1,x_2 : X$, there’s a canonical map $\newcommand{\tyP}{\mathsf{P}}i : \tyP_X(x_1,x_2) \to \tyEqv(Y(x_1),Y(x_2))$, defined by giving the identity equivalence $Y(x) \to Y(x)$ on reflexivity paths. (To construct something depending on a general path, it’s enough to construct it for reflexivity paths; this is the defining property of path-types, and is analogous to extending maps defined on $X$ to maps defined on a path-object $P(X)$ along the inclusion $X \to P(X)$.)

Now, say that a family of types $Y(x)$, indexed by $x : X$, is univalent if this map $i : \tyP_X(x_1,x_2) \to \tyEqv(Y(x_1),Y(x_2))$ is an equivalence for each $x_1,x_2 : X$.

I hope the remarks so far about interpretation make it reasonably plausible, if not quite watertight, why a family of types is univalent in this sense just if its interpretation as a fibration is univalent in the simplicial sense.

Now, in type theory (as in other foundations), one often wants to consider a universe — a family of types closed under common constructions (e.g. forming function types). Indeed, one may consider multiple such universes. The Univalence Axiom, for a given universe, says just that this universe, considered just as a family of types, is univalent.

I’ll stop here, because this is plenty long enough already! But a full treatment of all the above, together with the construction of univalent universes in $\SSet$, can be found in The Simplicial Model of Univalent Foundations (Kapulkin, Lumsdaine, Voevodsky). Specifically, it’s in Section 3, using the universe introduced in in Section 2; you can probably comfortably skip Section 1, which is about the technicalities of constructing models of type theory, and also most of Section 2 after the universe is constructed.

• Very nice answer. I would have simply added the beautiful slogan $(A=B) \approx (A\approx B)$ :). – AFK Mar 10 '18 at 13:25