The Pullback Lemma

A key lemma in category theory is the “pullback lemma”.
Here we prove it in the category $\Set$.
(The diagram in $\Set$ showing the situation) is in (the lower part of the box below); (the functions which implement the isomorphism) are shown (above the diagram).

$$\langle\eltx,\elty,\eltc\rangle \mapsto \langle\eltx,\eltc\rangle \mapsto \langle\eltx,\eltx\functionf,\eltc\rangle \mapsto \langle\eltx,\eltc\rangle$$ $$\begin{array}{} \boxed{ \begin{array}{} \\ (\functionf \functiong)\inv \gamma\\ \langle\eltx,\eltc\rangle \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltc\gamma \\ \\ \\ \\ \end{array} } & \stackrel {\text{PBL}}\cong & \boxed{ \begin{array}{} \setX\times_\setY(\setY\times_\setZ\setC) \\ \functionf\inv\functiong\inv \gamma\\ \langle\eltx, \elty, \eltc\rangle \mid \eltx\functionf \xlongequal{\setY} \elty \wedge \elty\functiong \xlongequal{\setZ} \eltc\gamma \\ \langle\eltx,\eltc\rangle \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltc\gamma \\ (\functionf\functiong)\inv\gamma \\ \setX\times_\setZ\setC \\ \end{array} } & \xrightarrow{\mkern3em} & \boxed{ \begin{array}{} \\ \\ \\ \langle\elty,\eltc\rangle \mid \elty\functiong \xlongequal{\setZ} \eltc\gamma \\ \functiong\inv \gamma \\ \setY\times_\setZ\setC \\ \end{array} } & \xrightarrow{\mkern3em} & \setC \\ && \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow \rlap\gamma \\ && \setX & \xrightarrow[\textstyle \functionf]{} & \setY & \xrightarrow[\textstyle \functiong]{} & \setZ \\ \end{array}$$

A significant example of the use of this result is:

$$\langle\eltx,\elty\rangle \mapsto \eltx \mapsto \langle\eltx,\eltx\functionf\rangle \mapsto \eltx$$ $$\begin{array}{} \boxed{ \begin{array}{} \\ (\functionf \functionB)\inv \radjtop\\ \eltx \mid \eltx\functionf\functionB \xlongequal{\bftwo} \radjtop \\ \end{array} } & \stackrel {\text{PBL}}\cong & \boxed{ \begin{array}{} \functionf\inv\setB\\ \functionf\inv\functionB\inv \radjtop\\ \langle\eltx, \elty\rangle \mid \eltx\functionf \xlongequal{\setY} \elty \wedge \elty\functionB \xlongequal{\bftwo} \radjtop \\ \end{array} } & \xrightarrow{\mkern3em} & \boxed{ \begin{array}{} \setB \\ \functionB\inv \radjtop\\ \elty \mid \elty\functionB \xlongequal{\bftwo} \radjtop \\ \end{array} } & \xrightarrow{\mkern3em} & \bfone\\ && \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \big\downarrow \rlap\radjtop\\ && \setX & \xrightarrow[\textstyle \functionf]{} & \setY & \xrightarrow[\textstyle \functionB]{} & \bftwo\\ \end{array}$$

This demonstrates the naturality of the predicate/subset bijection.

---

The diagram below is a two-dimensional generalization of the ordinary (one-dimensional) pullback lemma stated above:

$$\begin{array}{} && \boxed{\begin{array}{} (\setU \times_\setZ \setY) \times_{(\setV\times_\setZ\setY)}(\setV \times_\setZ \setX)\\ \eltu, \elty, \eltv, \eltx \mid \eltu\functions\functiont \xlongequal{\setZ} \elty\functiong \land \langle \eltu\functions,\elty \rangle \xlongequal{\setV\times_\setZ\setY} \langle \eltv, \eltx\functionf \rangle \land \eltv\functiont \xlongequal{\setZ} \eltx\functionf\functiong \\ \eltu,\eltx \mid \eltu\functions\functiont \xlongequal{\setZ} \eltx\functionf\functiong \\ \setU \times_\setZ \setX \\ \end{array} } & \xrightarrow{} & \boxed{\begin{array}{} (\setV\times_\setZ\setY) \times_\setY \setX \\ \eltv, \elty, \eltx \mid \eltv\functiont \xlongequal{\setZ} \elty\functiong \land \elty \xlongequal{\setY} \eltx\functionf \\ \eltv,\eltx \mid \eltv\functiong \xlongequal{\setZ} \eltx\functionf\functiong \\ \setV \times_\setZ \setX \\ \end{array} } & \xrightarrow{} & \setX & \ni & \eltx \\ && \Bigg\downarrow & \llap {{\raise2ex\hbox{$\lrcorner$}}\mkern1em} \searrow & \Bigg\downarrow & \mkern-2em{\raise2ex\hbox{$\lrcorner$}} & \Bigg\downarrow \rlap\functionf \\ && \boxed{\begin{array}{} \setU \times_\setV (\setV\times_\setZ\setY) \\ \eltu,\eltv,\elty \mid \eltu\functions \xlongequal{\setV} \eltv \land \eltv\functiont \xlongequal{\setZ} \elty\functiong \\ \eltu,\elty \mid \eltu\functionf\functiong \xlongequal{\setZ} \elty\functiong \\ \setU \times_\setZ \setY \\ \end{array} } & \xrightarrow{} & \boxed{\begin{array}{} \\ \\ \eltv,\elty \mid \eltv\functiont \xlongequal{\setZ} \elty\functiong \\ \setV \times_\setZ \setY \\ \end{array} } & \xrightarrow{} & \setY & \ni & \elty \\ && \Bigg\downarrow & \mkern-10em{\raise2ex\hbox{$\lrcorner$}} & \Bigg\downarrow & \llap { {\raise2ex\hbox{$\lrcorner$}} \mkern3em } \searrow & \Bigg\downarrow \rlap\functiong \\ && \setU & \xrightarrow[\textstyle \mkern.8em \functions \mkern.8em]{} & \setV & \xrightarrow[\textstyle \mkern.8em \functiont \mkern.8em]{} & \setZ \\ &&\eltu &&\eltv \\ \end{array}$$