<-- Go Back Last Updated: 11/01/2025
A category \(C=(C_0,C_1,\mathrm{dom},\mathrm{cod},1,\circ)\) consists of a collection (formally a member of some Grothendieck universe) \(C_0\) of 'objects', a collection \(C_1\) of 'arrows' (or 'morphisms'), functions \(\mathrm{dom},\mathrm{cod}:C_1\to C_0\) which assign to each arrow its domain (source) and codomain (target) respectively, a function \(1:C_0\to C_1,X\mapsto 1_X\) which assigns to each object an 'identity arrow', and a partial function \(\circ:C_1\times C_1\to C_1, (f,g)\mapsto f\circ g\) so that \(f\circ g\) is defined precisely when \(\mathrm{dom}(f)=\mathrm{cod}(g)\), 'function composition'. The identity map must satisfy \(\forall X\in C_0:\mathrm{dom}(1_X)=\mathrm{cod}(1_X)=X\), and the composition (where it is defined) must satisfy \(\mathrm{dom}(f\circ g)=\mathrm{dom}(g)\) and \(\mathrm{cod}(f\circ g)=\mathrm{cod}(f)\). Composition must be associative, so that \(\forall f,g,h\in C_1:(\mathrm{dom}(f)=\mathrm{cod}(g)\land\mathrm{dom}(g)=\mathrm{cod}(h))\Rightarrow f\circ(g\circ h)=(f\circ g)\circ h\), and unital via the identity, i.e. \(\forall X\in C_0:\forall f\in C_1:(\mathrm{dom}(f)=X\Rightarrow f\circ 1_X=f)\land(\mathrm{cod}(f)=X\Rightarrow 1_X\circ f=f)\).