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

Estimated changes