# Kerodon

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

Construction 3.4.0.3 (The Homotopy Fiber Product). Let $f_0: X_0 \rightarrow X$ and $f_1: X_1 \rightarrow X$ be morphisms of simplicial sets, where $X$ is a Kan complex. We let $X_0 \times _{X}^{\mathrm{h}} X_1$ denote the simplicial set

$X_0 \times _{ \operatorname{Fun}( \{ 0\} , X) } \operatorname{Fun}( \Delta ^1, X ) \times _{ \operatorname{Fun}( \{ 1\} , X) } X_1.$

We will refer to $X_0 \times _{X}^{\mathrm{h}} X_1$ as the homotopy fiber product of $X_0$ with $X_1$ over $X$.