# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$

Proposition 5.1.4.16. Suppose we given a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ X \ar [rr]^{f} \ar [dr]_{q_ X} & & Y \ar [dl]^{q_ Y} \\ & S, & }$

where $S$ is a Kan complex. The following conditions are equivalent:

$(1)$

The morphism $f$ is a covariant equivalence relative to $S$.

$(2)$

The morphism $f$ is a contravariant equivalence relative to $S$.

$(3)$

The morphism $f$ is a weak homotopy equivalence.

Proof. The implications $(1) \Rightarrow (3)$ and $(2) \Rightarrow (3)$ follow from Remark 5.1.4.8 (and do not require the assumption that $S$ is a Kan complex). We will complete the proof by establishing the implication $(3) \Rightarrow (1)$ (the proof of the implication $(3) \Rightarrow (2)$ is similar). Assume that $f$ is a weak homotopy equivalence and let $Z \rightarrow S$ be a left fibration; we wish to show that the induced map $\theta : \operatorname{Fun}_{/S}(Y,Z) \rightarrow \operatorname{Fun}_{/S}(X,Z)$ is bijective on connected components. Our assumption that $S$ is a Kan complex guarantees that $q$ is a Kan fibration (Lemma 5.1.2.4), so that $Z$ is also a Kan complex. Consider the diagram of simplicial sets

5.5
\begin{equation} \begin{gathered}\label{equation:covariant-equivalence-over-Kan} \xymatrix@C =50pt@R=50pt{ \operatorname{Fun}(Y,Z) \ar [r]^-{\circ f} \ar [d]^{q \circ } & \operatorname{Fun}(X,Z) \ar [d]^{q \circ } \\ \operatorname{Fun}(Y,S) \ar [r]^-{\circ f} & \operatorname{Fun}(X,S). } \end{gathered} \end{equation}

Our assumption that $f$ is a weak homotopy equivalence guarantees that the horizontal maps in this diagram are homotopy equivalences (Corollary 3.1.6.5), so that diagram (5.5) is a homotopy Cartesian (Corollary 3.4.1.3). Corollary 3.1.3.2 guarantees that the vertical maps in the diagram (5.5) are Kan fibrations. Invoking Example 3.4.1.4, we conclude that the induced map

$\theta : \operatorname{Fun}_{/S}(Y,Z) = \{ q_ Y \} \times _{ \operatorname{Fun}(Y,S)} \operatorname{Fun}(Y,Z) \rightarrow \{ q_ X \} \times _{ \operatorname{Fun}(X,S) } \operatorname{Fun}(X,Z) = \operatorname{Fun}_{/S}(X,Z)$

is also a homotopy equivalence, and is therefore bijective on connected components. $\square$