Limits and colimits indexed by preorders #
In this file, we obtain the following very basic results
about limits and colimits indexed by a preordered type J:
- a least element in
Jimplies the existence of all limits indexed byJ - a greatest element in
Jimplies the existence of all colimits indexed byJ
instance Preorder.instHasLimitsOfShape (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type w) [Preorder J] [OrderBot J] :
instance Preorder.instHasColimitsOfShape (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type w) [Preorder J] [OrderTop J] :