# Kerodon

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

Lemma 5.2.4.12. Let $\operatorname{\mathcal{E}}$ be an $\infty$-category. Then the morphism $\rho : \Delta ^1 \times \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}\star \operatorname{\mathcal{E}}$ of Construction 5.2.4.1 is an inner fibration of simplicial sets.

Proof. Suppose we are given integers $0 < i < n$; we wish to show that every lifting problem

$\xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{i} \ar [r]^-{ \sigma _0 } \ar [d] & \Delta ^1 \times \operatorname{\mathcal{E}}\ar [d]^-{\rho } \\ \Delta ^ n \ar@ {-->}[ur]^{\sigma } \ar [r]^-{ \overline{\sigma } } & \operatorname{\mathcal{E}}\star \operatorname{\mathcal{E}}}$

admits a solution. Let us identify $\sigma _0$ with a pair of maps

$\sigma '_0: \Lambda ^{n}_{i} \rightarrow \Delta ^1 \quad \quad \sigma ''_0: \Lambda ^{n}_{i} \rightarrow \operatorname{\mathcal{E}}.$

By virtue of Proposition 1.2.3.1, we can extend $\sigma '_{0}$ uniquely to a morphism $\sigma ': \Delta ^ n \rightarrow \Delta ^1$. If $\sigma '$ is constant, then $\overline{\sigma }$ factors through one of the inclusion maps

$\operatorname{\mathcal{E}}\star \emptyset \hookrightarrow \operatorname{\mathcal{E}}\star \operatorname{\mathcal{E}}\hookleftarrow \emptyset \star \operatorname{\mathcal{E}},$

in which case the desired extension exists and is unique. If $\sigma '$ is not constant, then our assumption that $\operatorname{\mathcal{E}}$ is an $\infty$-category guarantees that we can extend $\sigma ''_0$ to an $n$-simplex $\sigma '': \Delta ^ n \rightarrow \operatorname{\mathcal{E}}$, and we can take $\sigma$ to be the pair $(\sigma ', \sigma '')$. $\square$