The n-Category Café

In Voevodsky’s original phrasing, the univalence axiom is an augmentation of universes, which are a type-theoretic notion that I haven’t mentioned yet. (If you don’t like universes, that’s okay; carry on reading.) At an informal level, I think type-theoretic universes are not very different from the universes of the Grothendieck sort that you may be more familiar with, and are even more closely related to their categorial analogues. In terms of categorical semantics, a universe is a type $U$, together with a display map $E\to U$ (that is, a type $E(u)$ dependent on $u\in U$). We think of the elements of $U$ as “codes for types”, with $u\in U$ coding for the type $E(u)$. And we require that the type-theoretic operations, such as dependent sums and products, are represented by operations on $U$, so that types of the form $E(u)$ are closed under such operations.

Type-theoretically, we usually identify types $E(u)$ with their codes $u\in U$, so that the elements (terms) of $U$ are types. We generally assume every type is contained in some universe, so that we can replace judgments of the form “$A$ is a type” with “$A\in U$” for some universe $U$. In particular, any universe $U=U_0$ must be an element of some universe $U_1$, which must be an element of some universe $U_2$, and so on; we often postulate that every type belongs to one of a specific sequence of universes $U_0 \in U_1\in U_2\in\dots$. Frequently a universe is written as “$Type$” or “$Type_n$”.

Thus a universe is a “type of types.” If we regard types as sets, then this is like a set of sets. But if we are category theorists, we know that it’s unnatural to have a set of sets; really we should have a category, or at least a groupoid, of sets. And we should have a 2-groupoid of groupoids, and an $(n+1)$-groupoid of $n$-groupoids, and so on. But the nice thing about $\infty$ is that $\infty = \infty+1$, so that we can expect to have an $\infty$-groupoid of $\infty$-groupoids. Thus, arguably, it’s really in the homotopy context that the notion of universe is “most sensible”.

Now it’s all well and good to say we have an $\infty$-groupoid of $\infty$-groupoids, but what is that $\infty$-groupoid? Its objects are of course $\infty$-groupoids, but we also know what its morphisms should be, and its 2-morphisms, and so on: they should be the equivalences, homotopies, and so on between $\infty$-groupoids. However, the basic type-theoretic notion of universe doesn’t tell us anything about what the path-types of the universe are like; this is what the univalence axiom fixes. (It’s analogous to how plain intensional type theory doesn’t tell us anything about when two functions should be considered equal; hence we need function extensionality.)

To make things more precise, let $A$ and $B$ be types in some universe $U$; we want to specify what $Paths_U(A,B)$ should be. And we have a natural candidate, namely the type

$$Equiv(A,B) \coloneqq \sum_{f\colon A \to B} IsEquiv(f).$$

of equivalences from $A$ to $B$. (Remember that $IsEquiv(f)$ is a proposition, so it makes sense to think of points of $Equiv(A,B)$ as functions $A\to B$ with the property of “being an equivalence.”) Moreover, we have a natural map

$$extern_{U,A,B} \colon Paths_U(A,B) \to Equiv(A,B)$$

and the univalence axiom for $U$ simply states that this map is an equivalence for any $A$ and $B$, i.e.

$$UnivalenceAxiom(U) \coloneqq \prod_{A,B\in U} IsEquiv(extern_{U,A,B}).$$

How do we define $extern_{U,A,B}$? Remember from the first post that the “elimination rule” for path-types says:

• Given a type $C(x,y,p)$ which may depend on two points $x,y\in X$ and a path $p\in Paths_X(x,y)$ between them, if we have a way to produce an element of $C(x,x,r_x)$ for any $x\in X$, then we can “transport” it along any path $p\in Path_X(x,y)$ to produce a canonical element of $C(x,y,p)$ (and in such a way that if we transport it along $r_x$ then it doesn’t change).

We’re going to apply this rule with $X=U$, $x=A$, and $y=B$. We’ll take the type $C(A,B,p)$ to be $Equiv(A,B)$, which depends on $A$ and $B$ and (vacuously) a path between them. Now we do have a way to produce an element of $C(A,A,r_A) = Equiv(A,A)$, namely the identity function $1_A\colon A\to A$ (which is an equivalence; I’ll leave proving that as an exercise). Therefore, we can transport the identity $1_A$ along any path $p\in Paths_U(A,B)$ to produce a canonical element of $Equiv(A,B)$ corresponding to $p$. This defines the map $extern_{U,A,B}$.

Let’s think first about the semantics of univalence. First of all, in the form I stated it above, it is an axiom about a particular universe $U$. A universe satisfying the univalence axiom is called a univalent universe. We generally assume that all of the specified universes $U_0 \in U_1\in U_2\in\dots$ are univalent.

In the “standard” model in $\infty$-groupoids, we obtain a univalent universe from “the $\infty$-groupoid of all $\infty$-groupoids bounded in size by some inaccessible cardinal $\kappa$”. Thus, if there are arbitrarily large inaccessibles, every type will belong to some univalent universe. (I’m not sure whether inaccessibles are necessary here or whether some weaker assumption would suffice.) I believe this is the only model with enough univalent universes that has been constructed in set theory with anything approaching rigor (by Voevodsky).

