Commit 2026-06-02 08:57 be227a36

fix(CategoryTheory/Adjunction): make the left and right triangle identities type-correct (#40139) The current lemmas CategoryTheory.Adjunction.left_triangle and CategoryTheory.Adjunction.right_triangle abuse strict associativity and unitality of functor compositions and are missing associators and unitors. Their expressions are changed to be correct and proofs relying on this are reworked. This came up in #39867.