Structures · Category theory
CategoryTheory.Limits.ReflectsFiniteColimits
A functor is said to reflect finite colimits, if it reflects all colimits of shape J,
where J : Type is a finite category.
- Shape
- One type argument · adds reflects
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- CategoryTheory.HasExactLimitsOfShape.domain_of_functor
- CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves
- CategoryTheory.Limits.reflectsFiniteLimits_leftOp
- CategoryTheory.Limits.reflectsFiniteLimits_unop
- CategoryTheory.Limits.ReflectsFiniteColimits.reflects
- CategoryTheory.Limits.reflectsFiniteLimits_of_unop
- CategoryTheory.Limits.reflectsFiniteLimits_of_leftOp
- CategoryTheory.Limits.instReflectsFiniteCoproductsOfReflectsFiniteColimits
- CategoryTheory.Limits.reflectsFiniteLimits_of_op
- CategoryTheory.Limits.reflectsFiniteLimits_rightOp
- CategoryTheory.Limits.reflectsFiniteLimits_op
- CategoryTheory.Limits.reflectsFiniteLimits_of_rightOp
Ancestors0
No ancestors.