Definition 4.9.1.  Let u ∈ ℕ, S be a set. We define:
Disu(S) := [S({a} ∩ {b})a,b ∈ S(c)c ∈ S(({e} ∩ {f}) × ({d} ∩ {e}) → ({d} ∩ {f})x ↦ e)d,e,f ∈ S]u is a/an u-small category
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.