Kerodon

Proof. The $2$-category $\operatorname{\mathcal{C}}$ is a $2$-groupoid if and only if it is a $(2,1)$-category and the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ is a groupoid (Remark 2.2.8.25). The first condition is equivalent to the requirement that $\operatorname{N}_{\bullet }^{\operatorname{D}}(\operatorname{\mathcal{C}})$ is an $\infty $-category (Theorem 2.3.2.1). If this condition is satisfied, then Corollary 2.3.4.6 supplies an isomorphism $\mathrm{h} \mathit{\operatorname{\mathcal{C}}} \simeq \mathrm{h} \mathit{ \operatorname{N}_{\bullet }^{\operatorname{D}}(\operatorname{\mathcal{C}}) }$. The desired equivalence now follows from Proposition 4.4.2.1. $\square$

Proof. Combine Proposition 4.4.2.1 with Remark 4.2.1.8. $\square$

Proof. Without loss of generality, we may assume that $q$ is a left fibration. By virtue of Remark 3.1.3.11, the simplicial set $\operatorname{Fun}_{A/ \, /S}( B, X)$ can be identified with a fiber of the restriction map

Proposition 4.2.5.1 asserts that $\theta $ is a left fibration of simplicial sets, so its fibers are Kan complexes (Corollary 4.4.2.3). If $i$ is left anodyne, then $\theta $ is a trivial Kan fibration (Proposition 4.2.5.4), so its fibers are contractible Kan complexes. $\square$

Proof. Apply Corollary 4.4.2.4 in the special case $A = \emptyset $. $\square$

Proof of Proposition 4.4.2.1 from Theorem 4.4.2.6. Let $X$ be a simplicial set. By definition, the projection map $X \rightarrow \Delta ^{0}$ is a left fibration if and only if, for every pair of integers $0 \leq i < n$, every morphism of simplicial sets $\sigma _0: \Lambda ^{n}_{i} \rightarrow X$ can be extended to an $n$-simplex $\sigma : \Delta ^ n \rightarrow X$. This condition is automatically satisfied when $n=1$ (we can identify $\sigma _0$ with a vertex $x \in X$, and take $\sigma $ to be the degenerate edge $\operatorname{id}_{x}$), and is satisfied for $0 < i < n$ if and only if $X$ is an $\infty $-category. Assuming that $X$ is an $\infty $-category, it is satisfied for $i = 0$ if and only if every morphism in $X$ is an isomorphism (by virtue of Theorem 4.4.2.6). This proves the equivalence $(d) \Leftrightarrow (e)$, and the equivalence $(d) \Leftrightarrow (f)$ follows by applying the same reasoning to the opposite simplicial set $X^{\operatorname{op}}$. In particular, $(e)$ and $(f)$ are equivalent to one another, and therefore equivalent to $(a)$ (see Example 4.2.1.5). The equivalences $(a) \Leftrightarrow (b)$ and $(c) \Leftrightarrow (d)$ are immediate from the definitions. $\square$

Proof. Without loss of generality, we may assume that $F$ is a left fibration. Let $u: X \rightarrow Y$ be a morphism in $\operatorname{\mathcal{C}}$, and suppose that $F(u)$ is an isomorphism in $\operatorname{\mathcal{D}}$. Let $\overline{v}: F(Y) \rightarrow F(X)$ is a homotopy inverse to $F(u)$, so that there exists a $2$-simplex $\overline{\sigma }$ of $\operatorname{\mathcal{D}}$ as depicted in the following diagram:

Invoking our assumption that $F$ is a left fibration, we can lift $\overline{\sigma }$ to a diagram

in the $\infty $-category $\operatorname{\mathcal{C}}$. This lift supplies a morphism $v: Y \rightarrow X$ and witnesses $\operatorname{id}_{X}$ as a composition of $v$ with $u$, so that $v$ is a left homotopy inverse to $u$. Moreover, the image $F(v) = \overline{v}$ is an isomorphism in $\operatorname{\mathcal{D}}$. Repeating the preceding argument (with $u: X \rightarrow Y$ replaced by $v: Y \rightarrow X$), we deduce that there exists a morphism $w: X \rightarrow Y$ which is left homotopy inverse to $v$. It follows that $u$ and $w$ are homotopic, so that $v$ is a homotopy inverse to $u$ (Remark 1.4.6.6). In particular, $u$ is an isomorphism. $\square$

