Past exam of the mathematics course of the University of Cambridge / 2025 / iii / Paper 165 / 1 / v / Solution

The contravariant simplicial mapping space functor takes the given pushout to the stated strict pullback. Since $X$ is a Kan complex, all four mapping spaces are Kan complexes. Moreover, the monomorphism $A\hookrightarrow B$ induces a Kan fibrationIndeed, a lifting problem against a horn is adjoint to a lifting problem for $X$ against the pushout-product of $A\hookrightarrow B$ with that horn inclusion; this pushout-product is an anodyne monomorphism, and $X$ fills it.

A strict pullback of fibrant simplicial sets along a fibration computes the homotopy pullback. The displayed pullback square is therefore also a homotopy pullback square.