# Kerodon

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

Proposition 4.4.2.11. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor between $\infty$-categories. If $F$ is a left or a right fibration, then $F$ is conservative.

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:

$\xymatrix@R =50pt@C=50pt{ & F(Y) \ar [dr]^{\overline{v}} & \\ F(X) \ar [ur]^{F(u)} \ar [rr]^{F( \operatorname{id}_ X) } & & F(X). }$

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

$\xymatrix@R =50pt@C=50pt{ & Y \ar [dr]^{v} & \\ X \ar [ur]^{u} \ar [rr]^{\operatorname{id}_{X}} & & X }$

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.3.6.6). In particular, $u$ is an isomorphism. $\square$