Commit 2024-05-16 09:19 fafe8ea4
View on Github →feat(CategoryTheory): the adjunction between Over.map and Over.baseChange (#12927) When a category has pullbacks, any morphism gives rise to an adjunction between over categories, with the left adjoint defined by composition and the right adjoint defined by pullback. This PR contains a definition of that adjunction.