Category, object, morphism, domain, codomain, identity, composition, and hom-collection

Under the definable-class convention of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why $\mathbf{C}\mathbf{A}\mathbf{T}$ is not formed, every class below is a formula and every function whose domain may be proper-class-sized is a definable class-function schema. When its domain is a set, it is an ordinary set-valued function.

A category $\mathcal{C}$ consists of a class $\mathrm{Ob}(\mathcal{C})$ of objects, a class $\mathrm{Mor}(\mathcal{C})$ of morphisms, functions $\mathrm{dom},\mathrm{cod}:\mathrm{Mor}(\mathcal{C})\to \mathrm{Ob}(\mathcal{C})$, an identity morphism $1_A:A\to A$ for every object $A$, and a composite $g\circ f:A\to C$ whenever $f:A\to B$ and $g:B\to C$.

These data satisfy, whenever the composites are defined,

$h\circ (g\circ f)=(h\circ g)\circ f,1_B\circ f=f=f\circ 1_A\mathrm{.}$

We write $\mathcal{C}(A,B)$, or ${\mathrm{Hom}}_{\mathcal{C}}(A,B)$, for the hom-collection of morphisms with domain $A$ and codomain $B$. The object class is allowed to be empty; then the morphism class is empty and all axioms are vacuous.

Morphisms carry their domain and codomain. A category is often presented the other way round, by saying what the morphisms from $A$ to $B$ are for each pair of objects. When it is, $\mathrm{Mor}(\mathcal{C})$ is the disjoint union of those hom-collections: a morphism is a triple $(A,B,f)$ with $f$ in the collection assigned to $(A,B)$, and $\mathrm{dom}$ and $\mathrm{cod}$ are the first two projections, which are then functions in the required sense. This is not a technicality that can be dropped. In this library a function is a set of ordered pairs and does not determine a codomain (A function is a relation $f$ with $(a,b)\in f$ and $(a,c)\in f$ implying $b=c$; $f:A\to B$, the value $f(a)$, domain and codomain), so the empty function is a function $\mathrm{\varnothing }\to B$ for every $B$ at once; reading the morphisms of $\mathbf{S}\mathbf{e}\mathbf{t}$ as bare functions would give that one set two different codomains and leave $\mathrm{cod}$ undefined. Every concrete category below whose morphisms are described as structure-preserving maps is to be read with this tagging, and each hom-collection is then in canonical bijection with the corresponding collection of untagged maps, so no size or smallness claim is affected.