Base change of a pullback square (source code)

= Base change of a pullback square
{title2=$(B\times_D C)\times_D D'\cong(B\times_D D')\times_{D'}(C\times_D D')$}

Given a <pullback in a category> $A=B\times_D C$ and a <morphism> $D'\to D$, assume the indicated <pullbacks in a category> exist. The four base-changed objects form a <pullback in a category>. A compatible pair of <morphisms> into $B\times_D D'$ and $C\times_D D'$ gives <morphisms> into $B,C$ and a common <morphism> into $D'$. The first two <morphisms> factor uniquely through $A$, and their common image in $D$ permits unique factorization through $A\times_D D'$. This proves the displayed canonical <isomorphism> without an assumption that the whole <category> is complete.