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 : CategoryTheory.typeToCat ⊣ CategoryTheory.Cat.objects

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

Equations

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

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

The connected components functor

Equations

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

def CategoryTheory.Cat.connectedComponentsTypeToCatAdj : CategoryTheory.Cat.connectedComponents ⊣ CategoryTheory.typeToCat

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

Equations

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