# mathlibdocumentation

category_theory.limits.small_complete

# Any small complete category is a preorder

We show that any small category which has all (small) limits is a preorder: In particular, we show that if a small category C in universe u has products of size u, then for any X Y : C there is at most one morphism X ⟶ Y. Note that in Lean, a preorder category is strictly one where the morphisms are in Prop, so we instead show that the homsets are subsingleton.

## References

• https://ncatlab.org/nlab/show/complete+small+category#in_classical_logic

## Tags

small complete, preorder, Freyd

@[instance]
def category_theory.has_hom.hom.subsingleton {C : Type u} {X Y : C} :

A small category with products is a thin category.

in Lean, a preorder category is one where the morphisms are in Prop, which is weaker than the usual notion of a preorder/thin category which says that each homset is subsingleton; we show the latter rather than providing a preorder C instance.