Structures · Category theory
CategoryTheory.Limits.HasFiniteWidePullbacks
A category HasFiniteWidePullbacks if it has all limits of shape WidePullbackShape J for
finite J, i.e. if it has a wide pullback for every finite collection of morphisms with the same
codomain.
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape
- CategoryTheory.Over.ConstructProducts.over_finiteProducts_of_finiteWidePullbacks
- CategoryTheory.Limits.HasFiniteWidePullbacks.out
- CategoryTheory.MorphismProperty.Over.instHasFiniteLimitsTopOfHasFiniteWidePullbacks
- CategoryTheory.Over.hasFiniteLimits
- CategoryTheory.Limits.instHasFiniteWidePushoutsOppositeOfHasFiniteWidePullbacks
Ancestors0
No ancestors.