1.7 The homotopy 2-category

Small 1-categories define the objects of a strict 2-category ${\mathord {\mathcal{Cat}}}$ of categories, functors, and natural transformations. Many basic categorical notions — those defined in terms of categories, functors, and natural transformations — can be defined internally to the 2-category ${\mathord {\mathcal{Cat}}}$. This suggests a natural avenue for generalization: reinterpreting these same definitions in a generic 2-category using its objects in place of small categories, its 1-cells in place of functors, and its 2-cells in place of natural transformations.

A significant portion of the theory of $\infty $-categories in any fixed $\infty $-cosmos can be developed by following exactly this outline, working internally to a 2-category that we refer to as the homotopy 2-category that we associate to any $\infty $-cosmos. The homotopy 2-category of an $\infty $-cosmos is a quotient of the full $\infty $-cosmos, replacing each quasi-categorical functor space by its homotopy category. Surprisingly, this rather destructive quotienting operation preserves quite a lot of information. This said, we caution the reader against becoming overly seduced by homotopy 2-categories, which are more of a technical convenience for reducing the complexity of our arguments than a fundamental notion of $\infty $-category theory.

Paralleling our discussion of simplicial categories in Definition 1.3.1 and Digression 1.3.5, there are two perspectives on the notion of a 2-category, which can be understood equally as:

“two-dimensional” categories, with objects; 1-cells, whose boundary are given by a pair of objects; and 2-cells, whose boundary are given by a parallel pair of 1-cells between a pair of objects — together with partially defined composition operations governed by this boundary data
or as categories enriched over ${\mathord {\mathcal{Cat}}}$.

Both notions exist in Mathlib in some form. The notion i is called a strict bicategory and is defined as a special case of a bicategory, in which the associators and unitors are identities (converted into 2-cells). The general notion of enriched category can be specialized to the case of enriching over the cartesian monoidal category of categories, but the connection between these notions remains to be explored.

Proposition 1.7.1

There is an equivalence between categories enriched in categories and strict bicategories. In particular, each can be converted into the other.

The homotopy 2-category is most efficiently defined as a category enriched in ${\mathord {\mathcal{Cat}}}$ by applying the theory of change-of-base developed in §1.6. The homotopy 2-category for the $\infty $-cosmos of quasi-categories was first introduced by Joyal in his work on the foundations of quasi-category theory [ Joy08 ] .

Definition 1.7.2 homotopy 2-category

Let ${\mathord {\mathcal{K}}}$ be an $\infty $-cosmos. Its homotopy 2-category is the 2-category $\mathfrak {h}{\mathord {\mathcal{K}}}$ whose

objects are the objects $A, B$ of ${\mathord {\mathcal{K}}}$, i.e., the $\infty $-categories;
1-cells $f \colon A \to B$ are the 0-arrows in the functor space ${\mathord {\mathsf{Fun}}}(A,B)$, i.e., the $\infty $-functors; and
2-cells

