Simplicial horns and Kan fibrations

Work with the standard simplices $\mathrm{\Delta }[n]$ (Simplicial sets, homotopies and trivial Kan fibrations). For $n\ge 1$ and $0\le k\le n$ the $k$-th horn ${\mathrm{\Lambda }}^k[n]$ is the union of the codimension-one faces ${\mathrm{\partial }}_i\mathrm{\Delta }[n]\cong \mathrm{\Delta }[n-1]$, $i\mathrm{\ne }k$, inside $\mathrm{\Delta }[n]$; equivalently, ${\mathrm{\Lambda }}^k[n{]}_m$ consists of those order-preserving $[m]\to [n]$ that factor through a face $[n-1]\to [n]$ omitting an index $i\mathrm{\ne }k$. The inclusion ${\mathrm{\Lambda }}^k[n]\hookrightarrow \mathrm{\Delta }[n]$ is the horn inclusion; for $n=1$ the two horns are the two vertices and the inclusions are the vertex inclusions, and for $n=0$ there is no horn.

A Kan fibration is a map $p\text{\hspace{0.17em}⁣}:X\to Y$ of simplicial sets with the right lifting property against every horn inclusion: every commutative square $\begin{array}{ccc}{\mathrm{\Lambda }}^k[n]& ⟶& X\\ \downarrow & & \downarrow \\ \mathrm{\Delta }[n]& ⟶& Y\end{array}$ with $n\ge 1$, $0\le k\le n$ admits a diagonal lift. A simplicial set $X$ is Kan when its unique map $X\to \mathrm{\Delta }[0]$ to a point is a Kan fibration, i.e. every horn in $X$ extends to a simplex. A trivial Kan fibration in the sense of Simplicial sets, homotopies and trivial Kan fibrations is a map with the same lifting property for all boundary inclusions $\mathrm{\partial }\mathrm{\Delta }[n]\hookrightarrow \mathrm{\Delta }[n]$, $n\ge 0$; a trivial Kan fibration is in particular a Kan fibration. For a horn lifting problem in dimension $n$, the prescribed faces specify the entire boundary of its missing $(n-1)$-face: intersect that face with the other faces. First use boundary lifting in dimension $n-1$ to supply the missing face over the corresponding face of the target simplex (for $n=1$ this is the degree-zero lift of a vertex). The now-complete boundary lifts in dimension $n$, producing the required horn filler.

For inclusions $i\text{\hspace{0.17em}⁣}:K\to L$ and $j\text{\hspace{0.17em}⁣}:K^{\mathrm{\prime }}\to L^{\mathrm{\prime }}$ of simplicial sets, their pushout product is $i\mathrm{\square }j\text{\hspace{0.17em}⁣}:(K\times L^{\mathrm{\prime }}){\cup }_{K\times K^{\mathrm{\prime }}}(L\times K^{\mathrm{\prime }})⟶L\times L^{\mathrm{\prime }},$ the map from the pushout of the two inclusions $K\times L^{\mathrm{\prime }}\to L\times L^{\mathrm{\prime }}$ and $L\times K^{\mathrm{\prime }}\to L\times L^{\mathrm{\prime }}$. A map is anodyne here when it is a composite of maps obtained by cobase change (pushout) from coproducts ${\coprod }_{\alpha }({\mathrm{\Lambda }}^{k_{\alpha }}[n_{\alpha }]\hookrightarrow \mathrm{\Delta }[n_{\alpha }])$ of horn inclusions. A map with the horn lifting property lifts against every anodyne map by successive lifting along the defining composites and coproduct factors; when the defining family is set-indexed, the simultaneous choice of lifts uses the Axiom of Choice (The Axiom of Choice), while finitely presented composites require no choice. These are lifting and construction definitions; they do not assert that a model structure on simplicial sets has been constructed.