A sparse category is a category with at most one morphism between each pair of objects.
Examples include posets, but many indexing categories (diagrams) for special shapes of (co)limits.
To construct a category instance one only needs to specify the category_struct part,
as the axioms hold for free.
def
category_theory.sparse_category
{C : Type u}
[category_theory.category_struct C]
[∀ (X Y : C), subsingleton (X ⟶ Y)] :
Construct a category instance from a category_struct, using the fact that hom spaces are subsingletons to prove the axioms.
Equations
- category_theory.sparse_category = {to_category_struct := _inst_1, id_comp' := _, comp_id' := _, assoc' := _}