Let $A$, $B$, and $C$ be sets.
-
Associativity. We have isomorphisms of sets1 where $\text{CoEq}\webleft (f,g,h\webright )$ is the colimit of the diagram\[ \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 )}, \]
in $\mathsf{Sets}$.
-
Unitality. We have an isomorphism of sets
\[ \text{CoEq}\webleft (f,f\webright )\cong B. \]
-
Commutativity. We have an isomorphism of sets
\[ \text{CoEq}\webleft (f,g\webright ) \cong \text{CoEq}\webleft (g,f\webright ). \]
-
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$.
1That is, the following three ways of forming “the” coequaliser of $\webleft (f,g,h\webright )$ agree:
- Take the coequaliser of $\webleft (f,g,h\webright )$, i.e. the colimit of the diagram
in $\mathsf{Sets}$.
- First take the coequaliser of $f$ and $g$, forming a diagram
\[ A\underset {g}{\overset {f}{\rightrightarrows }}B\overset {\text{coeq}\webleft (f,g\webright )}{\twoheadrightarrow }\text{CoEq}\webleft (f,g\webright ) \]
and then take the coequaliser of the composition
\[ A\underset {h}{\overset {f}{\rightrightarrows }}B\overset {\text{coeq}\webleft (f,g\webright )}{\twoheadrightarrow }\text{CoEq}\webleft (f,g\webright ), \]obtaining a quotient
of $\text{CoEq}\webleft (f,g\webright )$\[ \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 ) \] - First take the coequaliser of $g$ and $h$, forming a diagram
\[ A\underset {h}{\overset {g}{\rightrightarrows }}B\overset {\text{coeq}\webleft (g,h\webright )}{\twoheadrightarrow }\text{CoEq}\webleft (g,h\webright ) \]
and then take the coequaliser of the composition
\[ A\underset {g}{\overset {f}{\rightrightarrows }}B\overset {\text{coeq}\webleft (g,h\webright )}{\twoheadrightarrow }\text{CoEq}\webleft (g,h\webright ), \]obtaining a quotient
of $\text{CoEq}\webleft (g,h\webright )$.\[ \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 ) \]
