The Clowder Project

Let $A$, $B$, $C$, and $X$ be sets.

1. 1.

   Functoriality. The assignment $(A,B,C,f,g)\mapsto A\times _{f,C,g}B$ defines a functor

   \[ -_{1}\times _{-_{3}}-_{1}\colon \mathsf{Fun}(\mathcal{P},\mathsf{Sets})\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}(\mathcal{P},\mathsf{Sets})$ to the map $\xi \colon A\times _{C}B\overset {\exists !}{\to }A'\times _{C'}B'$ given by
   \[ \xi (a,b)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\phi (a),\psi (b)) \]

   for each $(a,b)\in A\times _{C}B$, which is the unique map making the diagram

   
   commute.

2. 2.

   Adjointness I. We have adjunctions

   
   witnessed by bijections
   \begin{align*} \mathsf{Sets}_{/X}(A\times _{X}B,C) & \cong \mathsf{Sets}_{/X}(A,\boldsymbol {\mathsf{Sets}}_{/X}(B,C)),\\ \mathsf{Sets}_{/X}(A\times _{X}B,C) & \cong \mathsf{Sets}_{/X}(B,\boldsymbol {\mathsf{Sets}}_{/X}(A,C)), \end{align*}

   natural in $(A,\phi _{A}),(B,\phi _{B}),(C,\phi _{C})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{/X})$, where $\boldsymbol {\mathsf{Sets}}_{/X}(A,B)$ is the object of $\mathsf{Sets}_{/X}$ consisting of (see , ):

   • •

     The Set. The set $\boldsymbol {\mathsf{Sets}}_{/X}(A,B)$ defined by

     \[ \boldsymbol {\mathsf{Sets}}_{/X}(A,B)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\coprod _{x\in X}\mathsf{Sets}(\phi ^{-1}_{A}(x),\phi ^{-1}_{Y}(x)) \]
   • •

     The Map to $X$. The map

     \[ \phi _{\boldsymbol {\mathsf{Sets}}_{/X}(A,B)}\colon \boldsymbol {\mathsf{Sets}}_{/X}(A,B)\to X \]

     defined by

     \[ \phi _{\boldsymbol {\mathsf{Sets}}_{/X}(A,B)}(x,f)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x \]

     for each $(x,f)\in \boldsymbol {\mathsf{Sets}}_{/X}(A,B)$.

3. 3.

   Adjointness II. We have an adjunction

   
   witnessed by a bijection
   \[ \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{/X}\times \mathsf{Sets}_{/X}}((A,A),(B,C))\cong \mathsf{Sets}_{/X}(A,B\times _{X}C), \]

   natural in $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{/X})$ and in $(B,C)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{/X}\times \mathsf{Sets}_{/X})$.

4. 4.

   Associativity. Given a diagram

   
   in $\mathsf{Sets}$, we have isomorphisms of sets
   \[ (A\times _{X}B)\times _{Y}C\cong (A\times _{X}B)\times _{B}(B\times _{Y}C) \cong A\times _{X}(B\times _{Y}C), \]

   where these pullbacks are built as in the diagrams

   

5. 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 (X\times ^{\phi ,q_{1}}_{A}(A\times ^{f,g}_{K}B))\times ^{p_{2},p_{1}}_{A\times ^{f,g}_{K}B}((A\times ^{f,g}_{K}B)\times ^{q_{2},\psi }_{B}Y)\\ & \cong X\times ^{\phi ,p}_{A}((A\times ^{f,g}_{K}B)\times ^{q_{2},\psi }_{B}Y)\\ & \cong (X\times ^{\phi ,q_{1}}_{A}(A\times ^{f,g}_{K}B))\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}}}^{(A\times ^{f,g}_{K}B)\times ^{q_{2},\psi }_{Y}}_{1},\\ p & = q_{1}\circ \operatorname {\mathrm{\mathrm{pr}}}^{(A\times ^{f,g}_{K}B)\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}(A\times ^{f,g}_{K}B)}_{2},\\ q & = q_{2}\circ \operatorname {\mathrm{\mathrm{pr}}}^{X\times ^{\phi ,q_{1}}_{A}(A\times ^{f,g}_{K}B)}_{2}, \end{aligned} \]

   and where these pullbacks are built as in the following diagrams:

   
   

6. 6.

   Unitality. We have isomorphisms of sets

   
   natural in $(A,f)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{/X})$.

7. 7.

   Commutativity. We have an isomorphism of sets

   
   natural in $(A,f),(B,g)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{/X})$.

8. 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}(B\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}C) \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(A\times _{X}B)\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(A\times _{X}C),\\ \delta ^{\mathsf{Sets}_{/X}}_{r} & \colon (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B)\times _{X}C \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(A\times _{X}C)\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}(B\times _{X}C), \end{align*}

   as in the diagrams

   
   natural in $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{/X})$.

9. 9.

   Annihilation With the Empty Set. We have isomorphisms of sets

   
   natural in $(A,f)\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{/X})$.

10. 10.

    Interaction With Products. We have an isomorphism of sets

    

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