# 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

`typeToCat : Type ⥤ Cat`

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

## Equations

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

## Instances For

The connected components functor

## Equations

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

## Instances For

`typeToCat : Type ⥤ Cat`

is right adjoint to `connectedComponents : Cat ⥤ Type`

## Equations

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