# Kerodon

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

Notation 5.1.3.10. Let $q: X \rightarrow S$ be an inner fibration of simplicial sets, let $y$ and $z$ be vertices of $X$ having images $s = q(y)$ and $t = q(z)$, and let $\overline{e}: s \rightarrow t$ be an edge of $S$. Recall that the relative morphism space $\operatorname{Hom}_{X}(y,z)_{\overline{e}}$ is defined to be the fiber product $\operatorname{Hom}_{X}(y,z) \times _{ \operatorname{Hom}_{S}( s,t )} \{ \overline{e} \}$ (Construction 4.6.1.14).

Let $x$ be another vertex of $X$ satisfying $q(x) = s$, and let $\sigma$ denote the image of $\overline{e}$ under the degeneracy map $\operatorname{Hom}_{S}(s,t) \rightarrow \operatorname{Hom}_{S}(s,s,t)$ (see Notation 4.6.8.1). It follows from Proposition 4.6.8.4 (and Example 4.6.1.16) that restriction along the inclusion $\Lambda ^{2}_{1} \hookrightarrow \Delta ^2$ induces a trivial Kan fibration of simplicial sets

$\theta : \operatorname{Hom}_{X}(x,y,z) \times _{\operatorname{Hom}_{S}( s,s,t ) } \{ \sigma \} \rightarrow \operatorname{Hom}_{X}(y,z)_{ \overline{e} } \times \operatorname{Hom}_{ X_{s} }(x,y),$

where $X_{\overline{y}}$ denotes the $\infty$-category given by the fiber $\{ \overline{y} \} \times _{S} X$. In particular, the homotopy class $[\theta ]$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. Combining the inverse isomorphism $[\theta ]^{-1}$ with the restriction map $\operatorname{Hom}_{X}(x,y,z) \times _{\operatorname{Hom}_{S}( s,s,t ) } \{ \sigma \} \rightarrow \operatorname{Hom}_{X}(x,z)_{ \overline{e} }$, we obtain a composition law

$\circ : \operatorname{Hom}_{X}(y,z)_{ \overline{e} } \times \operatorname{Hom}_{ X_{s} }(x,y) \rightarrow \operatorname{Hom}_{X}(x,z)_{ \overline{e} }.$

If $e: y \rightarrow z$ is an edge of $X$ satisfying $q(e) = \overline{e}$, then the restriction of this composition law to $\{ e \} \times \operatorname{Hom}_{X_ s}(x,y)$ determines a morphism of Kan complexes $\operatorname{Hom}_{X_ s}( x,y) \xrightarrow { [e] \circ } \operatorname{Hom}_{X}(x,z)_{ \overline{e} }$, which is well-defined up to homotopy.