Structures · Category theory
CategoryTheory.Limits.HasLimit
HasLimit F represents the mere existence of a limit for F.
- Defined in
- Mathlib.CategoryTheory.Limits.HasLimits
- Shape
- One type argument · adds exists_limit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances6
- CategoryTheory.Discrete
- CategoryTheory.Limits.WalkingParallelPair
- CategoryTheory.Limits.WidePullbackShape
- CategoryTheory.Limits.WalkingCospan
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by268
- CategoryTheory.Limits.limit
- CategoryTheory.Limits.limit.π
- CategoryTheory.Limits.limit.lift_π
- CategoryTheory.Limits.limit.isLimit
- CategoryTheory.Limits.limit.cone
- CategoryTheory.Limits.limit.lift_π_assoc
- CategoryTheory.Limits.limit.lift
- CategoryTheory.Limits.HasLimit.isoOfNatIso
- CategoryTheory.Limits.limit.hom_ext
- CategoryTheory.Limits.limMap
- CategoryTheory.Limits.limit.isoLimitCone_inv_π
- CategoryTheory.preservesLimitIso
- CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π
- CategoryTheory.Limits.hasLimit_of_iso
- CategoryTheory.Limits.limit.w
- CategoryTheory.Limits.limMap_π
- CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp
- CategoryTheory.Limits.Types.limit_ext
- CategoryTheory.Limits.limit.pre
- CategoryTheory.Limits.limit.post
- CategoryTheory.hasLimit_of_created
- CategoryTheory.Limits.Pi.isoLimit
- CategoryTheory.Limits.limit.isoLimitCone_hom_π
- CategoryTheory.Limits.limit.isoLimitCone
- CategoryTheory.preservesLimitIso_hom_π
- CategoryTheory.Limits.HasLimit.isoOfEquivalence
- CategoryTheory.Limits.limit.pre_π
- CategoryTheory.Limits.limitUncurryIsoLimitCompLim
- CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp
- CategoryTheory.Functor.limitIsoOfIsRightKanExtension
- CategoryTheory.Limits.limit.post_π
- CategoryTheory.Limits.Concrete.limit_ext
- CategoryTheory.Limits.limitIsoLimitCurryCompLim
- CategoryTheory.Limits.HasLimit.isoOfNatIso_inv_π
- CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π
- CategoryTheory.Limits.Types.Limit.π_mk
- CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂
- CategoryTheory.Limits.colimitUnopIsoOpLimit
- CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π
- CategoryTheory.Limits.limMap_π_apply
- CategoryTheory.Limits.colimitLeftOpIsoUnopLimit
- CategoryTheory.Limits.Types.limitEquivSections
- CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc
- CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit
- CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π
- CategoryTheory.Limits.Concrete.small_sections_of_hasLimit
- CategoryTheory.Limits.colimitOpIsoOpLimit
- CategoryTheory.Limits.colimitRightOpIsoUnopLimit
- CategoryTheory.preservesLimitIso_inv_π
- CategoryTheory.Limits.HasLimit.isoOfEquivalence_inv_π
Ancestors0
No ancestors.