Commit 2026-06-08 19:59 032bf56b
View on Github →feat: to_dual for Adjunction (#39867)
This PR uses the new capability of to_dual to deal with universe reorderings to tag Adjunction.
Adjunction.ext_counit is added as the dual of Adjunction.ext.
Note: there is a bug in the implementation that stops me from being able to tag Adjunction.comp. I'll fix that in a future PR.