Definition 4.9.1.  Let u ∈ , S be a set. We define:
Remarks.

This is one possible formalization of the discrete category obtained from elements of S. We simply define morphisms to be elements of S as well, such that %setEquals($../Morphisms(u = u, 𝓒 =$elements(u = u, S = S), 𝐗 = a, 𝐘 = a), %enumeration($../identity(u = u, 𝓒 =$elements(u = u, S = S), 𝐗 = a)), %enumeration(a)), and %setEquals($../Morphisms(u = u, 𝓒 =$elements(u = u, S = S), 𝐗 = a, 𝐘 = b), \$../../Essentials/Sets/"Empty set") if %not(%equals(a, b)).

(Note that the existence of x in the definition of morphism composition implies that %equals(d, e, f).)

References.