Functorially embedding Cat into the category of small categories

There is a canonical functor asSmallFunctor between the category of categories of any size and any larger category of small categories.

Future Work

Show that asSmallFunctor is faithful.

def CategoryTheory.Cat.asSmallFunctor : Functor Cat Cat

Assigning to each category C the small category AsSmall C induces a functor Cat ⥤ Cat.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Cat.asSmallFunctor_map {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) : asSmallFunctor.map F = AsSmall.down.comp (Functor.comp F AsSmall.up)

@[simp]

theorem CategoryTheory.Cat.asSmallFunctor_obj (C : Cat) : asSmallFunctor.obj C = of (AsSmall ↑C)