# Creating (co)limits #

We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

structure CategoryTheory.LiftableCone {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cone (K.comp F)) :
Type (max (max (max u₁ v₁) v₂) w)

Define the lift of a cone: For a cone c for K ⋙ F, give a cone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

We will then use this as part of the definition of creation of limits: every limit cone has a lift.

Note this definition is really only useful when c is a limit already.

• liftedCone :

a cone in the source category of the functor

• validLift : F.mapCone self.liftedCone c

the isomorphism expressing that liftedCone lifts the given cone

Instances For
structure CategoryTheory.LiftableCocone {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cocone (K.comp F)) :
Type (max (max (max u₁ v₁) v₂) w)

Define the lift of a cocone: For a cocone c for K ⋙ F, give a cocone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

We will then use this as part of the definition of creation of colimits: every limit cocone has a lift.

Note this definition is really only useful when c is a colimit already.

• liftedCocone :

a cocone in the source category of the functor

• validLift : F.mapCocone self.liftedCocone c

the isomorphism expressing that liftedCocone lifts the given cocone

Instances For
class CategoryTheory.CreatesLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) extends :
Type (max (max (max (max u₁ u₂) v₁) v₂) w)

Definition 3.3.1 of [Riehl]. We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

If F reflects isomorphisms, it suffices to show only that the lifted cone is a limit - see createsLimitOfReflectsIso.

Instances
class CategoryTheory.CreatesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

F creates limits of shape J if F creates the limit of any diagram K : J ⥤ C.

• CreatesLimit : {K : } →
Instances
class CategoryTheory.CreatesLimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

F creates limits if it creates limits of shape J for any J.

• CreatesLimitsOfShape : {J : Type w} → [inst : ] →
Instances
@[reducible, inline]
abbrev CategoryTheory.CreatesLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

F creates small limits if it creates limits of shape J for any small J.

Equations
Instances For
class CategoryTheory.CreatesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) extends :
Type (max (max (max (max u₁ u₂) v₁) v₂) w)

Dual of definition 3.3.1 of [Riehl]. We say that F creates colimits of K if, given any limit cocone c for K ⋙ F (i.e. below) we can lift it to a cocone "above", and further that F reflects limits for K.

If F reflects isomorphisms, it suffices to show only that the lifted cocone is a limit - see createsColimitOfReflectsIso.

Instances
class CategoryTheory.CreatesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

F creates colimits of shape J if F creates the colimit of any diagram K : J ⥤ C.

• CreatesColimit : {K : } →
Instances
class CategoryTheory.CreatesColimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

F creates colimits if it creates colimits of shape J for any small J.

• CreatesColimitsOfShape : {J : Type w} → [inst : ] →
Instances
@[reducible, inline]
abbrev CategoryTheory.CreatesColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

F creates small colimits if it creates colimits of shape J for any small J.

Equations
Instances For
def CategoryTheory.liftLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {c : CategoryTheory.Limits.Cone (K.comp F)} :

liftLimit t is the cone for K given by lifting the limit t for K ⋙ F.

