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.