The Clowder Project

Let $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ be pointed sets and let $f,g,h\colon \webleft (X,x_{0}\webright )\to \webleft (Y,y_{0}\webright )$ be morphisms of pointed sets.

1. Associativity. We have isomorphisms of pointed sets
   \[ \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 pointed sets
   \[ \text{CoEq}\webleft (f,f\webright )\cong B. \]
3. Commutativity. We have an isomorphism of pointed sets
   \[ \text{CoEq}\webleft (f,g\webright ) \cong \text{CoEq}\webleft (g,f\webright ). \]