Let $A$, $B$, $C$, and $X$ be sets.
-
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.
-
Adjointness. We have adjunctions witnessed by bijections
\begin{align*} \mathsf{Sets}_{/X}\webleft (A\times _{X}B,C\webright ) & \cong \mathsf{Sets}_{/X}\webleft (A,\textbf{Sets}_{/X}\webleft (B,C\webright )\webright ),\\ \mathsf{Sets}_{/X}\webleft (A\times _{X}B,C\webright ) & \cong \mathsf{Sets}_{/X}\webleft (B,\textbf{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 \text{Obj}\webleft (\mathsf{Sets}_{/X}\webright )$, where $\textbf{Sets}_{/X}\webleft (A,B\webright )$ is the object of $\mathsf{Sets}_{/X}$ consisting of (see , ):
- The Set. The set $\textbf{Sets}_{/X}\webleft (A,B\webright )$ defined by
\[ \textbf{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 _{\textbf{Sets}_{/X}\webleft (A,B\webright )}\colon \textbf{Sets}_{/X}\webleft (A,B\webright )\to X \]
defined by
\[ \phi _{\textbf{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 \textbf{Sets}_{/X}\webleft (A,B\webright )$.
- The Set. The set $\textbf{Sets}_{/X}\webleft (A,B\webright )$ defined by
-
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
-
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} & = \text{pr}^{A\times ^{f,g}_{K}B}_{1},\\ p_{1} & = \text{pr}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{Y}}_{1},\\ p & = q_{1}\circ \text{pr}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y}_{1}, \end{aligned} \qquad \begin{aligned} q_{2} & = \text{pr}^{A\times ^{f,g}_{K}B}_{2},\\ p_{2} & = \text{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 \text{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:
- Unitality. We have isomorphisms of sets natural in $\webleft (A,f\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{/X}\webright )$.
- Commutativity. We have an isomorphism of sets natural in $\webleft (A,f\webright ),\webleft (B,g\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{/X}\webright )$.
-
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 \text{Obj}\webleft (\mathsf{Sets}_{/X}\webright )$. - Annihilation With the Empty Set. We have isomorphisms of sets natural in $\webleft (A,f\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{/X}\webright )$.
- Interaction With Products. We have an isomorphism of sets
- Symmetric Monoidality. The 8-tuple $\webleft(\mathrlap {\phantom{\lambda ^{\mathsf{Sets}_{/X}}}}\mathsf{Sets}_{/X}\right.$, $\times _{X}$, $X$, $\textbf{Sets}_{/X}$, $\alpha ^{\mathsf{Sets}_{/X}}$, $\lambda ^{\mathsf{Sets}_{/X}}$, $\rho ^{\mathsf{Sets}_{/X}}$, $\left.\sigma ^{\mathsf{Sets}_{/X}}\webright)$ is a symmetric closed monoidal category.