Mathlib Map

Structures · Logic and sets

Small

A type is Small.{w} if there exists an equivalence to some S : Type w.

Defined in
Mathlib.Logic.Small.Defs
Shape
One type argument · adds equiv_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 instances41

  • Quiver.Hom
  • CategoryTheory.Functor
  • TensorProduct
  • Units
  • Finsupp
  • CategoryTheory.Discrete
  • DFinsupp
  • CategoryTheory.ObjectProperty.FullSubcategory
  • CategoryTheory.Skeleton
  • MonCat.carrier
  • MvPolynomial
  • CategoryTheory.CostructuredArrow
  • CategoryTheory.StructuredArrow
  • CategoryTheory.Arrow
  • List.Vector
  • GrpCat.carrier
  • AddCommGrpCat.Colimits.Quot
  • CategoryTheory.Subobject
  • CategoryTheory.Limits.MultispanShape.L
  • FirstOrder.Language.Term
  • CategoryTheory.Limits.WalkingMultispan
  • CategoryTheory.Functor.ColimitType
  • CategoryTheory.SmallObject.FunctorObjIndex
  • FirstOrder.Language.Theory.ModelType.Carrier
  • CategoryTheory.OrthogonalReflection.D₂
  • HomotopicalAlgebra.AttachCells.ι
  • CategoryTheory.OrthogonalReflection.D₁
  • Subtype
  • Prod
  • OrderDual
  • Set.Elem
  • ULift
  • HasQuotient.Quotient
  • Opposite
  • Sum
  • List
  • Sigma
  • Set
  • Quotient
  • PLift
  • Quot

How is a type an instance?

Loading the hierarchy index…

Assumed by711

Ancestors0

No ancestors.