The Clowder Project

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

1. 1.

   Functoriality. The assignment $\webleft (A,B,C,f,g\webright )\mapsto A\mathbin {\textstyle \coprod _{f,C,g}}B$ defines a functor

   \[ -_{1}\mathbin {\textstyle \coprod _{-_{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}\mathbin {\textstyle \coprod _{-_{3}}}-_{1}$ is given by sending a morphism
   
   in $\mathsf{Fun}\webleft (\mathcal{P},\mathsf{Sets}\webright )$ to the map $\xi \colon A\mathbin {\textstyle \coprod _{C}}B\overset {\exists !}{\to }A'\mathbin {\textstyle \coprod _{C'}}B'$ given by
   \[ \xi \webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \phi \webleft (a\webright ) & \text{if $x=\webleft [\webleft (0,a\webright )\webright ]$},\\ \psi \webleft (b\webright ) & \text{if $x=\webleft [\webleft (1,b\webright )\webright ]$} \end{cases} \]

   for each $x\in A\mathbin {\textstyle \coprod _{C}}B$, which is the unique map making the diagram

   
   commute.

2. 2.

   Adjointness. We have an adjunction

   
   witnessed by a bijection
   \[ \mathsf{Sets}_{X/}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X}B,C\webright ),\cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{X/}\times \mathsf{Sets}_{X/}}\webleft (\webleft (A,B\webright ),\webleft (C,C\webright )\webright ) \]

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

3. 3.

   Associativity. Given a diagram

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

   where these pullbacks are built as in the diagrams

   

4. 4.

   Interaction With Composition. Given a diagram

   
   in $\mathsf{Sets}$, we have isomorphisms of sets
   \begin{align*} X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi \circ f,\psi \circ g}_{K}Y & \cong \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi ,j_{1}}_{A}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{i_{2},i_{1}}_{A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B}\webleft (\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{j_{2},\psi }_{B}Y\webright )\\ & \cong X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi ,i}_{A}\webleft (\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{j_{2},\psi }_{B}Y\webright )\\ & \cong \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{\phi ,i_{1}}_{A}\webleft (A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{f,g}_{K}B\webright )\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}^{j,\psi }_{B}Y \end{align*}

   where

   \[ \begin{aligned} j_{1} & = \mathrm{inj}^{A\times ^{f,g}_{K}B}_{1},\\ i_{1} & = \mathrm{inj}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{Y}}_{1},\\ i & = j_{1}\circ \mathrm{inj}^{\webleft (A\times ^{f,g}_{K}B\webright )\times ^{q_{2},\psi }_{B}Y}_{1}, \end{aligned} \qquad \begin{aligned} j_{2} & = \mathrm{inj}^{A\times ^{f,g}_{K}B}_{2},\\ i_{2} & = \mathrm{inj}^{X\times ^{\phi ,q_{1}}_{A\times ^{f,g}_{K}B}\webleft (A\times ^{f,g}_{K}B\webright )}_{2},\\ j & = j_{2}\circ \mathrm{inj}^{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 diagrams

   
   

5. 5.

   Unitality. We have isomorphisms of sets

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

6. 6.

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

7. 7.

   Interaction With Coproducts. We have

   

8. 8.

   Symmetric Monoidality. The triple $\webleft (\mathsf{Sets}_{X/},\mathbin {\textstyle \coprod _{X}},X\webright )$ is a symmetric monoidal category.