Equations
• = .liftedCone
Instances For
def CategoryTheory.liftedLimitMapsToOriginal {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {c : CategoryTheory.Limits.Cone (K.comp F)} :
F.mapCone c

The lifted cone has an image isomorphic to the original cone.

Equations
Instances For
def CategoryTheory.liftedLimitIsLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {c : CategoryTheory.Limits.Cone (K.comp F)} :

The lifted cone is a limit.

Equations
Instances For
theorem CategoryTheory.hasLimit_of_created {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [CategoryTheory.Limits.HasLimit (K.comp F)] :

If F creates the limit of K and K ⋙ F has a limit, then K has a limit.

theorem CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (F : ) :

If F creates limits of shape J, and D has limits of shape J, then C has limits of shape J.

theorem CategoryTheory.hasLimits_of_hasLimits_createsLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] [] :

If F creates limits, and D has all limits, then C has all limits.

def CategoryTheory.liftColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {c : CategoryTheory.Limits.Cocone (K.comp F)} :

liftColimit t is the cocone for K given by lifting the colimit t for K ⋙ F.

Equations
• = .liftedCocone
Instances For
def CategoryTheory.liftedColimitMapsToOriginal {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {c : CategoryTheory.Limits.Cocone (K.comp F)} :
F.mapCocone c

The lifted cocone has an image isomorphic to the original cocone.

Equations
Instances For
def CategoryTheory.liftedColimitIsColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {c : CategoryTheory.Limits.Cocone (K.comp F)} :

The lifted cocone is a colimit.

Equations
Instances For
theorem CategoryTheory.hasColimit_of_created {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [CategoryTheory.Limits.HasColimit (K.comp F)] :

If F creates the limit of K and K ⋙ F has a limit, then K has a limit.

If F creates colimits of shape J, and D has colimits of shape J, then C has colimits of shape J.

theorem CategoryTheory.hasColimits_of_hasColimits_createsColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] [] :

If F creates colimits, and D has all colimits, then C has all colimits.

@[instance 10]
instance CategoryTheory.reflectsLimitsOfShapeOfCreatesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (F : ) :
Equations
• = { reflectsLimit := fun {K : } => inferInstance }
@[instance 10]
instance CategoryTheory.reflectsLimitsOfCreatesLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :
Equations
• = { reflectsLimitsOfShape := fun {J : Type w'} [] => inferInstance }
@[instance 10]
instance CategoryTheory.reflectsColimitsOfShapeOfCreatesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (F : ) :
Equations
• = { reflectsColimit := fun {K : } => inferInstance }
@[instance 10]
instance CategoryTheory.reflectsColimitsOfCreatesColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :
Equations
• = { reflectsColimitsOfShape := fun {J : Type w'} [] => inferInstance }
structure CategoryTheory.LiftsToLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cone (K.comp F)) extends :
Type (max (max (max u₁ v₁) v₂) w)

A helper to show a functor creates limits. In particular, if we can show that for any limit cone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates limits. Usually, F creating limits says that any lift of c is a limit, but here we only need to show that our particular lift of c is a limit.

Instances For
structure CategoryTheory.LiftsToColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cocone (K.comp F)) extends :
Type (max (max (max u₁ v₁) v₂) w)

A helper to show a functor creates colimits. In particular, if we can show that for any limit cocone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates colimits. Usually, F creating colimits says that any lift of c is a colimit, but here we only need to show that our particular lift of c is a colimit.

Instances For
def CategoryTheory.createsLimitOfReflectsIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.ReflectsIsomorphisms] (h : (c : CategoryTheory.Limits.Cone (K.comp F)) → (t : ) → ) :

If F reflects isomorphisms and we can lift any limit cone to a limit cone, then F creates limits. In particular here we don't need to assume that F reflects limits.

Equations
Instances For
def CategoryTheory.createsLimitOfReflectsIso' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.ReflectsIsomorphisms] {c : CategoryTheory.Limits.Cone (K.comp F)} (hc : ) (h : ) :

If F reflects isomorphisms and we can lift a single limit cone to a limit cone, then F creates limits. Note that unlike createsLimitOfReflectsIso, to apply this result it is necessary to know that K ⋙ F actually has a limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfLift' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] {l : CategoryTheory.Limits.Cone (K.comp F)} (hl : ) (c : ) (i : F.mapCone c l) :

When F is fully faithful, to show that F creates the limit for K it suffices to exhibit a lift of a limit cone for K ⋙ F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfLift {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] [CategoryTheory.Limits.HasLimit (K.comp F)] (c : ) (i : F.mapCone c CategoryTheory.Limits.limit.cone (K.comp F)) :

When F is fully faithful, and HasLimit (K ⋙ F), to show that F creates the limit for K it suffices to exhibit a lift of the chosen limit cone for K ⋙ F.

Equations
Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfIso' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] {l : CategoryTheory.Limits.Cone (K.comp F)} (hl : ) (X : C) (i : F.obj X l.pt) :

When F is fully faithful, to show that F creates the limit for K it suffices to show that a limit point is in the essential image of F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] [CategoryTheory.Limits.HasLimit (K.comp F)] (X : C) (i : F.obj X CategoryTheory.Limits.limit (K.comp F)) :

When F is fully faithful, and HasLimit (K ⋙ F), to show that F creates the limit for K it suffices to show that the chosen limit point is in the essential image of F.

Equations
Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfPreserves {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] :

A fully faithful functor that preserves a limit that exists also creates the limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[instance 100]
instance CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [CategoryTheory.Limits.HasLimit (K.comp F)] :

F preserves the limit of K if it creates the limit and K ⋙ F has the limit.

Equations
• One or more equations did not get rendered due to their size.
@[instance 100]

F preserves the limit of shape J if it creates these limits and D has them.

Equations
• = { preservesLimit := fun {K : } => inferInstance }
@[instance 100]
instance CategoryTheory.preservesLimitsOfCreatesLimitsAndHasLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] [] :

F preserves limits if it creates limits and D has limits.

Equations
• = { preservesLimitsOfShape := fun {J : Type w'} [] => inferInstance }
def CategoryTheory.createsColimitOfReflectsIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.ReflectsIsomorphisms] (h : (c : CategoryTheory.Limits.Cocone (K.comp F)) → (t : ) → ) :

If F reflects isomorphisms and we can lift any colimit cocone to a colimit cocone, then F creates colimits. In particular here we don't need to assume that F reflects colimits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsColimitOfReflectsIso' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.ReflectsIsomorphisms] {c : CategoryTheory.Limits.Cocone (K.comp F)} (hc : ) (h : ) :

If F reflects isomorphisms and we can lift a single colimit cocone to a colimit cocone, then F creates limits. Note that unlike createsColimitOfReflectsIso, to apply this result it is necessary to know that K ⋙ F actually has a colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfLift' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] {l : CategoryTheory.Limits.Cocone (K.comp F)} (hl : ) (c : ) (i : F.mapCocone c l) :

When F is fully faithful, to show that F creates the colimit for K it suffices to exhibit a lift of a colimit cocone for K ⋙ F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfLift {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] [CategoryTheory.Limits.HasColimit (K.comp F)] (c : ) (i : F.mapCocone c CategoryTheory.Limits.colimit.cocone (K.comp F)) :

When F is fully faithful, and HasColimit (K ⋙ F), to show that F creates the colimit for K it suffices to exhibit a lift of the chosen colimit cocone for K ⋙ F.

Equations
Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfPreserves {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] :

A fully faithful functor that preserves a colimit that exists also creates the colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfIso' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] {l : CategoryTheory.Limits.Cocone (K.comp F)} (hl : ) (X : C) (i : F.obj X l.pt) :

When F is fully faithful, to show that F creates the colimit for K it suffices to show that a colimit point is in the essential image of F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } [F.Full] [F.Faithful] [CategoryTheory.Limits.HasColimit (K.comp F)] (X : C) (i : F.obj X CategoryTheory.Limits.colimit (K.comp F)) :

