# Kerodon

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

Remark 5.1.4.15 (Axioms for Covariant Equivalence). Fix a simplicial set $S$. Combining Remark 5.1.4.10, Proposition 5.1.4.13, and Proposition 5.1.4.14, we see that the notion of covariant equivalence (relative to $S$) satisfies the following properties:

$(a)$

If $f: X \rightarrow Y$ and $g: Y \rightarrow Z$ are morphisms in $(\operatorname{Set_{\Delta }})_{/S}$ and two of the morphisms $f$, $g$, and $g \circ f$ are covariant equivalences, then so is the third.

$(b)$

Every left anodyne morphism of $(\operatorname{Set_{\Delta }})_{/S}$ is a covariant equivalence.

$(c)$

If $q_{X}: X \rightarrow S$ and $q_{Y}: Y \rightarrow S$ are left fibrations, then a morphism $f: X \rightarrow Y$ in $(\operatorname{Set_{\Delta }})_{/S}$ is a covariant equivalence if and only if the induced map $f_{s}: X_{s} \rightarrow Y_{s}$ is a homotopy equivalence of Kan complexes, for each $s \in S$.

In fact, the notion of covariant equivalence is completely characterized by $(a)$, $(b)$, and $(c)$. To prove this, suppose we are given an arbitrary commutative diagram of simplicial sets

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

Using Proposition 4.2.2.7, we can factor $q_{Y}$ as a composition $Y \xrightarrow {q'_{Y}} Y' \xrightarrow {q''_{Y} } S$ where $q'_{Y}$ is left anodyne and $q''_{Y}$ is a left fibration. Similarly, we can factor the composite map $q'_{Y} \circ f$ as a composition $X \xrightarrow {q'_{X}} X' \xrightarrow {f'} Y'$, where $q'_{X}$ is left anodyne and $f'$ is a left fibration. We then have a commutative diagram

$\xymatrix@R =50pt@C=50pt{ X \ar [r]^-{f} \ar [d]^{q'_{X} } & Y \ar [d]^{ q'_{Y} } \\ X' \ar [r]^-{f'} & Y' }$

where the vertical maps are left anodyne (and therefore covariant equivalences, by virtue of $(b)$). Using $(a)$, we conclude that $f$ is a covariant equivalence if and only if $f'$ is a covariant equivalence relative to $S$. By virtue of $(c)$, this is equivalent to the requirement that for each vertex $s \in S$, the induced map $f'_{s}: X'_{s} \rightarrow Y'_{s}$ is a homotopy equivalence.