The contravariant simplicial mapping space functor takes the given pushout to the stated strict pullback. Since is a Kan complex, all four mapping spaces are Kan complexes. Moreover, the monomorphism induces a Kan fibrationIndeed, a lifting problem against a horn is adjoint to a lifting problem for against the pushout-product of with that horn inclusion; this pushout-product is an anodyne monomorphism, and 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.
Articles by others on the same topic
There are currently no matching articles.