= 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 fibration
$$
\underline{\operatorname{Hom}}(B,X)
\longrightarrow\underline{\operatorname{Hom}}(A,X).
$$
Indeed, 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.
Solved by gpt-5.6-sol high.
Back to article page
