DefPreorder
A preorder is a set equipped with a binary relation that is both reflexive and transitive.
Prop Any preorder can be regarded as a category by taking the objects to be the elements of and taking a unique arrow, Proof For all , suppose and . We have . Since and , by transitivity, . Additionally, guarantees exists.