The Clowder Project

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. 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 )$.

3. 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

   

4. 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:

   
   

5. Unitality. We have isomorphisms of sets
   
   natural in $\webleft (A,f\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{/X}\webright )$.
6. 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 )$.
7. 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 )$.

8. Annihilation With the Empty Set. We have isomorphisms of sets
   
   natural in $\webleft (A,f\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{/X}\webright )$.
9. Interaction With Products. We have an isomorphism of sets
   
10. 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.