mathlib

83bce9f1 - feat(category_theory/adjunction/whiskering): Whiskering adjunctions. (#10495)

feat(category_theory/adjunction/whiskering): Whiskering adjunctions. (#10495) Construct adjunctions between functor categories induced by whiskering (both left and right). This will be used later to construct adjunctions between categories of sheaves.