Mathlib Map

Structures · Category theory

CategoryTheory.LocallySmall

A category is w-locally small if every hom set is w-small. See ShrinkHoms C for a category instance where every hom set has been replaced by a small model.

Defined in
Mathlib.CategoryTheory.EssentiallySmall
Shape
One type argument · adds hom_small
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by3

Forgetful instances

Provided automatically by

Concrete types that are instances17

  • CategoryTheory.Functor
  • CategoryTheory.Over
  • HomologicalComplex
  • CategoryTheory.ObjectProperty.FullSubcategory
  • CategoryTheory.Quotient
  • CategoryTheory.Comma
  • CategoryTheory.Under
  • CategoryTheory.CostructuredArrow
  • CategoryTheory.StructuredArrow
  • CategoryTheory.Functor.Elements
  • CategoryTheory.Limits.ColimitPresentation.Total
  • HomotopicalAlgebra.BifibrantObject.HoCat
  • CategoryTheory.Limits.WalkingMultispan
  • CategoryTheory.CountableCategory.ObjAsType
  • CategoryTheory.SmallModel
  • Opposite
  • Shrink

How is a type an instance?

Loading the hierarchy index…

Assumed by423

Ancestors0

No ancestors.