Commit 2025-01-01 14:50 9419c034

View on Github →

chore(CategoryTheory/Adjunction/Opposites): redefine the opposite of an adjunction (#20375) Change the definition of Adjunction.adjointOfOpAdjointOp and Adjunction.opAdjointOpOfAdjoint to be more in line with the new definition of adjunctions from #16317 (which removes the homEquiv field), and rename these to Adjunction.op and Adjunction.unop to be consistent with Equivalence.op and Equivalence.unop. The 6 other variants of opposite adjunctions are all defined from Adjunction.op or Adjunction.unop and should not be needed anymore, they have been marked as deprecated, as well as Adjunction.adjointOfOpAdjointOp and Adjunction.opAdjointOpOfAdjoint.

Estimated changes