Pullback pasting lemma (source code)

= Pullback pasting lemma

In a <commutative diagram> consisting of two horizontally adjacent squares, if both squares are <pullbacks in a category>, their outside rectangle is a <pullback in a category>. If the right square and the outside rectangle are <pullbacks in a category>, the left square is a <pullback in a category>. To prove the first assertion, factor a compatible pair of <morphisms> first through the right square and then through the left square. For the second assertion, factor through the rectangle and use uniqueness in the right square to recover the prescribed middle <morphism>. Each factorization is unique by the same <universal properties>.