Commit 2026-05-04 11:17 3858cf58

feat(Translate): reorder universes (#36604) This PR improves the heuristic for reordering of universes in to_dual/to_additive. The previous heuristic worked well when the first two universes had to be swapped. For example for translating a ^ n to n • a, and for dualizing GaloisConnection. However, in Category theory we sometimes need to swap more universes because a category instance comes with 2 universes which both need to be swapped. In particular, the comma category, and adjunctions both need this feature. This PR doesn't add any syntax for specifying the reordering of universes. It is assumed that the universe reordering can always be inferred from the normal reordering and from the type.