mathlib

246df99f - 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