Trivial simplicial fibrations lift monomorphisms and have contractible products of fibres

Unique nondegenerate ancestors. Every simplex $x$ of a simplicial set has a unique expression $x={\alpha }^{\ast }y$ with $\alpha$ surjective and $y$ nondegenerate. For the first assertion, if ${\alpha }^{\ast }y={\beta }^{\ast }z$ with $\alpha ,\beta$ surjective and $y,z$ nondegenerate, choose an order-preserving section $\xi$ of $\beta$; factor $\alpha \xi$ as a surjection followed by an injection. A nonidentity surjective factor would express $z=(\alpha \xi {)}^{\ast }y$ as degenerate, so nondegeneracy forces $\alpha \xi$ to be injective, hence $\dim z\le \dim y$, and symmetry gives equality of the dimensions. For every order-preserving section $\xi$ of $\beta$, the map $\alpha \xi$ is then an order-preserving injection between equally sized finite ordinals, hence the identity. Every position $j$ may be included in such a section (choose $j$ in its fibre of $\beta$ and any position in each other ordered fibre), so $\alpha (j)=\beta (j)$ for all $j$. Thus $\alpha =\beta$, and applying a section recovers $y=z$. Existence follows by repeatedly applying degeneracy operators backwards until the dimension drops and the resulting simplex is nondegenerate. Consequently, adjoining a missing simplex of smallest dimension together with its degeneracies is exactly the pushout of a simplex along its boundary, and no two such adjunctions conflict.

Stability under pullback and products. If $Y^{\mathrm{\prime }}\to Y$ is a map of simplicial sets, the pullback $p^{\mathrm{\prime }}\text{\hspace{0.17em}⁣}:X{\times }_Y{Y}^{\mathrm{\prime }}\to Y^{\mathrm{\prime }}$ lifts any boundary square because a lift of the corresponding square for $p$, composed with the projection, provides a lift for $p^{\mathrm{\prime }}$ by the universal property. For a set-indexed family $(p_i\text{\hspace{0.17em}⁣}:X_i\to Y_i)$ of trivial Kan fibrations, a boundary square into the product has coordinate boundary squares; by [F3] choose one lift in each coordinate simultaneously and combine them by the universal property of the product. The empty product is the one-point simplicial set, and the statement holds vacuously.

Lifting monomorphisms. Let $Z\subseteq W$ be a degreewise injective map and let $f\text{\hspace{0.17em}⁣}:Z\to X$, $g\text{\hspace{0.17em}⁣}:W\to Y$ satisfy $pf=g{\mathrm{\mid }}_Z$. Well-order the nondegenerate simplices of $W$ not lying in $Z$ first by dimension and then within each dimension, using [F3]. Adjoin them one at a time: at each stage the new nondegenerate simplex has boundary lying in the already constructed part (by the minimality of the ordering), so the lifting property of the trivial Kan fibration supplies a lift of that simplex over the prescribed boundary; at limit stages take the union. Step 1.1 ensures that the degenerate simplices generated along the way receive compatible values, so the construction produces a map $W\to X$ lifting along $p$ and extending $f$. This proves lifting against every monomorphism. AC is used exactly in the well-ordering and in the transfinite selection of lifts.

Fibres are trivial fibrations over a point. The fibre $F=X_y=p^{-1}(y)$ over a vertex $y\in Y_0$, defined as the pullback of $p$ along the map $\mathrm{\Delta }[0]\to Y$ with value $y$, is a trivial Kan fibration over $\mathrm{\Delta }[0]$ by step 1.2; in particular $F_0$ is nonempty by degree-zero surjectivity [F1]. Choose a vertex of $F$, which gives a section $q\text{\hspace{0.17em}⁣}:\mathrm{\Delta }[0]\to F$; the existence of one vertex follows from degree-zero surjectivity and needs only a single choice. The inclusion of the boundary $F\times \mathrm{\partial }\mathrm{\Delta }[1]\subseteq F\times \mathrm{\Delta }[1]$ has prescribed maps ${\mathrm{i}\mathrm{d}}_F$ on $F\times \{0\}$ and $q\circ p_F$ on $F\times \{1\}$, where $p_F\text{\hspace{0.17em}⁣}:F\to \mathrm{\Delta }[0]$; lifting this square by step 2.1 (the inclusion is degreewise injective) yields a homotopy from ${\mathrm{i}\mathrm{d}}_F$ to the constant map, and the composite $p_F\circ q={\mathrm{i}\mathrm{d}}_{\mathrm{\Delta }[0]}$, so $F$ is contractible. The product of a set-indexed family of fibres is itself a trivial Kan fibration over a point by step 1.2, so the same argument applies to it and gives nonemptiness and contractibility.

Homotopy equivalence. Lifting the inclusion $X\times \mathrm{\partial }\mathrm{\Delta }[1]\subseteq X\times \mathrm{\Delta }[1]$ with the prescribed maps ${\mathrm{i}\mathrm{d}}_X$ on $X\times \{0\}$ and $q^{\mathrm{\prime }}\text{\hspace{0.17em}⁣}p$ on $X\times \{1\}$, where $q^{\mathrm{\prime }}\text{\hspace{0.17em}⁣}:Y\to X$ is a section of $p$ obtained by lifting the empty subobject of $Y$ (AC supplies the simultaneous choices over the simplex set of $Y$, using step 2.1 with $Z=\mathrm{\varnothing }$), gives a homotopy from ${\mathrm{i}\mathrm{d}}_X$ to $q^{\mathrm{\prime }}\text{\hspace{0.17em}⁣}p$, while $p{q}^{\mathrm{\prime }}={\mathrm{i}\mathrm{d}}_Y$; hence $p$ is a simplicial homotopy equivalence.