Theorems · Inductive type · category theory

CategoryTheory.LocallySmall

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop

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

Cited by

242 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category