Theorems · Theorem · category theory

CategoryTheory.locallySmall_of_faithful

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) [F.Faithful] [CategoryTheory.LocallySmall.{w, v', u'} D],
  CategoryTheory.LocallySmall.{w, v, u} C

Defined in

Mathlib.CategoryTheory.EssentiallySmall

Cited by

5 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.FaithfulCategoryTheory.LocallySmall