Thin categories #
A thin category (also known as a sparse category) is a category with at most one morphism between each pair of objects.
Examples include posets, but also some indexing categories (diagrams) for special shapes of (co)limits.
To construct a category instance one only needs to specify the
as the axioms hold for free.
C is thin, then the category of functors to
C is also thin.
Further, to show two objects are isomorphic in a thin category, it suffices only to give a morphism
in each direction.
Construct a category instance from a category_struct, using the fact that hom spaces are subsingletons to prove the axioms.
X ≅ Y in a thin category, it suffices to just give any morphism in each direction.