Could $\infty$-Category Theory Be Taught to Undergraduates?

1. The Algebra of Paths

It is natural to probe a suitably nice topological space $X$ by means of its paths, the continuous functions from the standard unit interval $I\coloneq [0,1] \subset \mathbb{R}$ to $X$. But what structure do the paths in $X$ form?

To start, the paths form the edges of a directed graph whose vertices are the points of $X$: a path $p \colon I \to X$ defines an arrow from the point $p(0)$ to the point $p(1)$. Moreover, this graph is reflexive, with the constant path $\mathrm{refl}_x$ at each point $x \in X$ defining a distinguished endoarrow.

Can this reflexive directed graph be given the structure of a category? To do so, it is natural to define the composite of a path $p$ from $x$ to $y$ and a path $q$ from $y$ to $z$ by gluing together these continuous maps—i.e., by concatenating the paths—and then by reparametrizing via the homeomorphism $I \cong I \cup _{1=0} I$ that traverses each path at double speed:

$$\begin{equation} \vcenter{\img[][111pt][35pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} I \arrow[r, "\cong"] \arrow[rr, bend right, "p \ast q"'] & I \cup_{1=0} I \arrow[r, "p \cup q"] & X \end{tikzcd}}]{Images/img9b7a0ac0a8b3ca8a74ea3f7f70c30743.svg}} {\tag{1.1}} \end{equation}$$

But the composition operation $\ast$ fails to be associative or unital. In general, given a path $r$ from $z$ to $w$, the composites $(p \ast q) \ast r$ and $p \ast (q \ast r)$ are not equal: while the have the same image in $X$, their parametrizations differ. However, they are based homotopic, in the sense that there exists a continuous function $h \colon I \times I \to X$ so that

$$\begin{gather*} h(-,0) \coloneq (p \ast q) \ast r, \quad h(-,1) \coloneq p \ast (q \ast r), \\ h(0,-) \coloneq \mathrm{refl}_{x}, \quad \text{and} \quad h(1,-) \coloneq \mathrm{refl}_{w}, \end{gather*}$$

a situation we summarize by writing $(p \ast q) \ast r \simeq p \ast (q \ast r)$. Similarly, the paths $p \ast \mathrm{refl}_y \simeq \mathrm{refl}_x \ast p \simeq p$ are all based homotopic, though not equal (unless $p$ is the constant path).

Paths are also invertible up to based homotopy: for any path $p \colon I \to X$ from $x$ to $y$, its reversal $p^{-1} \colon I \to X$, defined by precomposing with the flipping automorphism $I \cong I$, defines an inverse up to based homotopy: $p \ast p^{-1} \simeq \mathrm{refl}_x$ and $p^{-1}\ast p \simeq \mathrm{refl}_y$. These observations motivate the following definition:

Definition 1.2.

For a space $X$, the fundamental groupoid $\pi _1X$ is the category whose:

•

objects are the points of $X$ and

•

arrows are based homotopy classes of paths of $X$

with composition defined by concatenation, identity arrows defined by the constant paths, and inverses defined by reversing paths.

The fundamental groupoid of a space $X$ answers a slightly different question than originally posed, describing the structure formed by the based homotopy classes of paths in $X$. The paths themselves form something like a weak groupoid where composition is not uniquely defined. Indeed, given paths $p$ from $x$ to $y$ and $q$ from $y$ to $z$, the composite in $\pi _1X$ is represented by any path $s$ so that there is a based homotopy $h$ witnessing $p \ast q \simeq s$. Here, the based homotopy $h$ defines a continuous function from the solid 2-simplex into $X$ that restricts along the boundary triangle to the map defined by gluing the three paths:

$$\begin{equation*} \vcenter{\img[][56pt][48pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} \partial\Delta^2 \arrow[r, "{(p,q,s)}"] \arrow[d, hook] & X \\ \Delta^2 \arrow[ur, "h"'] \end{tikzcd}}]{Images/imgc27e03aa5d34cc25563771f70700abe1.svg}} \end{equation*}$$

While multivalued composition operations are not well-behaved in general, this one has a certain homotopical uniqueness property: the witnessing homotopies for two such composites can be glued together—by a higher-dimensional analogue of the construction 1.1—to define a homotopy $s \simeq p \ast q \simeq t$. This suggests that the witnessing homotopies that fill the triangles formed by the paths between $x$ and $y$ and $z$ might be productively regarded as part of the composition data. Thus, the moduli space of composites of $p$ and $q$ is defined as follows:

Definition 1.3.

Given composable paths $p$ and $q$ in a space $X$, the space of composites of $p$ and $q$ is the subspace $\mathrm{Comp}(p,q) \subset \mathrm{Map}(\Delta ^2,X)$ of continuous maps $h \colon \Delta ^2 \to X$ that restrict on the boundary horn to $p \cup q$:

$$\begin{equation} \vcenter{\img[][151pt][47pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} \Comp(p,q) \arrow[r, hook] \arrow[d] \arrow[dr, phantom, "\lrcorner" very near start] & \Map(\Delta^2,X) \arrow[d, "\res"] \\ \ast\arrow[r, "{p \cup q}"] & \Map(I\cup_{1=0} I,X) \end{tikzcd}}]{Images/img1b18da68bd2a5aa416d8c88b90a20269.svg}} {\tag{1.4}} \end{equation}$$

The homotopical uniqueness of path composition can be strengthened by the following observation:

Theorem 1.5.

For any composable paths $p$ and $q$ in a space $X$, the space of composites $\mathrm{Comp}(p,q)$ is contractible.

So what do the paths in $X$ form? We have seen that they form a weak groupoid with a multivalued but homotopically unique composition law. In fact, this weak category is an infinite-dimensional category. The based homotopies $h \colon I \times I \to X$ between parallel paths $s$ and $t$ themselves might be regarded as paths $h \colon I \to \mathrm{Map}(I,X)$ between points $s$ and $t$ in the space $\mathrm{Map}(I,X)$ to which Theorem 1.5 equally applies, and these observations extend iteratively to higher-dimensional homotopies. The points, paths, and higher paths in a space $X$ assemble into a weak infinite-dimensional category—with interacting weak composition and identities for paths at all levels⁠¹—in which all morphisms are weakly invertible. Such a structure is known as an $\infty$-groupoid.

¹

Famously, the definition of a weak 3-dimensional category by Gordon, Power, and Street takes six pages to state.

✖

The homotopy hypothesis

The fundamental $\infty$-groupoid $\pi _\infty X$ of paths in $X$ captures the data of all of the higher homotopy groups of the space, information which is referred to as the homotopy type of the space. In a famous letter to Quillen G, Grothendieck formulated his homotopy hypothesis, positing that the fundamental $\infty$-groupoid construction defines an equivalence between homotopy types and $\infty$-groupoids. Grothendieck’s vision was that this result should be provable for various models of $\infty$-groupoids that were then under development, though some instead use this thesis to define an $\infty$-groupoid to be a homotopy type.

There is something unsatisfying, though, about the naïve interpretation of the homotopy hypothesis as the assertion of a bijection between the collection of homotopy types and the collection of $\infty$-groupoids, or even as an equivalence between the homotopy category of spaces⁠² and the homotopy category of $\infty$-groupoids. The disappointment lies in the fact that both spaces and $\infty$-groupoids live most naturally as the objects in weak infinite-dimensional categories, with the standard morphisms between them supplemented by higher-dimensional weakly invertible morphisms. Thus, a more robust expression of the homotopy hypothesis is the assertion that the $\infty$-categories of spaces and of $\infty$-groupoids are equivalent,⁠³ so now we must explain what $\infty$-categories are.

²

Homotopy types can be understood as isomorphism classes of objects in the homotopy category of spaces, the category obtained by localizing the category of spaces and continuous functions by the weak homotopy equivalences, those functions that induce isomorphisms on all homotopy groups.

✖

³

In fact, a version of this result had been proven already by Quillen for the Kan complex model of $\infty$-groupoids Q, but this was not so clearly understood at the time.

✖

2. $\infty$-Categories in Mathematics

Over the past few decades, $\infty$-categories—weak infinite-dimensional categories with weakly invertible morphisms above dimension one—have been invading certain areas of mathematics. In derived algebraic geometry, the derived category of a ring is now understood as the 1-categorical quotient of the $\infty$-category of chain complexes, and an $\infty$-categorical property called “stability” explains the triangulated structure borne by the derived category. In mathematical physics, Atiyah’s topological quantum field theories have been “extended up” to define functors between $\infty$-categories.⁠⁴ $\infty$-categories have also made appearances in the Langlands program in representation theory and in symplectic geometry among other areas. Quillen’s model categories Q from abstract homotopy theory are now understood as presentations of $\infty$-categories.

⁴

Lurie’s “fully extended” topological quantum field theories are also “extended down” so that they might be understood as functors between $(\infty ,n)$-categories, with non-invertible morphisms up to and including the dimension $n$ of the indexing cobordisms. Here we reserve the term “$\infty$-categories” for “$(\infty ,1)$-categories,” which have non-invertible morphisms only in the bottom dimension.

✖

Ordinary categories “frame a template for a mathematical theory,” with the objects providing the “nouns” and the morphisms the “verbs,” in a metaphor suggested by Mazur. As the objects mathematicians study increase in complexity, a more robust linguistic template may be required to adequately describe their natural habitats—with adjectives, adverbs, pronouns, prepositions, conjunctions, interjections, and so on—leading to the idea of an $\infty$-category. Like an ordinary 1-category, an $\infty$-category has objects and morphisms, now thought of as “1-dimensional” transformations. The extra linguistic color is provided by higher-dimensional invertible morphisms between morphisms—such as chain homotopies or diffeomorphisms—and higher morphisms between these morphisms, continuing all the way up.

How might a researcher in one of these areas go about learning this new technology of $\infty$-categories? And how might $\infty$-category theory ultimately be distilled down into something that we could reasonably teach advanced undergraduates of the future?

Curiosities from the literature

$\infty$-categories were first introduced by Boardman and Vogt to describe the composition structure of homotopy coherent natural transformations between homotopy coherent diagrams BV. Joyal was the first to assert that “most concepts and results of category theory can be extended to [$\infty$-categories]” and pioneered the development of $\infty$-categorical analogues of standard categorical notions J. Lurie then developed various aspects of $\infty$-category theory that were needed for his thesis on derived algebraic geometry L1. His books L2L3 and the online textbook Kerodon are primary references for uses of this technology, while texts written by Cisinski, Groth, Hinich, Rezk, and others provide parallel introductions to the field.

If one delves further into the $\infty$-categories literature, some curiosities soon become apparent:

(i)

Particularly in talks or lecture series introducing the subject, the definition of $\infty$-category is frequently delayed, and when definitions are given, they don’t always agree.

These competing definitions are referred to as models of $\infty$-categories, which are Bourbaki-style mathematical structures defined in terms of sets and functions that represent infinite-dimensional categories with a weak composition law in which all morphisms above dimension one are weakly invertible. In order of appearance, these include simplicial categories, quasi-categories, relative categories, Segal categories, complete Segal spaces, and 1-complicial sets, each of which comes with an associated array of naturally occurring examples Be.

(ii)

Considerable work has gone into defining the key notions for and proving the fundamental results about $\infty$-categories, but sometimes this work is later redeveloped starting from a different model.

For instance, KV begins:

In recent years $\infty$-categories or, more formally, $(\infty$,1)-categories appear in various areas of mathematics. For example, they became a necessary ingredient in the geometric Langlands problem. In his books L2L3 Lurie developed a theory of $\infty$-categories in the language of quasi-categories and extended many results of the ordinary category theory to this setting.

In his work R1 Rezk introduced another model of $\infty$-categories, which he called complete Segal spaces. This model has certain advantages. For example, it has a generalization to $(\infty ,n)$-categories (see R2).

It is natural to extend results of the ordinary category theory to the setting of complete Segal spaces. In this note we do this for the Yoneda lemma.

(iii)

Alternatively, authors decline to pick a model at all and instead work “model-independently.”

One instance of this appears in the precursor L1 to L2, which avoids selecting a model of $\infty$-categories at all:

We will begin in §1 with an informal review of the theory of $\infty$-categories. There are many approaches to the foundation of this subject, each having its own particular merits and demerits. Rather than single out one of those foundations here, we shall attempt to explain the ideas involved and how to work with them. The hope is that this will render this paper readable to a wider audience, while experts will be able to fill in the details missing from our exposition in whatever framework they happen to prefer.

The fundamental obstacle to giving a uniform definition of an $\infty$-category is that our traditional set-based foundations for mathematics are not really suitable for reasoning about $\infty$-categories: sets do not feature prominently in $\infty$-categorical data, especially when $\infty$-categories are only well-defined up to equivalence, as they must be when different models are involved. When considered up to equivalence, $\infty$-categories, like ordinary categories, do not have a well-defined set of objects. Essentially, $\infty$-categories are 1-categories in which all the sets have been replaced by $\infty$-groupoids. Where a category has a set of elements, an $\infty$-category has an $\infty$-groupoid of elements, and where a category has hom-sets of morphisms, $\infty$-categories have $\infty$-groupoidal mapping spaces.⁠⁵ The axioms that turn a directed graph into a category are expressed in the language of set theory: a category has a composition function satisfying axioms expressed in first-order logic with equality. By analogy, composition in an $\infty$-category can be understood as a morphism between $\infty$-groupoids, but such morphisms no longer define functions since homotopy types do not have underlying sets of points.⁠⁶ This is why there is no canonical model of $\infty$-categories.

⁵

“Large” $\infty$-categories also exist and behave like large 1-categories.

✖

⁶

Similar considerations have motivated Scholze et al to use the term “anima”—referring to the “soul” of a “space”—as a synonym for $\infty$-groupoids.

✖

Reimagining the foundations of $\infty$-category theory

Despite these subtleties, it is possible to reason rigorously and model-independently about $\infty$-categories without getting bogged down in the combinatorial scaffolding of a particular model. The framework introduced in §3 considerably streamlines the basic core theory of $\infty$-categories, though its scope is currently more limited than the corpus of results that have been proven using a model.

However, this current state of the art employs proof techniques that are unfamiliar to non-category theorists and thus is not feasible to integrate into the undergraduate curriculum. The concluding §4 describes a more speculative dream for the future where enhancements to the foundations of mathematics would allow us to interpret uniqueness as contractibility and automatically ensure that all constructions are invariant under equivalence.

3. The Formal Theory of $\infty$-Categories

In the paper “General theory of natural equivalences” that marked the birth of category theory, Eilenberg and Mac Lane observed that categories, functors, and natural transformations assemble into a 2-category $\mathsf{CAT}$. The essence of this result is the observation that natural transformations can be composed in 2-dimensions’ worth of ways: “vertically” along a boundary functor or “horizontally” along a boundary category.

More generally, Power proves that any pasting diagram of compatibly oriented functors and natural transformations has a unique composite.

$$\begin{equation*} \vcenter{\img[][188pt][84pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd}[sep=small] & \arrow[ddr, phantom, "\scriptstyle\Downarrow\beta"] & & D \arrow[drr, "p"] \\ A \arrow[ddr, "f"'] \arrow[drr, "g" description] \arrow[urrr, "h"] & & & & & E \arrow[drr, "r"] \arrow[ddr, "q" description] & \arrow[dd, phantom, "\scriptstyle\Downarrow\epsilon"] \\ \arrow[rr, phantom, "\scriptstyle\Downarrow\alpha"] & & C \arrow[uur, "\ell" description] \arrow[urrr, "m" description] \arrow[rrrr, phantom, "\scriptstyle\Downarrow\delta"] & \arrow[uu, phantom, "\scriptstyle\Downarrow\gamma"] & &~ & ~& G \\ & B \arrow[ur, "j" description, pos=.4] \arrow[rrrrr, "k"'] & & & & & F \arrow[ur, "s"'] \end{tikzcd}}]{Images/img5b0a1aca32c7f0eb6426241f235d8f95.svg}} \end{equation*}$$

The pasting composite, which in the example above defines a natural transformation between the categories $A$ and $G$ from the functor $rph$ to the functor $skf$, can be decomposed as a vertical composite of whiskerings of the atomic natural transformations $\alpha , \beta , \gamma ,\delta ,\epsilon$: for instance, the composite factors as $rp\beta$ followed by $r\gamma g$ followed by $\epsilon mg$ followed by $sqm\alpha$ followed by $s\delta f$, among eight total possibilities. Power’s theorem is that pasting composition is well-defined.

Similarly, in well-behaved models of $\infty$-categories:

Proposition 3.1 (Joyal, Riehl–Verity).

$\infty$-categories, $\infty$-functors, and $\infty$-natural transformations assemble into a cartesian closed 2-category $\infty \text{-}\mathsf{CAT}$.

This result was first observed in the quasi-category model by Joyal J. Since the category of quasi-categories is cartesian closed, it is enriched over itself, defining an $(\infty ,2)$-category of quasi-categories. The 2-category of quasi-categories is obtained by a quotienting process, that maps each hom-quasi-category to its homotopy category, by applying the left adjoint to the (nerve) inclusion of categories into quasi-categories. The other “well-behaved” models—including complete Segal spaces, Segal categories, and 1-complicial sets among others—are also cartesian closed, so a similar construction defines a 2-category of complete Segal spaces, and so on.⁠⁷ To adopt a “model-independent” point of view, note that these 2-categories are all biequivalent or “the same” in the sense appropriate to 2-category theory RV2, §E.2.

⁷

While the meaning of the terms “$\infty$-categories” and “$\infty$-functors” in a given model is typically clear, the “$\infty$-natural transformations,” which can be understood as equivalence classes of 2-cells in the ambient $(\infty ,2)$-category, are less evident.

✖

The good news, which is surprising to many experts, is that a fair portion of the basic theory of $\infty$-categories can be developed in the 2-category $\infty \text{-}\mathsf{CAT}$. These aspects might be described as formal category theory, as they involve definitions of categorical notions such as equivalence, adjunction, limit, and colimit that can be defined internally to any 2-category. In the 2-category $\mathsf{CAT}$, these recover the classical notions from 1-category theory, while in the 2-category $\infty \text{-}\mathsf{CAT}$ these specialize to the correct notions in $\infty$-category theory.⁠⁸ Thus, for the core basic theory involving these notions, ordinary category theory extends to $\infty$-categories simply by appending the prefix “$\infty -$” RV2, §2-4.

⁸

The technical part of this story involves proofs that the “synthetic” or “formal” notions introduced here agree with the previously-defined “analytic” notions in the quasi-categories model RV2, §F. But we encourage those not already acquainted with the analytic theory of some model of $\infty$-categories to learn these definitions first.

✖

Equivalences and adjunctions

The following definitions make sense in an arbitrary cartesian closed 2-category, such as $\infty \text{-}\mathsf{CAT}$.

Definition 3.2.

An equivalence between $\infty$-categories is given by:

•

a pair of $\infty$-categories $A$ and $B$,

•

a pair of $\infty$-functors $g \colon A \to B$ and $h \colon B \to A$, and

•

a pair of invertible $\infty$-natural transformations $\alpha \colon \mathrm{id}_A \cong h g$, and $\beta \colon g h \cong \mathrm{id}_B$.

Definition 3.3.

An adjunction between $\infty$-categories is given by:

•

a pair of $\infty$-categories $A$ and $B$,

•

a pair of $\infty$-functors $u \colon A \to B$ and $f \colon B \to A$, and

•

a pair of $\infty$-natural transformations $\eta \colon \mathrm{id}_B \Rightarrow uf$ and $\epsilon \colon fu \Rightarrow \mathrm{id}_A$

so that the following pasting identities hold:

$$\begin{equation*} \vcenter{\img[][297pt][40pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd}[column sep=1.5em] B \arrow[dr, "f"'] \arrow[rr, equals] & \arrow[d, phantom, "\scriptstyle\Downarrow\eta"] & B \arrow[dr, "f"] \arrow[d, phantom, "\scriptstyle\Downarrow\epsilon"] & & B \arrow[d, bend left, "f"] \arrow[d, bend right, "f"'] \arrow[d, phantom, "="] & & B \arrow[d, phantom, "\scriptstyle\Downarrow\epsilon"] \arrow[rr, equals] \arrow[dr, "f" description] &\arrow[d, phantom, "\scriptstyle\Downarrow\eta"] & B \arrow[dr, phantom, "=\quad"] & B \\ & A \arrow[ur, "u" description] \arrow[rr, equals] & ~& A \arrow[ur, phantom, "=\quad"] & A & A \arrow[ur, "u"] \arrow[rr, equals] & ~& A \arrow[ur, "u"'] & & A \arrow[u, bend left, "u"] \arrow[u, bend right, "u"'] \arrow[u, phantom, "="] \end{tikzcd}}]{Images/imgbf492aa4a46c11c7a544c37fb3ccb164.svg}}. \end{equation*}$$

One commonly writes $\vcenter{\img[][47pt][33pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} A \arrow[r, bend right, "u"'] \arrow[r, phantom, "\bot"] & B \arrow[l, bend right, "f"'] \end{tikzcd}}]{Images/img27da47b36b1d1ad8617028b8452e6652.svg}}$ to indicate that $f$ is left adjoint to $u$, its right adjoint, with the data of the unit $\eta$ and counit $\epsilon$ being left implicit.

