The Clowder Project

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

1. Associativity. We have isomorphisms of sets^[1]
   \[ \underbrace{\text{CoEq}\webleft (\text{coeq}\webleft (f,g\webright )\circ f,\text{coeq}\webleft (f,g\webright )\circ h\webright )}_{{}=\text{CoEq}\webleft (\text{coeq}\webleft (f,g\webright )\circ g,\text{coeq}\webleft (f,g\webright )\circ h\webright )}\cong \text{CoEq}\webleft (f,g,h\webright ) \cong \underbrace{\text{CoEq}\webleft (\text{coeq}\webleft (g,h\webright )\circ f,\text{coeq}\webleft (g,h\webright )\circ g\webright )}_{{}=\text{CoEq}\webleft (\text{coeq}\webleft (g,h\webright )\circ f,\text{coeq}\webleft (g,h\webright )\circ h\webright )}, \]

   where $\text{CoEq}\webleft (f,g,h\webright )$ is the colimit of the diagram
   

   in $\mathsf{Sets}$.

2. Unitality. We have an isomorphism of sets
   \[ \text{CoEq}\webleft (f,f\webright )\cong B. \]
3. Commutativity. We have an isomorphism of sets
   \[ \text{CoEq}\webleft (f,g\webright ) \cong \text{CoEq}\webleft (g,f\webright ). \]
4. Interaction With Composition. Let
   \[ A \underset {g}{\overset {f}{\rightrightarrows }} B \underset {k}{\overset {h}{\rightrightarrows }} C \]

   be functions. We have a surjection

   \[ \text{CoEq}\webleft (h\circ f,k\circ g\webright )\twoheadrightarrow \text{CoEq}\webleft (\text{coeq}\webleft (h,k\webright )\circ h\circ f,\text{coeq}\webleft (h,k\webright )\circ k\circ g\webright ) \]

   exhibiting $\text{CoEq}\webleft (\text{coeq}\webleft (h,k\webright )\circ h\circ f,\text{coeq}\webleft (h,k\webright )\circ k\circ g\webright )$ as a quotient of $\text{CoEq}\webleft (h\circ f,k\circ g\webright )$ by the relation generated by declaring $h\webleft (y\webright )\sim k\webleft (y\webright )$ for each $y\in B$.