Commit 2024-08-06 08:06 cea57e0d
View on Github →feat(CategoryTheory/Adjunction): typeToCat
is left adjoint to Cat.objects
(#15375)
The embedding of Type
into Cat
, which views a set as a discrete category, is left adjoint to the functor Cat.objects : Cat -> Set
mapping a category to its set of objects