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
.