Description:( SetCat2o ) is a category (provable from setccat and 2oex )
that does not have pairwise disjoint hom-sets, proved by this theorem
combined with setc2obas . Notably, the empty set (/) is
simultaneously an object ( setc2obas ) , an identity morphism from
(/) to (/) , and a non-identity morphism from (/) to
1o . See cat1lem and cat1 for a more general statement. This
category is also thin ( setc2othin ), and therefore is "equivalent" to
a preorder (actually a partial order). See prsthinc for more details
on the "equivalence". (Contributed by Zhi Wang, 24-Sep-2024)