# 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 100]

instance
CategoryTheory.instIsThin
{C : Type u}
[CategoryTheory.SmallCategory C]
[CategoryTheory.Limits.HasProducts 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.

## Equations

- ⋯ = ⋯