However, I think most people expect that in more general $(\infty,1)$-categorical semantics, we ought to obtain a univalent universe from any object classifier with strong enough closure properties. In particular, in any (Grothendieck) $(\infty,1)$-topos, there ought to be a univalent universe of all “$\kappa$-compact” types, for any inaccessible $\kappa$.

Moreover, any “full subuniverse” of a univalent universe will again be a univalent universe, as long as it is closed under the type-theoretic operations. In particular, if $U$ is any univalent universe, then its full subuniverse of $n$-types is again univalent for any $n$, and that subuniverse will itself be an $(n+1)$-type. Thus a univalent universe need not itself be of infinite h-level: we can have a univalent groupoid (1-type) of small sets (0-types), a univalent 2-groupoid (2-type) of small groupoids, and so on. At the bottom, we can have a univalent set (0-type) of small truth values ((-1)-types).

In particular, a subobject classifier, if one exists, is also a univalent universe; so to get ourselves out of the world of sets we need at least two univalent universes. Similarly, we can have a sequence of univalent universes $U_0 \in U_1\in U_2\in\dots$ in which $U_0$ contains only (-1)-types and is itself a 0-type, $U_1$ contains only 0-types and is itself a 1-type, and so on. Such a stratification of universes by “categorical dimension” as well as by size does seem to match much of mathematical practice—but only outside of homotopy theory. For homotopy theory, we do really want to have $\infty$-types that aren’t $n$-types for any finite $n$ (such as, for instance, the 2-sphere $S^2$), and an infinite sequence of univalent universes doesn’t seem to be enough to guarantee this. I’ll come back to this later.

Vladimir explained the origin of the word “univalent” as follows:

• a universal fibration is one of which every other fibration is a pullback in a unique way (up to homotopy).
• a versal fibration is one of which every other fibration is a pullback in some way, not necessarily unique.
• a univalent fibration is one of which every other fibration is a pullback in at most one way (up to homotopy).

Thus the univalence axiom asserts that the structural fibration of the universe is univalent.

Now, the principal way we use the univalence axiom is as follows: given an equivalence $f\colon A \to B$, we apply the inverse of $extern_{U,A,B}$ to get a path $\hat{f}\in Paths_U(A,B)$, then apply the above-mentioned “elimination rule” for elements of path-types. Putting this together, we get the following consequence of univalence, apparently first formulated by Peter Lumsdaine and Andrej Bauer.

• Given a type $C(A,B,f)$ which may depend on two types $A,B$ and an equivalence $f\colon A\to B$ between them, if we have a way to produce an element of $C(A,A,1_x)$ for any type $A$, then we can “transport” it along any equivalence $f\colon A\to B$ to produce a canonical element of $C(A,B,f)$ (and in such a way that if we transport it along $1_A$ then it doesn’t change).

The elimination rule for paths is sometimes called path induction, since it is an instance of the general induction principle for inductively defined types. By analogy, we refer to the above consequence of univalence as equivalence induction. Informally, it means that

• Given an equivalence $f\colon A\to B$, we can “identify” $B$ with $A$ along $f$. Specifically, in any construction we can perform, or theorem we can prove, starting only from a type $A$, we can obtain another valid construction or theorem by replacing some copies of $A$ with $B$ and any necessary occurrences of $1_A$ by $f$. Behind the scenes, this replacement uses $f$ and its inverse to silently transfer data back and forth between $A$ and $B$ as necessary.

Such “identification” of course a very common thing to do in mathematics, often without even remarking on it! But usually, if it is justified at all, it is “by abuse of notation” or by trusting the reader to do the translation. The univalence axiom formalizes it, makes it happen “automatically” in the background, and makes it “natural/continuous.”

Moreover, equivalence induction actually implies the full univalence axiom. For if we apply equivalence induction to the type $C(A,B,f) \coloneqq Paths_U(A,B)$ and the identity path $r_A\in Paths_U(A,A)$, we obtain a way to make any equivalence $f\colon A\to B$ into a path $\hat{f}\in Paths_U(A,B)$. The final condition that transporting along the identity equivalence leaves something unchanged (together with the same property for the identity path) then makes this construction into an inverse of $extern_{U,A,B}$. I’ve checked this in Coq. But it’s not really surprising, because equivalence induction gives the type $Equiv(A,B)$ the “same inductive/universal property” as $Paths_U(A,B)$. (But I don’t know how to state equivalence induction in a way that is evidently a proposition.)

Note that equivalence induction makes no reference to a particular universe containing $A$ and $B$, except that the type $C(A,B,f)$ is required to be defined “parametrically” for all $A,B$ in the universe. In particular, this implies that if $U_1$ is a univalent universe and $U_2$ is a “larger” universe, in the sense that every type in $U_1$ also belongs to $U_2$, then $extern_{U_2,A,B}$ is also an equivalence for any $A,B\in U_1$, whether or not $U_2$ itself is univalent. (It can apparently still be the case that a “smaller” non-univalent universe is contained in a “larger” univalent one, however.) So univalence is almost a property of types (or pairs of types) rather than a property of universes. Furthermore, we can make sense of equivalence induction even if there are no universes, if instead we have some sort of “polymorphism” allowing us to make sense of “defining a type parametrically over other types”. (Thanks to Peter Lumsdaine for correcting some errors in the original version of this paragraph; see his comment and ensuing discussion below.)

Univalence also implies other useful things, like function extensionality and (maybe, with some help) quotients, but let’s save those for another day.