Homotopy pullback (source code)

= Homotopy pullback
{wiki}

A homotopy pullback is the derived form of a pullback. A strict pullback square of fibrant objects computes a homotopy pullback whenever one of the two maps into the lower-right object is a fibration.