Adjunctions related to Cat, the category of categories

The embedding typeToCat: Type ⥤ Cat, mapping a type to the corresponding discrete category, is left adjoint to the functor Cat.objects, which maps a category to its set of objects.

Another functor connectedComponents : Cat ⥤ Type maps a category to the set of its connected components and functors to functions between those sets.

Notes

All this could be made with 2-functors

def CategoryTheory.Cat.typeToCatObjectsAdj : typeToCat ⊣ objects

typeToCat : Type ⥤ Cat is left adjoint to Cat.objects : Cat ⥤ Type

def CategoryTheory.Cat.connectedComponents : Functor Cat (Type u)

The connected components functor

def CategoryTheory.Cat.connectedComponentsTypeToCatAdj : connectedComponents ⊣ typeToCat

typeToCat : Type ⥤ Cat is right adjoint to connectedComponents : Cat ⥤ Type