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