Commit 2024-08-12 22:49 577bed1b

View on Github →

feat(CategoryTheory/Adjunction): typeToCat is right adjoint to connectedComponents functor (#15614) The embedding of Type into Cat, which views a set as a discrete category, is right adjoint to the functor connectedComponents : Cat -> Set which maps a category to its set of connected components.

Estimated changes