Kerodon

Proof. Assume that $\iota '$ is a weak homotopy equivalence; we will show that $\overline{U}$ is a Kan fibration (the converse is a special case of Corollary 3.3.7.4). Using Proposition 3.1.7.1, we can factor $\iota \circ U$ as a composition $\operatorname{\mathcal{E}}' \xrightarrow {\iota ''} \overline{\operatorname{\mathcal{E}}}'' \xrightarrow {\overline{V}} \overline{\operatorname{\mathcal{E}}}$, where $\iota ''$ is inner anodyne and $V$ is a Kan fibration. Our assumption that $\iota '$ is a weak homotopy equivalence guarantees that the lifting problem

admits a solution. To show that $\overline{U}$ is a Kan fibration, it will suffice to show that $F$ is an equivalence of left fibrations over $\overline{\operatorname{\mathcal{E}}}$ (Proposition 5.1.7.14). Using the criterion of Corollary 5.1.7.16, we are reduced to proving that for every vertex $X \in \overline{\operatorname{\mathcal{E}}}$, the induced map

is a homotopy equivalence. We consider two cases:

• Suppose that $X$ belongs to the image of $\iota $. In this case, the desired result follows by applying Proposition 3.2.8.1 to the diagram

  \[ \xymatrix { \operatorname{\mathcal{E}}' \ar [d]^{U} \ar [r]^{ \iota '' } & \overline{\operatorname{\mathcal{E}}}'' \ar [d]^{V} \\ \operatorname{\mathcal{E}}\ar [r]^{\iota } & \overline{\operatorname{\mathcal{E}}}, } \]

  since the vertical maps are Kan fibrations and the horizontal maps are weak homotopy equivalences.

• Suppose that $X$ does not belong to the image of $\iota $: that is, it lies over the cone point $C \in \operatorname{\mathcal{C}}^{\triangleright }$. Set $\overline{\operatorname{\mathcal{E}}}_{C} = \{ C\} \times _{ \operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ and define $\overline{\operatorname{\mathcal{E}}}'_{C}$ and $\overline{\operatorname{\mathcal{E}}}''_{C}$ similarly, so that we have a commutative diagram

  \[ \xymatrix { \overline{\operatorname{\mathcal{E}}}'_{C} \ar [r]^{ F_{C} } \ar [d]^{U_{C}} & \overline{\operatorname{\mathcal{E}}}''_{C} \ar [d]^{V_{C}} \\ \overline{\operatorname{\mathcal{E}}}_{C} \ar@ {=}[r] & \overline{\operatorname{\mathcal{E}}}_{C} } \]

  The morphisms $U_{C}$ and $V_{C}$ are pullbacks of $U$ and $V$ respectively, and are therefore left fibrations. Assumption $(a)$ guarantees that the simplicial set $\overline{\operatorname{\mathcal{E}}}_{C}$ is a Kan complex (Proposition 4.4.2.1), so that $U$ and $V$ are Kan fibrations (Corollary 4.4.3.8). Consequently, to show that $F_{X}$ is a homotopy equivalence, it will suffice to show that $F_{C}$ is a homotopy equivalence (Proposition 3.2.8.1). By construction, we have a pullback diagram of simplicial sets

  \[ \xymatrix { \overline{\operatorname{\mathcal{E}}}'_{C} \ar [r]^{F_ C} \ar [d] & \overline{\operatorname{\mathcal{E}}}''_{C} \ar [d] \\ \overline{\operatorname{\mathcal{E}}}' \ar [r]^{ F } & \overline{\operatorname{\mathcal{E}}}'', } \]

  where $F$ is a weak homotopy equivalence by construction. We are therefore reduced to showing that the vertical maps in this diagram are weak homotopy equivalences. In fact, the vertical maps are right anodyne, since they arise as the pullback of the right anodyne inclusion $\{ C\} \hookrightarrow \operatorname{\mathcal{C}}^{\triangleright }$ along left fibrations (Corollary 7.2.3.13).

Proof. Assume that $\Gamma $ is an isofibration; we will show that it is a left fibration (the reverse implication follows from Corollary 5.6.7.5). Let $\iota : A \hookrightarrow B$ be a left anodyne map of simplicial sets; we wish to show that every lifting problem

admits a solution. Let us regard the upper horizontal map and the underlying morphism $B \rightarrow \operatorname{\mathcal{C}}$ as fixed, and let

be the morphism given by composition with $\Gamma $. Since $U$ and $U'$ are left fibrations, the source and target of $V$ are contractible Kan complexes (Proposition 4.2.5.4); in particular, $V$ is a categorical equivalence of simplicial sets. Since $\Gamma $ is an isofibration, $V$ is also an isofibration (see Proposition 4.5.5.14), and is therefore a trivial Kan fibration (Proposition 4.5.5.20). In particular, $V$ is surjective on vertices, which guarantees that the lifting problem ( 7.90) admits a solution. $\square$

Proof. It follows from Lemma 7.7.6.3 that $\Gamma $ is a left fibration of simplicial sets. Consequently, it is a Kan fibration if and only if it also a right fibration (Example 4.2.1.5). The equivalence of $(1)$ and $(2)$ now follows from Proposition 4.2.6.1. Note that the morphism $\theta $ is automatically a left fibration of simplicial sets (Proposition 4.2.5.1), and is therefore a trivial Kan fibration if and only if it has contractible fibers (Proposition 4.4.2.14). Note that every fiber of $\theta $ also appears as a fiber of $\theta _{u}$, for some edge $u: C \rightarrow D$ of $\operatorname{\mathcal{C}}$. Consequently, condition $(2)$ is equivalent to the requirement that each of the morphisms $\theta _{u}$ has contractible fibers. Note that the restriction map $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \Delta ^1, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \{ 1\} , \operatorname{\mathcal{E}})$ is a left fibration whose target is a Kan complex, and is therefore a Kan fibration (Corollary 4.4.3.8). The equivalence $(3) \Leftrightarrow (4)$ now follows from Example 3.4.1.3. It also follows that the fiber product $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \{ 1\} , \operatorname{\mathcal{E}}') \times _{ \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \{ 1\} , \operatorname{\mathcal{E}}) } \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \Delta ^1, \operatorname{\mathcal{E}})$ is a Kan complex, so that $\theta _{u}$ is a Kan fibration (Corollary 4.4.3.8). The equivalence $(2) \Leftrightarrow (3)$ now follows from Proposition 3.2.7.2.

To complete the proof, it will suffice to show that for each edge $u: C \rightarrow D$ as above, the following conditions are equivalent:

$(4_ u)$

The diagram of Kan complexes (7.91) is a homotopy pullback square.

$(5_ u)$

The natural transformation $\gamma $ carries $u$ to a pullback diagram

7.92

\begin{equation} \begin{gathered}\label{equation:cartesian-transformation-in-spaces2} \xymatrix { \mathscr {F}(C) \ar [d]^{\mathscr {F}(u) } \ar [r]^{ \gamma _{C} } & \mathscr {F}'(C) \ar [d]^{ \mathscr {F}'(u) } \\ \mathscr {F}(D) \ar [r]^{\gamma _{D}} & \mathscr {F}'(D) } \end{gathered} \end{equation}

in the $\infty $-category $\operatorname{\mathcal{S}}$ of spaces.

To see this, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^1$ and that $u$ is the nondegenerate edge of $\operatorname{\mathcal{C}}$. In particular, $\operatorname{\mathcal{C}}$ can be identified with the nerve of the ordinary category $\operatorname{\mathcal{C}}_0 = [1]$. Applying Example 7.4.2.12, we may assume that $\gamma $ is given by applying the (homotopy coherent) nerve construction to the map of strict transport representations $\operatorname{sTr}_{\operatorname{\mathcal{E}}'/ \operatorname{\mathcal{C}}_0 } \rightarrow \operatorname{sTr}_{\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}_0 }$ determined by $\Gamma $. In particular, the diagram (7.92) in the $\infty $-category $\operatorname{\mathcal{S}}$ is obtained from the strictly commutative diagram of Kan complexes (7.91). The equivalence $(4_ u) \Leftrightarrow (5_ u)$ now follows from Example 7.6.3.2. $\square$

Proof. Write $\overline{\mathscr {F}}$ and $\overline{\mathscr {F}}'$ as the covariant transport representations of left fibrations $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ and $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$, respectively. By virtue of Theorem 7.4.2.4, there exists a morphism $\overline{\Gamma } \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleright } }( \overline{\operatorname{\mathcal{E}}}', \overline{\operatorname{\mathcal{E}}} )$ which is compatible with $\overline{\gamma }$, in the sense of Definition 7.4.2.2. Replacing $\overline{U}'$ with an equivalent left fibration if necessary, we may assume that $\overline{\Gamma }$ is an isofibration (Remark 7.7.6.4), and therefore a left fibration (Lemma 7.7.6.3). Set $\operatorname{\mathcal{E}}= \operatorname{\mathcal{C}}\times _{ \operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ and $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}\otimes _{ \operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}'$, so that $\overline{\Gamma }$ restricts to a left fibration $\Gamma : \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$. Since $\gamma $ is cartesian, Proposition 7.7.6.5 guarantees that $\Gamma $ is a Kan fibration; moreover, $\overline{\gamma }$ is cartesian if and only if $\overline{\Gamma }$ is also a Kan fibration. Since $\overline{\mathscr {F}}$ is a colimit diagram, Corollary 7.4.3.14 guarantees that the inclusion map $\iota : \operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is a weak homotopy equivalence; moreover, $\overline{\mathscr {F}}'$ is a colimit diagram if and only if the inclusion map $\iota ': \operatorname{\mathcal{E}}' \hookrightarrow \overline{\operatorname{\mathcal{E}}}'$ is a weak homotopy equivalence. We are therefore reduced to showing that $\iota '$ is a weak homotopy equivalence if and only if $\overline{\Gamma }$ is a Kan fibration, which is a restatement of Proposition 7.7.6.2. $\square$