Mathlib Map

Structures · Category theory

CategoryTheory.Limits.HasLimitsOfSize

C has all limits of size v₁ u₁ (HasLimitsOfSize.{v₁ u₁} C) if it has limits of every shape J : Type u₁ with [Category.{v₁} J].

Defined in
Mathlib.CategoryTheory.Limits.HasLimits
Shape
One type argument · adds has_limits_of_shape
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances30

  • CategoryTheory.Functor
  • CategoryTheory.Over
  • CategoryTheory.Discrete
  • ModuleCat
  • AddCommGrpCat
  • TopCat
  • CommGrpCat
  • GrpCat
  • AddGrpCat
  • SheafOfModules
  • CategoryTheory.Skeleton
  • CategoryTheory.Comma
  • CommRingCat
  • PresheafOfModules
  • CategoryTheory.Sheaf
  • CategoryTheory.StructuredArrow
  • CommMonCat
  • AddCommMonCat
  • TopCat.Sheaf
  • MonCat
  • AddMonCat
  • RingCat
  • CommSemiRingCat
  • SemiRingCat
  • CategoryTheory.Subobject
  • CondensedSet
  • CategoryTheory.ThinSkeleton
  • CategoryTheory.MonoOver
  • CondensedMod
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by97

Ancestors0

No ancestors.