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 #
Tags #
small complete, preorder, Freyd
@[protected, instance]
def
category_theory.quiver.hom.subsingleton
{C : Type u}
[category_theory.small_category C]
[category_theory.limits.has_products C]
{X Y : C} :
subsingleton (X ⟶ Y)
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.