Among the many advantages of using definitions that are taken “off the shelf” from the 2-categories literature is that the standard 2-categorical proofs then specialize to prove the following facts about adjunctions between $\infty$-categories.⁠⁹

⁹

What is less obvious is that these definitions are “correct” for $\infty$-category theory. In the case of equivalences, this is easily seen in any of the models. In the case of adjunctions, this is quite subtle, and involves the fact that the low-dimensional data enumerated in Definition 3.3 suffices to determine a full “homotopy coherent adjunction,” uniquely up to a contractible space of choices RV1.

✖

Proposition 3.4 (RV2, 2.1.9).

Adjunctions between $\infty$-categories compose:

$$\begin{equation*} \vcenter{\img[][211pt][34pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} A \arrow[r, bend right, "u"'] \arrow[r, phantom, "\bot"] & B \arrow[l, bend right, "f"'] \arrow[r, bend right, "v"'] \arrow[r, phantom, "\bot"] & C \arrow[l, bend right, "g"'] & \rightsquigarrow& A \arrow[r, bend right, "v \circ u"'] \arrow[r, phantom, "\bot"] & C \arrow[l, "f \circ g"', bend right] \end{tikzcd}}]{Images/img5b515b2dd896c9aea252a82d8cfd012c.svg}} \end{equation*}$$