$\begin{tikzcd} A \arrow[r, start anchor=15, end anchor=165, bend left, "f"] \arrow[r, start anchor=345, end anchor=195, bend right, "g"'] \arrow[r, phantom, "{\scriptstyle\Downarrow \alpha}"] & B\end{tikzcd}$

are homotopy classes of 1-simplices in ${\mathord {\mathsf{Fun}}}(A,B)$, which we call $\infty $-natural transformations.

Put another way $\mathfrak {h}{\mathord {\mathcal{K}}}$ is the 2-category with the same objects as ${\mathord {\mathcal{K}}}$ and with hom-categories defined by

\[ {\mathord {\mathsf{hFun}}}(A,B) :={\mathord {\mathsf{h}}}({\mathord {\mathsf{Fun}}}(A,B)), \]

that is, ${\mathord {\mathsf{hFun}}}(A,B)$ is the homotopy category of the quasi-category ${\mathord {\mathsf{Fun}}}(A,B)$.

Definition 1.7.3 underlying category of a 2-category

The underlying category of a 2-category is defined by simply forgetting its 2-cells. Note that an $\infty $-cosmos ${\mathord {\mathcal{K}}}$ and its homotopy 2-category $\mathfrak {h}{\mathord {\mathcal{K}}}$ share the same underlying category ${\mathord {\mathcal{K}}}_0$ of $\infty $-categories and $\infty $-functors in ${\mathord {\mathcal{K}}}$.

Lemma 1.7.4

The underlying category of the homotopy 2-category of an $\infty $-cosmos is isomorphic to the underlying category of the $\infty $-cosmos.

We elaborate on the connection between data in the homotopy 2-category and data in the $\infty $-cosmos.

Lemma 1.7.5

$\quad $

Every 2-cell

$\begin{tikzcd} A \arrow[r, start anchor=15, end anchor=165, bend left, "f"] \arrow[r, start anchor=345, end anchor=195, bend right, "g"'] \arrow[r, phantom, "\scriptstyle\Downarrow\alpha"] & B \end{tikzcd}$

in the homotopy 2-category of an $\infty $-cosmos is represented by a map of quasi-categories as below-left or equivalently by a functor as below-right

$\begin{tikzcd} [sep=small] & \catone+\catone \arrow[dl, hook'] \arrow[dr, "{(f,g)}"] & & & ~ & A \arrow[rr, "\name{\alpha}"] \arrow[dr, "{(g,f)}"'] & & B^\cattwo \arrow[dl, "{(p_1,p_0)}", two heads] \\ \cattwo \arrow[rr, "{\alpha}"'] && \Fun(A,B) &\arrow[ur, phantom, "\leftrightsquigarrow"] & && B \times B \end{tikzcd}$

and two such maps represent the same 2-cell if and only if they are homotopic as 1-simplices in ${\mathord {\mathsf{Fun}}}(A,B)$.
Every invertible 2-cell

$\begin{tikzcd} [column sep=large] A \arrow[r, start anchor=18, end anchor=162, bend left=20, "f"] \arrow[r, start anchor=342, end anchor=198, bend right=20, "g"'] \arrow[r, phantom, "\scriptstyle\cong\Downarrow\alpha"] & B \end{tikzcd}$

in the homotopy 2-category of an $\infty $-cosmos is represented by a map of quasi-categories as below-left or equivalently by a functor as below-right

$\begin{tikzcd} [sep=small] & \catone+\catone \arrow[dl, hook'] \arrow[dr, "{(f,g)}"] & & & ~ & A \arrow[rr, "\name{\alpha}"] \arrow[dr, "{(g,f)}"'] & & B^\iso \arrow[dl, "{(p_1,p_0)}", two heads] \\ \iso \arrow[rr, "{\alpha}"'] && \Fun(A,B) &\arrow[ur, phantom, "\leftrightsquigarrow"] & && B \times B \end{tikzcd}$

and two such maps represent the same invertible 2-cell if and only if their common restrictions along $[1]\hookrightarrow I$ are homotopic as 1-simplices in ${\mathord {\mathsf{Fun}}}(A,B)$.

The notion of homotopic 1-simplices referenced here is defined in Lemma 1.2.20. Since the 2-cells in the homotopy 2-category are referred to as $\infty $-natural transformations, we refer to the invertible 2-cells in the homotopy 2-category as $\infty $-natural isomorphisms.

Proof ▶

The statement i records the definition of the 2-cells in the homotopy 2-category and the universal property 1.3.1 of the simplicial cotensor. For ii, a 2-cell in the homotopy 2-category is invertible if and only if it defines an isomorphism in the appropriate hom-category ${\mathord {\mathsf{hFun}}}(A,B)$. By Proposition 1.2.32 it follows that each invertible 2-cell $\alpha $ is represented by a homotopy coherent isomorphism ${\alpha } \colon I\to {\mathord {\mathsf{Fun}}}(A,B)$, which similarly internalizes to define a functor ${\ulcorner {\alpha }\urcorner } \colon A \to B^I$.

We now begin to relate the simplicially enriched structures of an $\infty $-cosmos to the 2-categorical structures in its homotopy 2-category by proving that homotopy 2-categories inherit products from their $\infty $-cosmoi that satisfy a 2-categorical universal property. To illustrate, recall that the terminal $\infty $-category $1 \in {\mathord {\mathcal{K}}}$ has the universal property ${\mathord {\mathsf{Fun}}}(X,1) \cong [0]$ for all $X \in {\mathord {\mathcal{K}}}$. Applying the homotopy category functor we see that $1 \in \mathfrak {h}{\mathord {\mathcal{K}}}$ has the universal property ${\mathord {\mathsf{hFun}}}(X,1) \cong [0]$ for all $X \in \mathfrak {h}{\mathord {\mathcal{K}}}$, which is expressed by saying that the $\infty $-category $1$ defines a 2-terminal object in the homotopy 2-category. This 2-categorical universal property has both a 1-dimensional and a 2-dimensional aspect. Since ${\mathord {\mathsf{hFun}}}(X,1)\cong [0]$ is a category with a single object, there exists a unique morphism $X \to 1$ in ${\mathord {\mathcal{K}}}$, and since ${\mathord {\mathsf{hFun}}}(X,1)\cong [0]$ has only a single morphism, the only 2-cells in $\mathfrak {h}{\mathord {\mathcal{K}}}$ with codomain 1 are identities.

Proposition 1.7.6 cartesian (closure)

$\quad $

The homotopy 2-category of any $\infty $-cosmos has 2-categorical products.
The homotopy 2-category of a cartesian closed $\infty $-cosmos is cartesian closed as a 2-category.

Proof ▶

While the functor ${\mathord {\mathsf{h}}}\colon {\mathord {\mathcal{sSet}}}\to {\mathord {\mathcal{Cat}}}$ only preserves finite products, the restricted functor ${\mathord {\mathsf{h}}}\colon {\mathord {\mathcal{QCat}}}\to {\mathord {\mathcal{Cat}}}$ preserves all products on account of the simplified description of the homotopy category of a quasi-category given in Lemma 1.2.28. Thus for any set $I$ and family of $\infty $-categories $(A_i)_{i \in I}$ in ${\mathord {\mathcal{K}}}$, the homotopy category functor carries the isomorphism of functor spaces to an isomorphism of hom-categories

$\begin{tikzcd} [column sep=small] \Fun(X,\prod_{i \in I} A_i) \arrow[r, "\cong"] & \prod_{i \in I} \Fun(X,A_i) & \arrow[r, maps to, "\ho"] & ~ & \hFun(X,\prod_{i \in I} A_i) \arrow[r, "\cong"] & \prod_{i \in I} \hFun(X,A_i). \end{tikzcd}$

This proves that the homotopy 2-category $\mathfrak {h}{\mathord {\mathcal{K}}}$ has products whose universal properties have both a 1- and 2-dimensional component, as described in the empty case for terminal objects above.

If ${\mathord {\mathcal{K}}}$ is a cartesian closed $\infty $-cosmos, then for any triple of $\infty $-categories $A,B,C \in {\mathord {\mathcal{K}}}$ there exist exponential objects $C^A, C^B \in {\mathord {\mathcal{K}}}$ characterized by natural isomorphisms

\[ {\mathord {\mathsf{Fun}}}(A \times B, C) \cong {\mathord {\mathsf{Fun}}}(A, C^B) \cong {\mathord {\mathsf{Fun}}}(B,C^A). \]

Passing to homotopy categories we have natural isomorphisms

\[ {\mathord {\mathsf{hFun}}}(A \times B, C) \cong {\mathord {\mathsf{hFun}}}(A, C^B) \cong {\mathord {\mathsf{hFun}}}(B,C^A), \]

which demonstrates that $\mathfrak {h}{\mathord {\mathcal{K}}}$ is cartesian closed as a 2-category: functors $A \times B \to C$ transpose to define functors $A \to C^B$ and $B \to C^A$, and natural transformations transpose similarly.

There is a standard definition of isomorphism between two objects in any 1-category, preserved by any functor. Similarly, there is a standard definition of equivalence between two objects in any 2-category, preserved by any 2-functor:

Definition 1.7.7 equivalence

An equivalence in a 2-category is given by

a pair of objects $A$ and $B$;
a pair of 1-cells $f \colon A \to B$ and $g \colon B \to A$; and
a pair of invertible 2-cells

$\begin{tikzcd} [column sep=large] A \arrow[r, bend left=25, equals] \arrow[r, bend right=25, "gf"'] \arrow[r, phantom, "{\scriptstyle\cong\Downarrow\alpha}"] & A & \text{and} & B \arrow[r, bend right=25, equals] \arrow[r, bend left=25, "fg"] \arrow[r, phantom, "{\scriptstyle\cong\Downarrow\beta}"] & B \end{tikzcd}$

When $A$ and $B$ are equivalent, we write $A \simeq B$ and refer to the 1-cells $f$ and $g$ as equivalences, denoted by “$\rightsquigarrow $.”

In the case of the homotopy 2-category of an $\infty $-cosmos we have a competing definition of equivalence from 1.4.1: namely a 1-cell $f \colon A \rightsquigarrow B$ that induces an equivalence $f_* \colon {\mathord {\mathsf{Fun}}}(X,A) \rightsquigarrow {\mathord {\mathsf{Fun}}}(X,B)$ on functor spaces — or equivalently, by Lemma 1.4.9, a homotopy equivalence defined relative to the interval $I$. Crucially, all three notions of equivalence coincide:

Theorem 1.7.8 equivalences are equivalences

In any $\infty $-cosmos ${\mathord {\mathcal{K}}}$, the following are equivalent and characterize what it means for a functor $f \colon A \to B$ between $\infty $-categories to define an equivalence.

For all $X \in {\mathord {\mathcal{K}}}$, the post-composition map $f_* \colon {\mathord {\mathsf{Fun}}}(X,A) \rightsquigarrow {\mathord {\mathsf{Fun}}}(X,B)$ defines an equivalence of quasi-categories.
There exists a functor $g \colon B \to A$ and natural isomorphisms $\alpha \colon \textup{id}_A \cong gf$ and $\beta \colon fg \cong \textup{id}_B$ in the homotopy 2-category.
There exists a functor $g \colon B \to A$ and maps

$\begin{tikzcd} & A & & & B \\ A \arrow[ur, equals] \arrow[dr, "gf"'] \arrow[r, "\alpha"] & A^\iso \arrow[u, two heads, "\sim", "\ev_0"'] \arrow[d, two heads, "\sim"', "\ev_1"] &\text{and} & B \arrow[dr, equals] \arrow[r, "\beta"] \arrow[ur, "fg"] & B^\iso \arrow[u, two heads, "\sim", "\ev_0"'] \arrow[d, two heads, "\sim"', "\ev_1"] \\ & A & & & B \end{tikzcd}$

in the $\infty $-cosmos ${\mathord {\mathcal{K}}}$.

As an illustrative comparison of 2-categorical and quasi-categorical techniques, rather than appealing to Lemma 1.4.9 to prove i$\Leftrightarrow $iii, we re-prove it.

Proof ▶

For i$\Rightarrow $ii, if the induced map $f_* \colon {\mathord {\mathsf{Fun}}}(X,A) \rightsquigarrow {\mathord {\mathsf{Fun}}}(X,B)$ defines an equivalence of quasi-categories then the functor $f_* \colon {\mathord {\mathsf{hFun}}}(X,A) \rightsquigarrow {\mathord {\mathsf{hFun}}}(X,B)$ defines an equivalence of categories, by Lemma 1.2.36. In particular, the equivalence $f_* \colon {\mathord {\mathsf{hFun}}}(B,A) \rightsquigarrow {\mathord {\mathsf{hFun}}}(B,B)$ is essentially surjective so there exists $g \in {\mathord {\mathsf{hFun}}}(B,A)$ and an isomorphism $\beta \colon fg \cong \textup{id}_B \in {\mathord {\mathsf{hFun}}}(B,B)$. Now since $f_* \colon {\mathord {\mathsf{hFun}}}(A,A) \rightsquigarrow {\mathord {\mathsf{hFun}}}(A,B)$ is fully faithful, the isomorphism $\beta f \colon fgf \cong f \in {\mathord {\mathsf{hFun}}}(A,B)$ can be lifted to define an isomorphism $\alpha ^{-1} \colon gf \cong \textup{id}_A \in {\mathord {\mathsf{hFun}}}(A,A)$. This defines the data of a 2-categorical equivalence in Definition 1.7.7.

To see that ii$\Rightarrow $iii recall from Lemma 1.7.5 that the natural isomorphisms $\alpha \colon \textup{id}_A \cong gf$ and $\beta \colon fg \cong \textup{id}_B$ in $\mathfrak {h}{\mathord {\mathcal{K}}}$ are represented by maps $\alpha \colon A \to A^I$ and $\beta \colon B \to B^I$ in ${\mathord {\mathcal{K}}}$ as in Lemma 1.4.9.

Finally, iii$\Rightarrow $i since ${\mathord {\mathsf{Fun}}}(X,-)$ carries the data of iii to the data of an equivalence of quasi-categories as in Definition 1.2.35.

It is hard to overstate the importance of Theorem 1.7.8 for the work that follows. The categorical constructions that we introduce for $\infty $-categories, $\infty $-functors, and $\infty $-natural transformations are invariant under 2-categorical equivalence in the homotopy 2-category and the universal properties we develop similarly characterize 2-categorical equivalence classes of $\infty $-categories. Theorem 1.7.8 then asserts that such constructions are “homotopically correct”: both invariant under equivalence in the $\infty $-cosmos and precisely identifying equivalence classes of objects.

The equivalence invariance of the functor space in the codomain variable is axiomatic, but equivalence invariance in the domain variable is not. ¹ Nor is it evident how this could be proven from either i or iii of Theorem 1.7.8. But using ii and 2-categorical techniques, there is now a short proof.

Corollary 1.7.9

Equivalences of $\infty $-categories $A' \rightsquigarrow A$ and $B \rightsquigarrow B'$ induce an equivalence of functor spaces ${\mathord {\mathsf{Fun}}}(A,B) \rightsquigarrow {\mathord {\mathsf{Fun}}}(A',B')$.

Proof ▶

The representable simplicial functors ${\mathord {\mathsf{Fun}}}(A,-)\colon {\mathord {\mathcal{K}}}\to {\mathord {\mathcal{QCat}}}$ and ${\mathord {\mathsf{Fun}}}(-,B)\colon {\mathord {\mathcal{K}}}^{\mathord {\textup{op}}}\to {\mathord {\mathcal{QCat}}}$ induce 2-functors ${\mathord {\mathsf{Fun}}}(A,-)\colon \mathfrak {h}{\mathord {\mathcal{K}}}\to \mathfrak {h}{\mathord {\mathcal{QCat}}}$ and ${\mathord {\mathsf{Fun}}}(-,B)\colon \mathfrak {h}{\mathord {\mathcal{K}}}^{\mathord {\textup{op}}}\to \mathfrak {h}{\mathord {\mathcal{QCat}}}$, which preserve the 2-categorical equivalences of Definition 1.7.7. By Theorem 1.7.8 this is what we wanted to show.

There is also a standard 2-categorical notion of an isofibration, defined in the statement of Proposition 1.7.10. We now show that any isofibration in an $\infty $-cosmos defines an isofibration in its homotopy 2-category.

Proposition 1.7.10 isofibrations are isofibrations

An isofibration $p \colon E \twoheadrightarrow B$ in an $\infty $-cosmos ${\mathord {\mathcal{K}}}$ also defines an isofibration in the homotopy 2-category $\mathfrak {h}{\mathord {\mathcal{K}}}$: given any invertible 2-cell as displayed below-left abutting to $B$ with a specified lift of one of its boundary 1-cells through $p$, there exists an invertible 2-cell abutting to $E$ with this boundary 1-cell as displayed below-right that whiskers with $p$ to the original 2-cell.

$\begin{tikzcd} X \arrow[r, "e"] \arrow[dr, bend right, "b"'] & E \arrow[d, two heads, "p"] \arrow[dl, phantom, "{\scriptstyle\cong\Downarrow\beta}" near start] &\arrow[d, phantom, "="] & X \arrow[rr, start anchor=15, end anchor=165, bend left=20, "e"] \arrow[rr, start anchor=345, end anchor=195, bend right=20, "\bar{e}"', dashed] \arrow[rr, phantom, "{\scriptstyle\cong\Downarrow\gamma}"] && E \arrow[d, two heads, "p"] \\ ~ & B & ~ & & & B \end{tikzcd}$

Proof ▶

The universal property of the statement says that the functor

\[ p_* \colon {\mathord {\mathsf{hFun}}}(X,E) \twoheadrightarrow {\mathord {\mathsf{hFun}}}(X,B) \]

is an isofibration of categories in the sense defined in Proposition 1.5.2. By axiom 1.4.1 ii, since $p \colon E \twoheadrightarrow B$ is an isofibration in ${\mathord {\mathcal{K}}}$, the induced map $p_* \colon {\mathord {\mathsf{Fun}}}(X,E) \twoheadrightarrow {\mathord {\mathsf{Fun}}}(X,B)$ is an isofibration of quasi-categories. So it suffices to show that the functor ${\mathord {\mathsf{h}}}\colon {\mathord {\mathcal{QCat}}}\to {\mathord {\mathcal{Cat}}}$ carries isofibrations of quasi-categories to isofibrations of categories.

So let us now consider an isofibration $p \colon E \twoheadrightarrow B$ between quasi-categories. By Proposition 1.2.32, every isomorphism $\beta $ in the homotopy category ${\mathord {\mathsf{h}}}{B}$ of the quasi-category $B$ is represented by a simplicial map $\beta \colon I\to B$. By Definition 1.2.34, the lifting problem

$\begin{tikzcd} \catone \arrow[r, "e"] \arrow[d, hook] & E \arrow[d, two heads, "p"] \\ \iso \arrow[ur, dashed, "\gamma"] \arrow[r, "\beta"'] & B \end{tikzcd}$

can be solved, and the map $\gamma \colon I\to E$ so produced represents a lift of the isomorphism from ${\mathord {\mathsf{h}}}{B}$ to an isomorphism in ${\mathord {\mathsf{h}}}{E}$ with domain $e$.

Convention 1.7.11 on isofibrations in homotopy 2-categories

Since the converse to Proposition 1.7.10 does not hold, there is a potential ambiguity when using the term “isofibration” to refer to a map in the homotopy 2-category of an $\infty $-cosmos. We adopt the convention that when we declare a map in $\mathfrak {h}{\mathord {\mathcal{K}}}$ to be an isofibration we always mean this is the stronger sense of defining an isofibration in ${\mathord {\mathcal{K}}}$. This stronger condition gives us access to the 2-categorical lifting property of Proposition 1.7.10 and also to homotopical properties axiomatized in Definition 1.4.1, which ensure that the strictly defined limits of 1.4.1 i are automatically equivalence invariant constructions (see [ RV22 , 6.2.8, § C.1 ] ).

We conclude this chapter with a final definition that can be extracted from the homotopy 2-category of an $\infty $-cosmos. The 1- and 2-cells in the homotopy 2-category from the terminal $\infty $-category $1 \in {\mathord {\mathcal{K}}}$ to a generic $\infty $-category $A \in {\mathord {\mathcal{K}}}$ define the objects and morphisms in the homotopy category of the $\infty $-category $A$.

Definition 1.7.12 homotopy category of an $\infty $-category

The homotopy category of an $\infty $-category $A$ in an $\infty $-cosmos ${\mathord {\mathcal{K}}}$ is defined to be the homotopy category of its underlying quasi-category, that is:

\[ {\mathord {\mathsf{h}}}A :={\mathord {\mathsf{hFun}}}(1,A) :={\mathord {\mathsf{h}}}({\mathord {\mathsf{Fun}}}(1,A)). \]

As we shall discover, homotopy categories generally inherit “derived” analogues of structures present at the level of $\infty $-categories.