When F is fully faithful, and HasColimit (K ⋙ F), to show that F creates the colimit for K it suffices to show that the chosen colimit point is in the essential image of F.

Equations
Instances For
@[instance 100]
instance CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [CategoryTheory.Limits.HasColimit (K.comp F)] :

F preserves the colimit of K if it creates the colimit and K ⋙ F has the colimit.

Equations
• One or more equations did not get rendered due to their size.
@[instance 100]

F preserves the colimit of shape J if it creates these colimits and D has them.

Equations
• = { preservesColimit := fun {K : } => inferInstance }
@[instance 100]
instance CategoryTheory.preservesColimitsOfCreatesColimitsAndHasColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] [] :

F preserves limits if it creates limits and D has limits.

Equations
• = { preservesColimitsOfShape := fun {J : Type w'} [] => inferInstance }
def CategoryTheory.createsLimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) [] :

Transfer creation of limits along a natural isomorphism in the diagram.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsLimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {G : } (h : F G) :

If F creates the limit of K and F ≅ G, then G creates the limit of K.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsLimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

If F creates limits of shape J and F ≅ G, then G creates limits of shape J.

Equations
• = { CreatesLimit := fun {K : } => }
Instances For
def CategoryTheory.createsLimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

If F creates limits and F ≅ G, then G creates limits.

Equations
• = { CreatesLimitsOfShape := fun {J : Type w'} [] => }
Instances For
def CategoryTheory.createsColimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) :

Transfer creation of colimits along a natural isomorphism in the diagram.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsColimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {G : } (h : F G) :

If F creates the colimit of K and F ≅ G, then G creates the colimit of K.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.createsColimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

If F creates colimits of shape J and F ≅ G, then G creates colimits of shape J.

Equations
• = { CreatesColimit := fun {K : } => }
Instances For
def CategoryTheory.createsColimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

If F creates colimits and F ≅ G, then G creates colimits.

Equations
• = { CreatesColimitsOfShape := fun {J : Type w'} [] => }
Instances For
def CategoryTheory.liftsToLimitOfCreates {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cone (K.comp F)) :

If F creates the limit of K, any cone lifts to a limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.liftsToColimitOfCreates {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cocone (K.comp F)) :

If F creates the colimit of K, any cocone lifts to a colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.idLiftsCone {C : Type u₁} [] {J : Type w} {K : } (c : CategoryTheory.Limits.Cone (K.comp )) :

Any cone lifts through the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.idCreatesLimits {C : Type u₁} [] :

The identity functor creates all limits.

Equations
• One or more equations did not get rendered due to their size.
def CategoryTheory.idLiftsCocone {C : Type u₁} [] {J : Type w} {K : } (c : ) :

Any cocone lifts through the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.idCreatesColimits {C : Type u₁} [] :

The identity functor creates all colimits.

Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.inhabitedLiftableCone {C : Type u₁} [] {J : Type w} {K : } (c : CategoryTheory.Limits.Cone (K.comp )) :

Satisfy the inhabited linter

Equations
• = { default := }
instance CategoryTheory.inhabitedLiftableCocone {C : Type u₁} [] {J : Type w} {K : } (c : ) :
Equations
• = { default := }
instance CategoryTheory.inhabitedLiftsToLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cone (K.comp F)) :

Satisfy the inhabited linter

Equations
• = { default := }
instance CategoryTheory.inhabitedLiftsToColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) (c : CategoryTheory.Limits.Cocone (K.comp F)) :
Equations
• = { default := }
instance CategoryTheory.compCreatesLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.CreatesLimit (K.comp F) G] :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.compCreatesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
Equations
• = { CreatesLimit := fun {K : } => inferInstance }
instance CategoryTheory.compCreatesLimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :
Equations
• = { CreatesLimitsOfShape := fun {J : Type w'} [] => inferInstance }
instance CategoryTheory.compCreatesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.CreatesColimit (K.comp F) G] :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.compCreatesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
Equations
• = { CreatesColimit := fun {K : } => inferInstance }
instance CategoryTheory.compCreatesColimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :
Equations
• = { CreatesColimitsOfShape := fun {J : Type w'} [] => inferInstance }