The Clowder Project

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

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

   

3. Unitality. We have isomorphisms of sets
   
4. Commutativity. We have an isomorphism of sets
   
5. Interaction With Coproducts. We have
   
6. Symmetric Monoidality. The triple $\webleft (\mathsf{Sets},\mathbin {\textstyle \coprod _{X}},X\webright )$ is a symmetric monoidal category.