Proof. We will show that the functor $F_{/q}$ is conservative; the conservativity of $F_{q/}$ follows by a similar argument. Let $\pi : \operatorname{\mathcal{C}}_{/q} \rightarrow \operatorname{\mathcal{C}}$ and $\pi ': \operatorname{\mathcal{D}}_{/(F \circ q)} \rightarrow \operatorname{\mathcal{D}}$ denote the projection maps. Then $\pi $ and $\pi '$ are right fibrations of $\infty $-categories (Proposition 4.3.6.1), and therefore conservative (Proposition 4.4.2.11). Since $F$ is conservative, from Remark 4.4.2.10 that the functor $F \circ \pi = \pi ' \circ F_{/q}$ is also conservative. Applying Remark 4.4.2.10 again, we conclude that $F_{/q}$ is conservative. $\square$

Proof. Using Lemma 4.3.6.16, we can identify the horn $\Lambda ^{n}_{n}$ with the pushout

Set $f= \sigma _0|_{ \Delta ^{n-2} }$ and $f_0 = \sigma _0|_{ \operatorname{\partial \Delta }^{n-2} }$, and let $\operatorname{\mathcal{E}}$ denote the fiber product $\operatorname{\mathcal{C}}_{f_0/} \times _{\operatorname{\mathcal{D}}_{ (q \circ f_0)/}} \operatorname{\mathcal{D}}_{( q \circ f)/}$. Note that there is an evident projection map $\theta : \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, given by the composition

The morphism $\theta ''$ is a left fibration (Proposition 4.3.6.1), and the morphism $\theta '$ is a pullback of the restriction map $\operatorname{\mathcal{D}}_{(q \circ f)/} \rightarrow \operatorname{\mathcal{D}}_{(q \circ f_0)/}$ and is therefore also a left fibration (Corollary 4.3.6.14). It follows that $\theta : \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a left fibration (Remark 4.2.1.11), and in particular $\operatorname{\mathcal{E}}$ is an $\infty $-category (Remark 4.1.1.9).

Note that the restriction of $\sigma _0$ to $\Delta ^{n-2} \star \{ 1\} $ can be identified with an object $Y$ of the coslice $\infty $-category $\operatorname{\mathcal{C}}_{f/}$. Let

be the left fibration of Proposition 4.3.6.8, and set $\overline{Y} = \rho (Y) \in \operatorname{\mathcal{E}}$. Then the restriction $\sigma _0|_{ \operatorname{\partial \Delta }^{n-2} \star \Delta ^1}$ and $\overline{\sigma }$ determine a morphism $\overline{v}: \overline{X} \rightarrow \overline{Y}$ in the $\infty $-category $\operatorname{\mathcal{E}}$. Unwinding the definitions, we see that choosing an $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ satisfying the requirements of Proposition 4.4.2.13 is equivalent to choosing a morphism $v: X \rightarrow Y$ in $\operatorname{\mathcal{C}}_{f/}$ satisfying $\rho (v) = \overline{v}$. Since $\rho $ is a left fibration, it is an isofibration (Example 4.4.1.11). Consequently, to prove the existence of $v$, it will suffice to show that $\overline{v}$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}$. Since $\theta $ is a left fibration, this follows from our assumption that $u = \theta ( \overline{v} )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$ (Proposition 4.4.2.11). $\square$

Proof of Theorem 4.4.2.6. The implication $(1) \Rightarrow (3)$ is a special case of Proposition 4.4.2.13. We will complete the proof by showing that $(3) \Rightarrow (1)$ (a similar argument shows that $(1)$ and $(2)$ are equivalent). Let $u: X \rightarrow Y$ be a morphism in an $\infty $-category $\operatorname{\mathcal{C}}$, and consider the map $\sigma _0: \Lambda ^{2}_{2} \rightarrow \operatorname{\mathcal{C}}$ depicted in the diagram

