feat(category_theory/limits): Any small complete category is a preorder (#4907)
feat(category_theory/limits): Any small complete category is a preorder (#4907)

Show that any small complete category has subsingleton homsets.

Not sure if this is useful for anything - maybe it shouldn't be an instance



leanprover-community/mathlib,leanprover-community/mathlib