Proposition 3.5 (RV2, 2.1.10).

Given an adjunction $\vcenter{\img[][47pt][33pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} A \arrow[r, bend right, "u"'] \arrow[r, phantom, "\bot"] & B \arrow[l, bend right, "f"'] \end{tikzcd}}]{Images/img27da47b36b1d1ad8617028b8452e6652.svg}}$ between $\infty$-categories and a functor $f' \colon B \to A$, $f'$ is left adjoint to $u$ if and only if there exists a natural isomorphism $f \cong f'$.

Proposition 3.6 (RV2, 2.1.12).

Any equivalence can be promoted to an adjoint equivalence at the cost of replacing either of the natural isomorphisms.

Relative adjunctions

The unit and counit in an adjunction satisfy a universal property in the 2-category $\infty \text{-}\mathsf{CAT}$ that we now explore in the case of the counit $\epsilon \colon fu \Rightarrow \mathrm{id}_A$. Given any $\infty$-functors $a \colon X \to A$ and $b \colon X \to B$, pasting with $\epsilon$ defines a bijection between $\infty$-natural transformations $\alpha \colon fb \Rightarrow a$ and $\beta \colon b \Rightarrow ua$. Any $\alpha \colon fa \Rightarrow b$ factors through a unique $\beta \colon b \Rightarrow ua$ as displayed below:

$$\begin{equation} \vcenter{\img[][136pt][44pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} X \arrow[r, "b"] \arrow[d, "a"'] \arrow[dr, phantom, "\scriptstyle\forall\Downarrow\alpha"] & B \arrow[d, "f"] & X \arrow[r, "b"] \arrow[d, "a"'] \arrow[dr, phantom, "\scriptstyle\exists!\!\Downarrow\!\beta" very near start, "\scriptstyle\Downarrow\epsilon" very near end] & B \arrow[d, "f"]\\ A \arrow[r, equals] & A \arrow[ur, phantom, "="] & A \arrow[r, equals] \arrow[ur, "u" description] & A \end{tikzcd}}]{Images/img499156d0b6f7a0d2292cac3d7347d9f2.svg}} {\tag{3.7}} \end{equation}$$

which is to say that the pair $(u,\epsilon )$ defines an absolute right lifting of $\mathrm{id}_A$ through $f$. Indeed, $f$ is left adjoint to $u$ with counit $\epsilon$ if and only if $(u,\epsilon )$ defines an absolute right lifting of $\mathrm{id}_A$ through $f$ RV2, 2.3.7.

Any component $\epsilon a$ of the counit $\epsilon$ of an adjunction satisfies a universal property analogous to 3.7:

$$\begin{equation*} \vcenter{\img[][176pt][48pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} Y \arrow[r, "b"] \arrow[d, "x"'] \arrow[dr, phantom, "\scriptstyle\forall\Downarrow\alpha"] & B \arrow[d, "f"] & Y \arrow[rr, "b"] \arrow[d, "x"'] \arrow[dr, phantom, "\scriptstyle\exists!\!\Downarrow\!\beta"] & \arrow[dr, phantom, "\scriptstyle\Downarrow\epsilon" very near end] & B \arrow[d, "f"]\\ X \arrow[r, "a"'] & A \arrow[ur, phantom, "="] & X \arrow[r, "a"'] & A \arrow[r, equals] \arrow[ur, "u" description] & A \end{tikzcd}}]{Images/imgffef98440988b4ad68ef6d2ac89566a7.svg}} \end{equation*}$$

which asserts that $(ua,\epsilon a)$ defines an absolute right lifting of $a$ through $f$. Motivated by examples such as these, absolute right liftings $(r,\rho )$ of a generic $\infty$-functor $g \colon C \to A$ through $f \colon B \to A$ can be thought of as exhibiting $r$ as right adjoint to $f$ relative to $g$ with partial counit $\rho$.

Definition 3.8.

Given $\infty$-functors $g \colon C \to A$ and $f \colon B \to A$ with common codomain, a functor $r \colon C \to B$ and $\infty$-natural transformation $\rho \colon fr \Rightarrow g$ define an absolute right lifting of $g$ through $f$ or a right adjoint of $f$ relative to $g$ if pasting with $\rho$ induces a bijection between $\infty$-natural transformations as displayed below:

$$\begin{equation*} \vcenter{\img[][135pt][50pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} X \arrow[r, "b"] \arrow[d, "c"'] \arrow[dr, phantom, "\scriptstyle\forall\Downarrow\alpha"] & B \arrow[d, "f"] & X \arrow[r, "b"] \arrow[d, "c"'] \arrow[dr, phantom, "\scriptstyle\exists!\!\Downarrow\!\beta" very near start, "\scriptstyle\Downarrow\rho" very near end] & B \arrow[d, "f"]\\ C \arrow[r, "g"'] & A \arrow[ur, phantom, "="] & C \arrow[r, "g"'] \arrow[ur, "r" description] & A \end{tikzcd}}]{Images/img0f26bb5522d4c1b1306797210824fd31.svg}} \end{equation*}$$

The following lemmas about relative right adjoints admit straightforward 2-categorical proofs:

Lemma 3.9 (RV2, 2.3.6).

If $(r,\rho )$ is right adjoint to $f \colon B \to A$ relative to $g \colon C \to A$ then for any $c \colon X \to C$, $(rc,\rho c)$ is right adjoint to $f$ relative to $gc$.

$$\begin{equation*} \vcenter{\img[][93pt][45pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd}& \arrow[dr, phantom, "\scriptstyle\Downarrow\rho" very near end] & B\arrow[d, "f"] \\ X \arrow[r, "c"'] & C \arrow[r, "g"'] \arrow[ur, "r"] & A \end{tikzcd}}]{Images/img6bbee9577967baf3bbf3021c587727bc.svg}} \end{equation*}$$

Lemma 3.10 (RV2, 2.4.1).

Suppose that $(r,\rho )$ is right adjoint to $f \colon B \to A$ relative to $g \colon C \to A$. Then in any diagram of $\infty$-functors and $\infty$-natural transformations

$$\begin{equation*} \vcenter{\img[][51pt][78pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} \arrow[dr, phantom, "\scriptstyle\Downarrow\sigma" very near end] & D \arrow[d, "k"] \\ \arrow[dr, phantom, "\scriptstyle\Downarrow\rho" very near end] & B \arrow[d, "f"] \\ C \arrow[r, "g"'] \arrow[ur, "r"] \arrow[uur, "s", bend left] & A \end{tikzcd}}]{Images/imgc64c6a7654f66bb716bcd6ec273ecd03.svg}} \end{equation*}$$

$(s,\sigma )$ is right adjoint to $k$ relative to $r$ if and only if $(s, \rho \cdot f\sigma )$ is right adjoint to $fk$ relative to $g$.

Limits and colimits

Relative adjunctions can be used to define limits and colimits of diagrams valued inside an $\infty$-category $A$ and indexed by another $\infty$-category $J$. As a cartesian closed 2-category, $\infty \text{-}\mathsf{CAT}$ contains a terminal $\infty$-category $1$, which admits a unique $\infty$-functor $! \colon J \to 1$ from any other $\infty$-category $J$. Maps $a \colon 1 \to A$ from the terminal $\infty$-category into another $\infty$-category define elements in the $\infty$-category $A$.⁠¹⁰ Using the cartesian closed structure, any diagram $d \colon J \to A$ defines an element $d \colon 1 \to A^J$ in the $\infty$-category of $J$-shaped diagrams in $A$. Exponentiation with the unique functor $! \colon J \to 1$ defines the constant diagrams functor $\Delta \colon A \to A^J$, which carries an element of $A$ to the constant $J$-shaped diagram at that element.

¹⁰

We find this terminology less confusing than referring to the “objects” in an $\infty$-category $A$, which is itself an object of $\infty \text{-}\mathsf{CAT}$.

✖

Definition 3.11.

An $\infty$-category $A$ admits $J$-shaped limits if the constant diagrams functor $\Delta \colon A \to A^J$ admits a right adjoint and admits $J$-shaped colimits if the constant diagrams functor admits a left adjoint:

$$\begin{equation*} \vcenter{\img[][51pt][41pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} A \arrow[r, "\Delta" description] & A^J \arrow[l, bend left=40, "\lim", "\bot"'] \arrow[l, bend right=40, "\colim"' pos=.45, "\bot" pos=.6] \end{tikzcd}}]{Images/imgb0520a6b678f3d894d460e28c626fb12.svg}} \end{equation*}$$

The counit $\lambda$ of the adjunction $\Delta \dashv \lim$ and the unit $\gamma$ of the adjunction $\mathrm{colim}\dashv \Delta$ encode the limit and colimit cones, as is most easily seen when considering their components at a diagram $d \colon 1 \to A^J$. By Lemma 3.9, the right and left adjoints restrict to define relative adjunctions:

$$\begin{equation*} \vcenter{\img[][221pt][47pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} & \arrow[dr, phantom, "\scriptstyle\Downarrow\lambda" very near end] & A \arrow[d, "\Delta"] & & \arrow[dr, phantom, "\scriptstyle\Uparrow\gamma" very near end] & A \arrow[d, "\Delta"] \\ 1 \arrow[r, "d"'] & A^J \arrow[ur, "\lim"] \arrow[r, equals] & A^J & 1 \arrow[r, "d"'] & A^J \arrow[ur, "\colim"] \arrow[r, equals] & A^J \end{tikzcd}}]{Images/imgbab4d195cefb7c2ea7cdf13e1a245c08.svg}} \end{equation*}$$

These observations allow us to generalize Definition 3.11 to express the universal properties of the limit or colimit of a single diagram in settings where the limit and colimit functors do not exist.

Definition 3.12.

A diagram $d \colon J \to A$ between $\infty$-categories admits a limit just when $\Delta$ admits a relative right adjoint at $d$ and admits a colimit just when $\Delta$ admits a relative left adjoint at $d$, as encoded by absolute lifting diagrams:

$$\begin{equation*} \vcenter{\img[][133pt][47pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} \arrow[dr, phantom, "\scriptstyle\Downarrow\lambda_d" very near end] & A \arrow[d, "\Delta"] & \arrow[dr, phantom, "\scriptstyle\Uparrow\gamma_d" very near end] & A \arrow[d, "\Delta"] \\ 1 \arrow[r, "d"'] \arrow[ur, "\lim d"] & A^J & 1 \arrow[r, "d"'] \arrow[ur, "\colim d"] & A^J \end{tikzcd}}]{Images/imgfb7cdad3d2facc12fdff04bdb72554be.svg}} \end{equation*}$$

There is an easy formal proof of the $\infty$-categorical version of a classical theorem:

Theorem 3.13.

Right adjoints preserve limits and left adjoints preserve colimits.

Proof.

Consider an adjunction as in Definition 3.3 and a limit of a diagram as in Definition 3.12. To show that the limit is preserved by the right adjoint, we must show that

