Commit 2024-12-14 10:55 d19d8405
View on Github →feat(CategoryTheory/Monoidal): composition of monoidal category adjunctions (#17956)
If C and D are monoidal categories, F : C ⥤ D and G : D ⥤ E are monoidal functors, an adjunction F ⊣ G is monoidal if some additional compatibilities are satisfied. We show in this PR that the property that these compatibilities hold is stable by composition of adjunctions.