Proposition 7.7.6.5. Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{E}}' \ar [rr]^{\Gamma } \ar [dr]_{U'} & & \operatorname{\mathcal{E}}\ar [dl]^{U} \\ & \operatorname{\mathcal{C}}& } \]
where $U$ and $U'$ are left fibrations and $\Gamma $ is an isofibration. Let $\mathscr {F} = \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ and $\mathscr {F}' = \operatorname{Tr}_{\operatorname{\mathcal{E}}' / \operatorname{\mathcal{C}}}$ be covariant transport representations for $U$ and $U'$, respectively, and suppose that $\Gamma $ is compatible with a natural transformation $\gamma : \mathscr {F}' \rightarrow \mathscr {F}$ (see Definition 7.4.2.2). The following conditions are equivalent:
- $(1)$
The morphism $\Gamma $ is a Kan fibration of simplicial sets.
- $(2)$
Composition with $\Gamma $ induces a trivial Kan fibration
\[ \theta : \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}' ) \rightarrow \operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{E}}') \times _{ \operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{E}}) } \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}). \]
- $(3)$
For every edge $u$ of $\operatorname{\mathcal{C}}$, composition with $\Gamma $ induces a homotopy equivalence
\[ \theta _{u}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \Delta ^1, \operatorname{\mathcal{E}}' ) \rightarrow \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}}). \]
- $(4)$
For every edge $u$ of $\operatorname{\mathcal{C}}$, the diagram of Kan complexes
7.91
\begin{equation} \begin{gathered}\label{equation:cartesian-transformation-in-spaces} \xymatrix { \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \Delta ^1, \operatorname{\mathcal{E}}' ) \ar [r]^{\Gamma \circ } \ar [d] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \Delta ^1, \operatorname{\mathcal{E}}) \ar [d] \\ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \{ 1\} , \operatorname{\mathcal{E}}' ) \ar [r]^{\Gamma \circ } & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \{ 1\} , \operatorname{\mathcal{E}}) } \end{gathered} \end{equation}
- $(5)$
The natural transformation $\gamma $ is cartesian.
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$