$$\begin{equation*} \vcenter{\img[][95pt][51pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd} \arrow[dr, phantom, "\scriptstyle\Downarrow\lambda_d" very near end] & A \arrow[d, "\Delta"] \arrow[r, "u"] & B \arrow[d, "\Delta"] \\ 1 \arrow[r, "d"'] \arrow[ur, "\lim d"] & A^J \arrow[r, "u^J"'] & B^J \end{tikzcd}}]{Images/imgce7d3eaedd3c5d72983db6a742d25d24.svg}} \end{equation*}$$

defines a relative right adjoint. By Lemma 3.10, it suffices to demonstrate this after pasting with the relative right adjoint encoded by the component at $d$ of the counit $\epsilon ^J$ of the adjunction $f^J \dashv u^J$, as below-left:

$$\begin{equation*} \vcenter{\img[][342pt][84pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd}[column sep=3em] \arrow[dr, phantom, "\scriptstyle\Downarrow\lambda_d" pos=.85] & A \arrow[d, "\Delta"]\arrow[r, "u"] & B \arrow[d, "\Delta"] & [-3pt]{~} &\arrow[dr, phantom, "\scriptstyle\Downarrow\epsilon" pos=.85] & B \arrow[d, "f"] & \arrow[dr, phantom, "\scriptstyle\Downarrow\epsilon_{\lim d}" pos=.8] & B \arrow[d, "f"] \\ 1 \arrow[ur, "\lim d"] \arrow[r, "d"'] & A^J \arrow[dr, equals] \arrow[r, "{u^J}"] & B^J \arrow[d, "{f^J}"] \arrow[dl, phantom, "{\scriptstyle\Downarrow\epsilon^J}" pos=.15] \arrow[r, phantom, "="] & ~\arrow[dr, phantom, "\scriptstyle\Downarrow\lambda_d" pos=.85] & A \arrow[ur, "u"] \arrow[r, equals] \arrow[d, "\Delta"] & A \arrow[d, "\Delta"] \arrow[r, phantom, "="] & ~\arrow[dr, phantom, "\scriptstyle\Downarrow\lambda_d" pos=.9] & A \arrow[d, "\Delta"] \\ & ~& A^J & 1 \arrow[r, "d"'] \arrow[ur, "\lim d"] & A^J \arrow[r, equals] & A^J & 1 \arrow[r, "d"'] \arrow[ur, "\lim d" {xshift=2pt}] \arrow[uur, bend left, "u\lim d"] & A^J \end{tikzcd}}]{Images/img6ec0b9219f60d90ccda35397d0eabdec.svg}} \end{equation*}$$

From the 2-functoriality of the exponential in a cartesian closed 2-category, $f^J\Delta = \Delta f$ and $\epsilon ^J \Delta = \Delta \epsilon$. Hence, the pasting diagram displayed above-left equals the one displayed above-center, which equals the diagram above-right. This latter diagram is a pasted composite of relative right adjoints, and is then a relative right adjoint in its own right by Lemma 3.10.

Universal properties

Definitions 3.3 and 3.12 do not express the full universal properties of adjunctions between and co/limits in $\infty$-categories. These require additional structure borne by the 2-category $\infty \text{-}\mathsf{CAT}$, namely the existence of comma $\infty$-categories for any pair of $\infty$-functors $f \colon B \to A$ and $g \colon C \to A$. The comma $\infty$-category is an $\infty$-category $\mathrm{Hom}_A(f,g)$ equipped with canonical functors and an $\infty$-natural transformation as below-left, formed by the pullback of $\infty$-categories below-right:

$$\begin{equation} \vcenter{\img[][286pt][55pt][{\renewcommand{\arraystretch}{1} \setlength{\unitlength}{1.0pt} \begin{tikzcd}[column sep=3.4em] \Hom_A(f,g) \arrow[r, "\dom"] \arrow[d, "\cod"'] \arrow[dr, phantom, "\scriptstyle\Downarrow\phi"] & B \arrow[d, "f"] & \Hom_A(f,g) \arrow[dr, phantom, "\lrcorner" very near start]\arrow[r, "\phi"] \arrow[d, "{(\cod,\dom)}"'] & A^{\mathbb{2}} \arrow[d, "{(\cod,\dom)}"] \\ C \arrow[r, "g"'] & A & C \times B \arrow[r, "g \times f"'] & A \times A \end{tikzcd}}]{Images/imgd626e83e30635f0afa09f5d9eb31716e.svg}} {\tag{3.14}} \end{equation}$$

While the universal property of $\mathrm{Hom}_A(f,g)$ as an object of $\infty \text{-}\mathsf{CAT}$ is weaker than the standard notion of comma object in 2-category theory, nevertheless:

Theorem 3.15 (RV2, 3.5.8).

An $\infty$-functor $f \colon B \to A$ admits a right adjoint $r \colon C \to B$ relative to $g \colon C \to A$ if and only if there exists an equivalence over $C \times B$:

$$\begin{equation*} \mathrm{Hom}_A(f,g) \simeq _{C \times B} \mathrm{Hom}_B(B,r). \end{equation*}$$

When Theorem 3.15 is applied to $f \colon B \to A$ and $\mathrm{id}_A$, it specializes to:

Corollary 3.16 (RV2, 4.1.1).

An $\infty$-functor $f \colon B \to A$ admits a right adjoint $u \colon A \to B$ if and only if $\mathrm{Hom}_A(f,A) \simeq _{A \times B} \mathrm{Hom}_B(B,u)$.

When Theorem 3.15 is applied to $\Delta \colon A \to A^J$ and $d \colon 1 \to A^J$ it specializes to:

Corollary 3.17 (RV2, 4.3.1).

A diagram $d \colon J \to A$ has a limit $\ell \colon 1 \to A$ if and only if $\mathrm{Hom}_{A^J}(\Delta ,d) \simeq _A \mathrm{Hom}_A(A,\ell )$.

Here the comma $\infty$-category $\mathrm{Hom}_{A^J}(\Delta ,d)$ defines the $\infty$-category of cones over $d$. The $\infty$-category $\mathrm{Hom}_A(A,\ell )$ admits a terminal element $\mathrm{id}_\ell \colon 1 \to \mathrm{Hom}_A(A,\ell )$, which defines a right adjoint to the unique functor $! \colon \mathrm{Hom}_A(A,\ell ) \to 1$. Via the equivalence $\mathrm{Hom}_{A^J}(\Delta ,d) \simeq _A \mathrm{Hom}_A(A,\ell )$ we see that the limit cone is terminal in the $\infty$-category of cones. Indeed, $d$ admits a limit if and only if the $\infty$-category of cones admits a terminal element RV2, 4.3.2.

Could we teach this to undergraduates?

If classical category theory were a standard course in the undergraduate mathematics curriculum, then perhaps students with a particular interest in the subject might go on to learn some 2-category theory, like students with a particular interest in algebra might go on to take more specialized courses in classical algebraic geometry, algebraic number theory, or representation theory when offered. From this point, the proofs of the results stated here are not too difficult.

But these results encompass only a small portion of $\infty$-category theory, and for most of the rest there is a greater jump in complexity when extending from 1-categories to $\infty$-categories. This is best illustrated by considering the Yoneda lemma, which in an important special case is stated as follows:

Theorem 3.18 (RV2, 5.7.1).

Given an $\infty$-category $A$ and elements $a,b \colon 1 \to A$, the $\infty$-groupoid $\mathrm{Hom}_A(a,b)$ is equivalent to the $\infty$-groupoid of functors $\mathrm{Hom}_A(A,a) \to \mathrm{Hom}_A(A,b)$ over $A$.

One direction of this equivalence is easy to describe: the map from right to left is defined by evaluation at the identity element $\mathrm{id}_a \colon 1 \to \mathrm{Hom}_A(a,a)$. The inverse equivalence defines the Yoneda embedding, which is notoriously difficult to construct in $\infty$-category theory as it involves equipping $A$ with a homotopy coherent composition function L2, §5.1.3.

To achieve further simplifications of $\infty$-category theory, one idea is to ask our foundation system to do more of the work.

4. A Synthetic Theory of $\infty$-Categories

To explain the desiderata for an alternative foundation, consider the default notions of “sameness” for $\infty$-categorical data. Two elements in an $\infty$-category are the same if and only if they are connected by a path in the underlying $\infty$-groupoid, while parallel morphisms are the same if and only if they are connected by an invertible 2-cell, defining a path in the appropriate mapping space. For an $\infty$-categorical construction to be “well-defined” it must:

(i)

respect the notions of sameness encoded by paths in suitable spaces, and

(ii)

respect equivalences between these spaces themselves, since they are only well-defined as homotopy types.

Axiomatizing sameness

In traditional foundations, there is a similar axiom that mathematical constructions or results must respect sameness as encoded by equality. The axioms that define the binary relation “$=$” in first-order logic are:

•

reflexivity: for all $x$, $x=x$ is true.

•

indiscernibility of identicals: for all $x,y$ and for all predicates $P$, if $x=y$ then $P(x)$ holds if and only if $P(y)$ holds.

Analogous rules govern Martin-Löf’s identity types in an alternative foundational framework for constructive mathematics known as dependent type theory M-L. Here the primitives include types like $\mathbb{N}$, $GL_n(\mathbb{R})$, and $\mathrm{Group}$ and terms like $17 : \mathbb{N}$, $I^n : GL_n(\mathbb{R})$, $S_n : \mathrm{Group}$, which may depend on an arbitrary context of variables drawn from previously defined types (e.g., the $n :\mathbb{N}$ appearing in three examples above).⁠¹¹ In traditional foundations, mathematical structures are defined in the language of set theory, while proofs obey the rules of first-order logic. In dependent type theory, mathematical constructions and mathematical proofs are unified: both are given by terms in appropriate types. The ambient type then describes the sort of object being constructed or the mathematical statement being proven, while the context describes the inputs to the construction or the hypotheses for the theorem.

¹¹

In a mathematical statement of the form “Let …be …then …” the stuff following the “let” likely declares the names of the variables in the context described after the “be,” while the stuff after the “then” most likely describes a type or term in that context.

✖

The rules for Martin-Löf’s identity types include:⁠¹²

¹²

One additional rule, not listed here, concerns the computational behavior of this system.

✖

•

identity-formation: in the context of two variables $x,y :A$ there is a type $x=_Ay$.

Types encode mathematically meaningful statements or assertions, so this rule says that it is reasonable to inquire whether $x$ and $y$ might be identified, once $x$ and $y$ are terms in the same type. Certain identity types, such as $3=_\mathbb{N}4$, will be empty, since the terms $3$ and $4$ cannot be identified, but the type nevertheless exists.

•

identity-introduction: for any $x : A$, there is a term $\mathrm{refl}_x : x=_Ax$.

Terms in types are witnesses to the truth of the statement encoded by the type, so this rule corresponds to the reflexivity axiom.

•

identity-elimination: given any family of types $Q(x,y,p)$ depending on $x, y : A$ and $p : x=_Ay$, to provide a family of terms $q_{x,y,p} : Q(x,y,p)$ for all $x,y,p$ it suffices to provide a family of terms $d_x : Q(x,x,\mathrm{refl}_x)$ for all $x$.

This rule implies Leibniz’s indiscernibility of identicals and much more besides:

Theorem 4.1 (BGLu).

The iterated identity types provide any type with the structure of an $\infty$-groupoid, in which the terms are the points, the identifications are the paths, and the higher identifications encode homotopies.

In low dimensions, the $\infty$-groupoid structure on the iterated identity types of a type $A$ provides:

•

functions $(-)^{-1} : (x=_A y) \to (y=_Ax)$ that invert identifications,

•

functions $-\ast - : (x=_Ay) \times (y=_Az) \to (x=_A z)$ that compose identifications,

•

higher identifications $\text{assoc} : (p \ast q) \ast r =_{x =_A w} p \ast (q \ast r)$ between composable triples of identifications,

and much more. All of these terms are constructed using the identity-elimination rule from the reflexivity terms provided by the identity-introduction rule. Since an identification $p : x=_A y$ defines a path from $x$ to $y$ in the $\infty$-groupoid $A$, identifications in dependent type theory are often referred to colloquially as “paths.”

The homotopical interpretation of dependent type theory

The homotopical interpretation of dependent type theory was discovered in the early 21st century by Awodey–Warren and Voevodsky, building on earlier work of Hofmann and Streicher. This connection inspired Voevodsky to make the following definition:

Definition 4.2.

A type $A$ is contractible just when there is a term of type

$$\begin{equation*} \Sigma _{x :A} \Pi _{y : A} x=_A y, \end{equation*}$$

which may be read as “there exists $x:A$, so that for all $y :A$, $x$ is identifiable with $y$” with all quantifiers interpreted as requiring continuous specifications of data.⁠¹³

¹³

The definition of contractible types makes use of the dependent pair and dependent function types in dependent type theory. A term of type $\Sigma _{x :A} \Pi _{y : A} x=_A y$ provides a term $c : A$, the “center of contraction,” together with a family of paths $p_z : c =_A z$ for all $z : A$, the “contracting homotopy.”

✖

Just as contractible spaces might contain uncountably infinitely many points, contractible types might contain more than one term. But since any two terms in a contractible type may be identified, and since identity-elimination implies that all of dependent type theory respects identifications, the theory behaves as if a contractible type had a unique term.

Univalent foundations

Martin-Löf’s dependent type theory is a formal system in which all constructions are continuous in paths, our first desideratum. The second desideratum, of well-definedness under equivalences between types, follows once Voevodsky’s univalence axiom is added to dependent type theory, resulting in a formal system called homotopy type theory or univalent foundations.

Voevodsky’s univalence connects two notions of sameness for types. In traditional dependent type theory, types can be encoded as terms in a universe of types.⁠¹⁴ Thus, one notion of sameness between types $A, B$ belonging to a universe $\mathcal{U}$ is given by paths $p : A=_\mathcal{U}B$ in the universe. Another notion of sameness is suggested by types as $\infty$-groupoids: for any $A$ and $B$ there is a type $A \simeq B$ of (homotopy) equivalences from $A$ to $B$.⁠¹⁵ By identity-elimination, to define a natural map $\text{id-to-equiv}: A =_\mathcal{U}B \to A \simeq B$ it suffices to define the image of $\mathrm{refl}_A : A =_\mathcal{U}A$, which we take to be the identity equivalence. The univalence axiom asserts that this map is an equivalence for all types $A$ and $B$.

¹⁴

Russell’s paradox can be resolved by a cumulative hierarchy of universes.

✖

¹⁵

It is an interesting challenge to define a type whose data witnesses that a given map $f \colon A \to B$ is an equivalence in such a way that this type is contractible whenever it is inhabited.

✖

By univalence, an equivalence $e : A \simeq B$ gives rise to a path $\mathrm{ua}(e) : A =_\mathcal{U}B$, which can then be used to transport terms in any type involving $A$ to terms in the corresponding type involving $B$. Thus, univalent mathematics is automatically invariant under equivalence between types.

$\infty$-categories in univalent foundations

There is an experimental exploration of $\infty$-category theory RSBWBa in an extension of homotopy type theory in which every type $A$ has a family of arrows $\mathrm{Hom}_A(x,y)$ in addition to the family of paths $x=_Ay$. These types are obtained from a new type-forming operation that produces extension types, whose terms are type-valued diagrams that strictly extend a given diagram along an inclusion of “shapes” (polytopes embedded in directed cubes constructed in the theory of a strict interval) RS, §2-4. Extension types include types analogous to the pullbacks of 1.4 and 3.14.

The formal system has semantics in complete Segal spaces RSW so it provides a rigorous way to prove theorems about $\infty$-categories as understood in traditional foundations. At the same time, the experience of working with $\infty$-categories in this “univalent” foundational setting is much more akin to the experience of working with 1-categories in traditional foundations.

It takes work to set up this formal system and considerably more to describe its interpretation in complete Segal spaces; indeed, this is where the hard work of solving homotopy coherence problems goes. But once this is done, it is possible to define the notion of an $\infty$-category, something that would no doubt be reassuring to undergraduates hoping to learn about them.⁠¹⁶ The two axioms express the “Segal” and “completeness” conditions of Rezk’s model R1, respectively.

¹⁶

Recall that in the formal $\infty$-category theory developed in the 2-category $\infty \text{-}\mathsf{CAT}$, a concrete definition of $\infty$-categories is not used.

✖

Definition 4.3 (RS, 5.3,10.6).

An $\infty$-category is a type $A$ in which:

•

every composable pair of arrows has a unique composite, and

•

for any pair of terms $x, y : A$ the natural map $x=_A y \to x \cong _A y$ from paths in $A$ to isomorphisms in $A$ is an equivalence.

The “uniqueness” in the first axiom is in the sense of Definition 4.2: what it asserts is that a suitable space of composites analogous to Definition 1.3 is contractible—the default meaning of uniqueness in this formal system. Like in the space defined by 1.4, a term in the space of composites provides a higher-dimensional witness to the composition relation. A composition function

$$\begin{equation*} \circ \colon \mathrm{Hom}_A(y,z) \times \mathrm{Hom}_A(x,y) \to \mathrm{Hom}_A(x,z), \end{equation*}$$

is obtained by throwing away these witnesses. Like any construction in homotopy type theory, this function respects identifications and is therefore well-defined. It follows from this axiom that composition is associative and unital, using canonical identity arrows $\mathrm{id}_x : \mathrm{Hom}_A(x,x)$.

The second axiom involves a type of isomorphisms in $A$, which may be defined in a similar manner to the type of equivalences between types RS, §10.

The Yoneda lemma

The advantages of this synthetic framework for $\infty$-category theory are on display when comparing the proofs of the Yoneda lemma in RV2, 5.7.1 and in RS, 9.1. We sketch the latter here in the same special case considered in Theorem 3.18.

Theorem 4.4 (RS, 9.1).

Given an $\infty$-category $A$ and elements $a,b \colon 1 \to A$, the type $\mathrm{Hom}_A(a,b)$ is equivalent to the type $\Pi _{x :A} \mathrm{Hom}_A(x,a) \to \mathrm{Hom}_A(x,b)$ of fiberwise functions.

A key difference between Theorem 3.18 and Theorem 4.4 is that in the present framework it is straightforward to define the inverse equivalence to the evaluation at identity map. The inverse equivalence takes an arrow $f: \mathrm{Hom}_A(a,b)$ to the natural map $x \mapsto g \mapsto f \circ g : \Pi _{x:A} \mathrm{Hom}_A(x,a) \to \mathrm{Hom}_A(x,b)$. The usual proof then demonstrates that these maps are inverse equivalences. In one direction, this is given by an identification $f \circ \mathrm{id}_a =_{\mathrm{Hom}_A(a,b)} f$, which expresses the fact that composition in an $\infty$-category is unital. In the other direction, we must show that a fiberwise map $\phi$ agrees with the map whose component at $x$ is given by $g \mapsto \phi _a(\mathrm{id}_a) \circ g: \mathrm{Hom}_A(x,a) \to \mathrm{Hom}_A(x,b)$. By a consequence of the univalence axiom called “function extensionality,” it suffices to show that $\phi _a(\mathrm{id}_a) \circ g =_{\mathrm{Hom}_A(x,b)} \phi _x(g)$. This follows from the fact that fiberwise maps are automatically “natural,” providing an identification $\phi _a(\mathrm{id}_a) \circ g =_{\mathrm{Hom}_A(x,b)} \phi _x(\mathrm{id}_a \circ g)$. Since the function $\phi _x$ respects the identification $\mathrm{id}_a \circ g =_{\mathrm{Hom}_A(x,a)} g$, we obtain the required identification.

In fact, RS, 9.5 proves a generalization of the Yoneda lemma that was first discovered with this formal system and later proven in traditional foundations RV2, 5.7.2

Conclusion

Significant technical problems remain to make it feasible to teach $\infty$-category theory to undergraduates, but I have hope that in the future the subject will not seem as forbidding as it does today.