If $u$ satisfies condition $(3)$, then we can complete $\sigma _0$ to a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$, which witnesses the morphism $v = d^{2}_2(\sigma )$ as a right homotopy inverse of $u$. The tuple $(\sigma , s^{1}_0(u), s^{1}_1(u), \bullet )$ then determines a morphism of simplicial sets $\tau _0: \Lambda ^3_3 \rightarrow \operatorname{\mathcal{C}}$ (see Proposition 1.2.4.7). Invoking assumption $(3)$ again, we can extend $\tau _0$ to a $3$-simplex $\tau $ of $\operatorname{\mathcal{C}}$. The face $d^{3}_3(\tau )$ then witnesses that $v$ is also a left homotopy inverse to $u$, so that $u$ is an isomorphism as desired. $\square$

Proof. When $n=0$, the desired result follows from the fact that the fiber $X_{s}$ is nonempty. We may therefore assume without loss of generality that $n > 0$. Replacing $q$ by the projection map $\Delta ^{n} \times _{S} X \rightarrow \Delta ^ n$, we may further reduce to the special case where $S = \Delta ^ n$ and $\overline{\sigma }$ is the identity map. In this case, our assumption that $q$ is a left fibration guarantees that $X$ is an $\infty $-category (Remark 4.1.1.9).

Let $\overline{h}: \Delta ^{1} \times \Delta ^{n} \rightarrow \Delta ^ n$ be the morphism given on vertices by $h(i,j) = \begin{cases} j & \textnormal{ if } i=0 \\ n & \textnormal{ if } i=1. \end{cases}$ Since the inclusion $\{ 0\} \times \operatorname{\partial \Delta }^ n \hookrightarrow \Delta ^1 \times \operatorname{\partial \Delta }^{n}$ is left anodyne (Proposition 4.2.5.3), our assumption that $q$ is a left fibration guarantees the existence of a morphism $h': \Delta ^1 \times \operatorname{\partial \Delta }^ n \rightarrow X$ satisfying $h'|_{ \{ 0\} \times \operatorname{\partial \Delta }^ n} = \sigma _0$ and $q \circ h' = \overline{h}|_{ \Delta ^1 \times \operatorname{\partial \Delta }^ n}$. We will complete the proof by showing that $h'$ can be extended to a map $h: \Delta ^1 \times \Delta ^ n \rightarrow X$ satisfying $q \circ h = \overline{h}$ (in this case, our original lifting problem admits the solution $\sigma = h|_{ \{ 0\} \times \Delta ^ n}$).

Let $Y(0) \subset Y(1) \subset Y(2) \subset \cdots \subset Y(n+1) = \Delta ^1 \times \Delta ^ n$ denote the filtration constructed in the proof of Lemma 3.1.2.12. Then $Y(0)$ can be described as the pushout

Using our assumption that the fiber $X_{s}$ is a contractible Kan complex, we see that $h'$ can be extended to a morphism of simplicial sets $h_0: Y(0) \rightarrow X$ satisfying $q \circ h_0 = \overline{h}|_{Y(0)}$. We claim that $h_0$ can be extended to a compatible sequence of maps $h_{i}: Y(i) \rightarrow X$ satisfying $q \circ h_ i = \overline{h}|_{Y(i)}$. To prove this, we recall that each $Y(i+1)$ can be realized as a pushout of the horn inclusion $\Lambda ^{n+1}_{i+1} \hookrightarrow \Delta ^{n+1}$, so that the construction of $h_{i+1}$ from $h_{i}$ can be rephrased as a lifting problem

For $0 \leq i < n$, this lifting problem is automatically solvable by virtue of our assumption that $q$ is a left fibration. In the case $i = n$, the edge

is an edge of the Kan complex $X_{s}$, and is therefore an isomorphism in the $\infty $-category $X$ (Proposition 1.4.6.10). In this case, the existence of the desired extension follows from Theorem 4.4.2.6. We complete the proof by taking $h = h_{n+1}$. $\square$

Proof of Proposition 4.4.2.14. The implication $(1) \Rightarrow (2)$ is immediate, and the converse follows from Lemma 4.4.2.15. The equivalence $(1) \Leftrightarrow (3)$ follows by a similar argument. $\square$