The pullback of $A$ and $B$ over $C$ along $f$ and $g$1 is the pullback of $A$ and $B$ over $C$ along $f$ and $g$ in $\mathsf{Sets}$ as in 
, .
- 1Further Terminology: Also called the fibre product of $A$ and $B$ over $C$ along $f$ and $g$.
4.1.4 Pullbacks
Let $A$, $B$, and $C$ be sets and let $f\colon A\to C$ and $g\colon B\to C$ be functions.
Concretely, the pullback of $A$ and $B$ over $C$ along $f$ and $g$ is the pair $\webleft (A\times _{C}B,\left\{ \operatorname {\mathrm{\mathrm{pr}}}_{1},\operatorname {\mathrm{\mathrm{pr}}}_{2}\right\} \webright )$ consisting of:
-
1.
The Limit. The set $A\times _{C}B$ defined by
\[ A\times _{C}B\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (a,b\webright )\in A\times B\ \middle |\ f\webleft (a\webright )=g\webleft (b\webright )\right\} . \] -
2.
The Cone. The maps1
\begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1} & \colon A\times _{C}B\to A,\\ \operatorname {\mathrm{\mathrm{pr}}}_{2} & \colon A\times _{C}B\to B \end{align*}defined by
\begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1}\webleft (a,b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}a,\\ \operatorname {\mathrm{\mathrm{pr}}}_{2}\webleft (a,b\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}b \end{align*}for each $\webleft (a,b\webright )\in A\times _{C}B$.
- 1Further Notation: Also written $\operatorname {\mathrm{\mathrm{pr}}}^{A\times _{C}B}_{1}$ and $\operatorname {\mathrm{\mathrm{pr}}}^{A\times _{C}B}_{2}$.
Proof of Construction 4.1.4.1.2.
We claim that $A\times _{C}B$ is the categorical pullback of $A$ and $B$ over $C$ with respect to $\webleft (f,g\webright )$ in $\mathsf{Sets}$. First we need to check that the relevant pullback diagram commutes, i.e. that we have
\begin{align*} \webleft [f\circ \operatorname {\mathrm{\mathrm{pr}}}_{1}\webright ]\webleft (a,b\webright ) & = f\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{1}\webleft (a,b\webright )\webright )\\ & = f\webleft (a\webright )\\ & = g\webleft (b\webright )\\ & = g\webleft (\operatorname {\mathrm{\mathrm{pr}}}_{2}\webleft (a,b\webright )\webright )\\ & = \webleft [g\circ \operatorname {\mathrm{\mathrm{pr}}}_{2}\webright ]\webleft (a,b\webright ),\end{align*}
where $f\webleft (a\webright )=g\webleft (b\webright )$ since $\webleft (a,b\webright )\in A\times _{C}B$. Next, we prove that $A\times _{C}B$ satisfies the universal property of the pullback. Suppose we have a diagram of the form
\begin{align*} \operatorname {\mathrm{\mathrm{pr}}}_{1}\circ \phi & = p_{1},\\ \operatorname {\mathrm{\mathrm{pr}}}_{2}\circ \phi & = p_{2}\end{align*}
via
\[ \phi \webleft (x\webright )=\webleft (p_{1}\webleft (x\webright ),p_{2}\webleft (x\webright )\webright ) \]
for each $x\in P$, where we note that $\webleft (p_{1}\webleft (x\webright ),p_{2}\webleft (x\webright )\webright )\in A\times B$ indeed lies in $A\times _{C}B$ by the condition
\[ f\circ p_{1}=g\circ p_{2}, \]
which gives
\[ f\webleft (p_{1}\webleft (x\webright )\webright )=g\webleft (p_{2}\webleft (x\webright )\webright ) \]
for each $x\in P$, so that $\webleft (p_{1}\webleft (x\webright ),p_{2}\webleft (x\webright )\webright )\in A\times _{C}B$.
It is common practice to write $A\times _{C}B$ for the pullback of $A$ and $B$ over $C$ along $f$ and $g$, omitting the maps $f$ and $g$ from the notation and instead leaving them implicit, to be understood from the context.
However, the set $A\times _{C}B$ depends very much on the maps $f$ and $g$, and sometimes it is necessary or useful to note this dependence explicitly. In such situations, we will write $A\times _{f,C,g}B$ or $A\times ^{f,g}_{C}B$ for $A\times _{C}B$.
Here are some examples of pullbacks of sets.
-
1.
Unions via Intersections. Let $X$ be a set. We have
for each $A,B\in \mathcal{P}\webleft (X\webright )$.
Proof of Example 4.1.4.1.4.
Item 1: Unions via Intersections
Indeed, we have
\begin{align*} A\times _{A\cup B}B & \cong \left\{ \webleft (x,y\webright )\in A\times B\ \middle |\ x=y\right\} \\ & \cong A\cap B. \end{align*}
This finishes the proof.
Let $A$, $B$, $C$, and $X$ be sets.
-
1.
Functoriality. The assignment $\webleft (A,B,C,f,g\webright )\mapsto A\times _{f,C,g}B$ defines a functor
\[ -_{1}\times _{-_{3}}-_{1}\colon \mathsf{Fun}\webleft (\mathcal{P},\mathsf{Sets}\webright )\to \mathsf{Sets}, \]where $\mathcal{P}$ is the category that looks like this:
In particular, the action on morphisms of $-_{1}\times _{-_{3}}-_{1}$ is given by sending a morphism
in $\mathsf{Fun}\webleft (\mathcal{P},\mathsf{Sets}\webright )$ to the map $\xi \colon A\times _{C}B\overset {\exists !}{\to }A'\times _{C'}B'$ given by
\[ \xi \webleft (a,b\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\phi \webleft (a\webright ),\psi \webleft (b\webright )\webright ) \]for each $\webleft (a,b\webright )\in A\times _{C}B$, which is the unique map making the diagram
commute.
-
2.
Adjointness I. We have adjunctions
witnessed by bijections
\begin{align*} \mathsf{Sets}_{/X}\webleft (A\times _{X}B,C\webright ) & \cong \mathsf{Sets}_{/X}\webleft (A,\boldsymbol {\mathsf{Sets}}_{/X}\webleft (B,C\webright )\webright ),\\ \mathsf{Sets}_{/X}\webleft (A\times _{X}B,C\webright ) & \cong \mathsf{Sets}_{/X}\webleft (B,\boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,C\webright )\webright ), \end{align*}natural in $\webleft (A,\phi _{A}\webright ),\webleft (B,\phi _{B}\webright ),\webleft (C,\phi _{C}\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{/X}\webright )$, where $\boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,B\webright )$ is the object of $\mathsf{Sets}_{/X}$ consisting of (see
, ):
-
•
The Set. The set $\boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,B\webright )$ defined by
\[ \boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,B\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\coprod _{x\in X}\mathsf{Sets}\webleft (\phi ^{-1}_{A}\webleft (x\webright ),\phi ^{-1}_{Y}\webleft (x\webright )\webright ) \] -
•
The Map to $X$. The map
\[ \phi _{\boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,B\webright )}\colon \boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,B\webright )\to X \]defined by
\[ \phi _{\boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,B\webright )}\webleft (x,f\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x \]for each $\webleft (x,f\webright )\in \boldsymbol {\mathsf{Sets}}_{/X}\webleft (A,B\webright )$.
-
•
-
3.
Adjointness II. We have an adjunction
witnessed by a bijection
\[ \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{/X}\times \mathsf{Sets}_{/X}}\webleft (\webleft (A,A\webright ),\webleft (B,C\webright )\webright )\cong \mathsf{Sets}_{/X}\webleft (A,B\times _{X}C\webright ), \]natural in $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{/X}\webright )$ and in $\webleft (B,C\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{/X}\times \mathsf{Sets}_{/X}\webright )$.
-
4.
Associativity. Given a diagram
in $\mathsf{Sets}$, we have isomorphisms of sets
\[ \webleft (A\times _{X}B\webright )\times _{Y}C\cong \webleft (A\times _{X}B\webright )\times _{B}\webleft (B\times _{Y}C\webright ) \cong A\times _{X}\webleft (B\times _{Y}C\webright ), \]where these pullbacks are built as in the diagrams
-
5.
Interaction With Composition. Given a diagram
in $\mathsf{Sets}$, we have isomorphisms of sets
\begin{align*} X\times ^{f\circ \phi ,g\circ \psi }_{K}Y & \cong \webleft (X\times ^{\phi ,q_{1}}_{A}\webleft (A\times ^{f,g}_{K}B\webright )\webright )\times ^{p_{2},p_{1}}_{A\times ^{f,g}_{K}B}\webleft (\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y\webright )\\ & \cong X\times ^{\phi ,p}_{A}\webleft (\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y\webright )\\ & \cong \webleft (X\times ^{\phi ,q_{1}}_{A}\webleft (A\times ^{f,g}_{K}B\webright )\webright )\times ^{q,\psi }_{B}Y \end{align*}where
\[ \begin{aligned} q_{1} & = \operatorname {\mathrm{\mathrm{pr}}}^{A\times ^{f,g}_{K}B}_{1},\\ p_{1} & = \operatorname {\mathrm{\mathrm{pr}}}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{Y}}_{1},\\ p & = q_{1}\circ \operatorname {\mathrm{\mathrm{pr}}}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y}_{1}, \end{aligned} \qquad \begin{aligned} q_{2} & = \operatorname {\mathrm{\mathrm{pr}}}^{A\times ^{f,g}_{K}B}_{2},\\ p_{2} & = \operatorname {\mathrm{\mathrm{pr}}}^{X\times ^{\phi ,q_{1}}_{A\times ^{f,g}_{K}B}\webleft (A\times ^{f,g}_{K}B\webright )}_{2},\\ q & = q_{2}\circ \operatorname {\mathrm{\mathrm{pr}}}^{X\times ^{\phi ,q_{1}}_{A}\webleft (A\times ^{f,g}_{K}B\webright )}_{2}, \end{aligned} \]and where these pullbacks are built as in the following diagrams:
-
6.
Unitality. We have isomorphisms of sets
natural in $\webleft (A,f\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{/X}\webright )$.
-
7.
Commutativity. We have an isomorphism of sets
natural in $\webleft (A,f\webright ),\webleft (B,g\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{/X}\webright )$.
-
8.
Distributivity Over Coproducts. Let $A$, $B$, and $C$ be sets and let $\phi _{A}\colon A\to X$, $\phi _{B}\colon B\to X$, and $\phi _{C}\colon C\to X$ be morphisms of sets. We have isomorphisms of sets
\begin{align*} \delta ^{\mathsf{Sets}_{/X}}_{\ell } & \colon A\times _{X}\webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright ) \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (A\times _{X}B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (A\times _{X}C\webright ),\\ \delta ^{\mathsf{Sets}_{/X}}_{r} & \colon \webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B\webright )\times _{X}C \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (A\times _{X}C\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (B\times _{X}C\webright ), \end{align*}as in the diagrams
natural in $A,B,C\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{/X}\webright )$.
-
9.
Annihilation With the Empty Set. We have isomorphisms of sets
natural in $\webleft (A,f\webright )\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}_{/X}\webright )$.
-
10.
Interaction With Products. We have an isomorphism of sets
-
11.
Symmetric Monoidality. The 8-tuple $\left(\mathrlap {\phantom{\lambda ^{\mathsf{Sets}_{/X}}}}\mathsf{Sets}_{/X}\right.$, $\times _{X}$, $X$, $\boldsymbol {\mathsf{Sets}}_{/X}$, $\alpha ^{\mathsf{Sets}_{/X}}$, $\lambda ^{\mathsf{Sets}_{/X}}$, $\rho ^{\mathsf{Sets}_{/X}}$, $\left.\sigma ^{\mathsf{Sets}_{/X}}\right)$ is a symmetric closed monoidal category.
Proof of Proposition 4.1.4.1.5.
Item 1: Functoriality
This is a special case of functoriality of co/limits, , of , with the explicit expression for $\xi $ following from the commutativity of the cube pullback diagram.
Item 2: Adjointness I
This is a repetition of , of , and is proved there.
Item 3: Adjointness II
This follows from the universal property of the product (pullbacks are products in $\mathsf{Sets}_{/X}$).
Item 4: Associativity
We have
\begin{align*} \webleft (A\times _{X}B\webright )\times _{Y}C & \cong \left\{ \webleft (\webleft (a,b\webright ),c\webright )\in \webleft (A\times _{X}B\webright )\times C\ \middle |\ h\webleft (b\webright )=k\webleft (c\webright )\right\} \\ & \cong \left\{ \webleft (\webleft (a,b\webright ),c\webright )\in \webleft (A\times B\webright )\times C\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (b\webright )$ and $h\webleft (b\webright )=k\webleft (c\webright )$}\right\} \\ & \cong \left\{ \webleft (a,\webleft (b,c\webright )\webright )\in A\times \webleft (B\times C\webright )\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (b\webright )$ and $h\webleft (b\webright )=k\webleft (c\webright )$}\right\} \\ & \cong \left\{ \webleft (a,\webleft (b,c\webright )\webright )\in A\times \webleft (B\times _{Y}C\webright )\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (b\webright )$}\right\} \\ & \cong A\times _{X}\webleft (B\times _{Y}C\webright ) \end{align*}
\begin{align*} \webleft (A\times _{X}B\webright )\times _{B}\webleft (B\times _{Y}C\webright ) & \cong \left\{ \webleft (\webleft (a,b\webright ),\webleft (b',c\webright )\webright )\in \webleft (A\times _{X}B\webright )\times \webleft (B\times _{Y}C\webright )\ \middle |\ b=b'\right\} \\ & \cong \left\{ \webleft (\webleft (a,b\webright ),\webleft (b',c\webright )\webright )\in \webleft (A\times B\webright )\times \webleft (B\times C\webright )\ \middle |\ \begin{aligned} & \text{$f\webleft (a\webright )=g\webleft (b\webright )$, $b=b'$,}\\ & \text{and $h\webleft (b'\webright )=k\webleft (c\webright )$}\end{aligned}\right\} \\ & \cong \left\{ \webleft (a,\webleft (b,\webleft (b',c\webright )\webright )\webright )\in A\times \webleft (B\times \webleft (B\times C\webright )\webright )\ \middle |\ \begin{aligned} & \text{$f\webleft (a\webright )=g\webleft (b\webright )$, $b=b'$,}\\ & \text{and $h\webleft (b'\webright )=k\webleft (c\webright )$}\end{aligned}\right\} \\ & \cong \left\{ \webleft (a,\webleft (\webleft (b,b'\webright ),c\webright )\webright )\in A\times \webleft (\webleft (B\times B\webright )\times C\webright )\ \middle |\ \begin{aligned} & \text{$f\webleft (a\webright )=g\webleft (b\webright )$, $b=b'$,}\\ & \text{and $h\webleft (b'\webright )=k\webleft (c\webright )$}\end{aligned}\right\} \\ & \cong \left\{ \webleft (a,\webleft (\webleft (b,b'\webright ),c\webright )\webright )\in A\times \webleft (\webleft (B\times _{B}B\webright )\times C\webright )\ \middle |\ \begin{aligned} & \text{$f\webleft (a\webright )=g\webleft (b\webright )$ and}\\ & \text{$h\webleft (b'\webright )=k\webleft (c\webright )$}\end{aligned}\right\} \\ & \cong \left\{ \webleft (a,\webleft (b,c\webright )\webright )\in A\times \webleft (B\times C\webright )\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (b\webright )$ and $h\webleft (b\webright )=k\webleft (c\webright )$}\right\} \\ & \cong A\times _{X}\webleft (B\times _{Y}C\webright ), \end{align*}
Item 5: Interaction With Composition
By Item 4, it suffices to construct only the isomorphism
\[ X\times ^{f\circ \phi ,g\circ \psi }_{K}Y\cong \webleft (X\times ^{\phi ,q_{1}}_{A}\webleft (A\times ^{f,g}_{K}B\webright )\webright )\times ^{p_{2},p_{1}}_{A\times ^{f,g}_{K}B}\webleft (\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y\webright ). \]
We have
\begin{align*} \webleft (X\times ^{\phi ,q_{1}}_{A}\webleft (A\times ^{f,g}_{K}B\webright )\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (x,\webleft (a,b\webright )\webright )\in X\times \webleft (A\times ^{f,g}_{K}B\webright )\ \middle |\ \phi \webleft (x\webright )=q_{1}\webleft (a,b\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (x,\webleft (a,b\webright )\webright )\in X\times \webleft (A\times ^{f,g}_{K}B\webright )\ \middle |\ \phi \webleft (x\webright )=a\right\} \\ & \cong \left\{ \webleft (x,\webleft (a,b\webright )\webright )\in X\times \webleft (A\times B\webright )\ \middle |\ \text{$\phi \webleft (x\webright )=a$ and $f\webleft (a\webright )=g\webleft (b\webright )$}\right\} ,\\ \webleft (\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (\webleft (a,b\webright ),y\webright )\in \webleft (A\times ^{f,g}_{K}B\webright )\times Y\ \middle |\ q_{2}\webleft (a,b\webright )=\psi \webleft (y\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (\webleft (a,b\webright ),y\webright )\in \webleft (A\times ^{f,g}_{K}B\webright )\times Y\ \middle |\ b=\psi \webleft (y\webright )\right\} \\ & \cong \left\{ \webleft (\webleft (a,b\webright ),y\webright )\in \webleft (A\times B\webright )\times Y\ \middle |\ \text{$b=\psi \webleft (y\webright )$ and $f\webleft (a\webright )=g\webleft (b\webright )$}\right\} ,\end{align*}
\begin{align*} S & = \webleft (X\times ^{\phi ,q_{1}}_{A}\webleft (A\times ^{f,g}_{K}B\webright )\webright )\\ S' & = \webleft (\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y\webright ), \end{align*}
we have
\begin{align*} S\times ^{p_{2},p_{1}}_{A\times ^{f,g}_{K}B}S' & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (\webleft (x,\webleft (a,b\webright )\webright ),\webleft (\webleft (a',b'\webright ),y\webright )\webright )\in S\times S'\ \middle |\ p_{1}\webleft (x,\webleft (a,b\webright )\webright )=p_{2}\webleft (\webleft (a',b'\webright ),y\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (\webleft (x,\webleft (a,b\webright )\webright ),\webleft (\webleft (a',b'\webright ),y\webright )\webright )\in S\times S'\ \middle |\ \webleft (a,b\webright )=\webleft (a',b'\webright )\right\} \\ & \cong \left\{ \webleft (\webleft (x,a,b,y\webright )\webright )\in X\times A\times B\times Y\ \middle |\ \text{$\phi \webleft (x\webright )=a$, $\psi \webleft (y\webright )=b$, and $f\webleft (a\webright )=g\webleft (b\webright )$}\right\} \\ & \cong \left\{ \webleft (\webleft (x,a,b,y\webright )\webright )\in X\times A\times B\times Y\ \middle |\ f\webleft (\phi \webleft (x\webright )\webright )=g\webleft (\psi \webleft (y\webright )\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}X\times _{K}Y. \end{align*}
Item 6: Unitality
We have
\begin{align*} X\times _{X}A & \cong \left\{ \webleft (x,a\webright )\in X\times A\ \middle |\ f\webleft (a\webright )=x\right\} ,\\ A\times _{X}X & \cong \left\{ \webleft (a,x\webright )\in X\times A\ \middle |\ f\webleft (a\webright )=x\right\} , \end{align*}
which are isomorphic to $A$ via the maps $\webleft (x,a\webright )\mapsto a$ and $\webleft (a,x\webright )\mapsto a$. The proof of the naturality of $\lambda ^{\mathsf{Sets}_{/X}}$ and $\rho ^{\mathsf{Sets}_{/X}}$ is omitted.
Item 7: Commutativity
We have
\begin{align*} A\times _{C}B & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (a,b\webright )\in A\times B\ \middle |\ f\webleft (a\webright )=g\webleft (b\webright )\right\} \\ & = \left\{ \webleft (a,b\webright )\in A\times B\ \middle |\ g\webleft (b\webright )=f\webleft (a\webright )\right\} \\ & \cong \left\{ \webleft (b,a\webright )\in B\times A\ \middle |\ g\webleft (b\webright )=f\webleft (a\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}B\times _{C}A. \end{align*}
The proof of the naturality of $\sigma ^{\mathsf{Sets}_{/X}}$ is omitted.
Item 8: Distributivity Over Coproducts
We have
\begin{align*} A\times _{X}\webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (a,z\webright )\in A\times \webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright )\ \middle |\ \phi _{A}\webleft (a\webright )=\phi _{B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C}\webleft (z\webright )\right\} \\ & = \left\{ \webleft (a,z\webright )\in A\times \webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright )\ \middle |\ \text{$z=\webleft (0,b\webright )$ and $\phi _{A}\webleft (a\webright )=\phi _{B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C}\webleft (z\webright )$}\right\} \\ & \phantom{={}} \mkern 4mu\cup \left\{ \webleft (a,z\webright )\in A\times \webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright )\ \middle |\ \text{$z=\webleft (1,c\webright )$ and $\phi _{A}\webleft (a\webright )=\phi _{B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C}\webleft (z\webright )$}\right\} \\ & = \left\{ \webleft (a,z\webright )\in A\times \webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright )\ \middle |\ \text{$z=\webleft (0,b\webright )$ and $\phi _{A}\webleft (a\webright )=\phi _{B}\webleft (b\webright )$}\right\} \\ & \phantom{={}} \mkern 4mu\cup \left\{ \webleft (a,z\webright )\in A\times \webleft (B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C\webright )\ \middle |\ \text{$z=\webleft (1,c\webright )$ and $\phi _{A}\webleft (a\webright )=\phi _{C}\webleft (c\webright )$}\right\} \\ & \cong \left\{ \webleft (a,b\webright )\in A\times B\ \middle |\ \phi _{A}\webleft (a\webright )=\phi _{B}\webleft (b\webright )\right\} \\ & \phantom{={}} \mkern 4mu\cup \left\{ \webleft (a,c\webright )\in A\times C\ \middle |\ \phi _{A}\webleft (a\webright )=\phi _{C}\webleft (c\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (A\times _{X}B\webright )\cup \webleft (A\times _{X}C\webright )\\ & \cong \webleft (A\times _{X}B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (A\times _{X}C\webright ), \end{align*}
\[ \delta ^{\mathsf{Sets}_{/X}}_{r} \colon \webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B\webright )\times _{X}C \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft (A\times _{X}C\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\webleft (B\times _{X}C\webright ) \]
being similar. The proof of the naturality of $\delta ^{\mathsf{Sets}_{/X}}_{\ell }$ and $\delta ^{\mathsf{Sets}_{/X}}_{r}$ is omitted.
Item 9: Annihilation With the Empty Set
We have
\begin{align*} A\times _{X}\text{Ø}& \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (a,b\webright )\in A\times \text{Ø}\ \middle |\ f\webleft (a\webright )=g\webleft (b\webright )\right\} \\ & = \left\{ k\in \text{Ø}\ \middle |\ f\webleft (a\webright )=g\webleft (b\webright )\right\} \\ & = \text{Ø}, \end{align*}
and similarly for $\text{Ø}\times _{X}A$, where we have used Item 8 of Proposition 4.1.3.1.3. The proof of the naturality of $\zeta ^{\mathsf{Sets}_{/X}}_{\ell }$ and $\zeta ^{\mathsf{Sets}_{/X}}_{r}$ is omitted.
Item 10: Interaction With Products
We have
\begin{align*} A\times _{\mathrm{pt}}B & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (a,b\webright )\in A\times B\ \middle |\ \mathord {!}_{A}\webleft (a\webright )\mathbin {=}\mathord {!}_{B}\webleft (b\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (a,b\webright )\in A\times B\ \middle |\ \star =\star \right\} \\ & = \left\{ \webleft (a,b\webright )\in A\times B\right\} \\ & = A\times B. \end{align*}
Item 11: Symmetric Monoidality
Omitted.
