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.