Commit 2026-07-02 11:53 c19037a8

fix(Translate): fix universe reorder inference (#40493) This PR fixes the way to_dual determines the universe reordering. Previously, the universe reordering was inferred using a heuristic. But, this heuristic fails on Adjunction.comp, because there we are reordering two arguments whose types themselves reorder their universes. This PR removes the heuristic, and instead uses unification to figure out the universe reordering (in the case of to_dual self/to_dual existing. When generating a new declaration, universes are now never reordered. I verified locally that Adjunction.comp can now be tagged with to_dual.