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{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),g\circ \text{eq}\webleft (g,h\webright )\webright )}_{{}=\text{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),h\circ \text{eq}\webleft (g,h\webright )\webright )}\cong \text{Eq}\webleft (f,g,h\webright ) \cong \underbrace{\text{Eq}\webleft (f\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright )}_{{}=\text{Eq}\webleft (g\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright )}, \]

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

   in $\mathsf{Sets}_{*}$, being explicitly given by

   \[ \text{Eq}\webleft (f,g,h\webright )\cong \webleft\{ a\in A\ \middle |\ f\webleft (a\webright )=g\webleft (a\webright )=h\webleft (a\webright )\webright\} . \]
2. Unitality. We have an isomorphism of pointed sets
   \[ \text{Eq}\webleft (f,f\webright )\cong X. \]
3. Commutativity. We have an isomorphism of pointed sets
   \[ \text{Eq}\webleft (f,g\webright ) \cong \text{Eq}\webleft (g,f\webright ). \]