Adjoint equivalence between (ℚ, _≤_, _≡_) and (ℚᵘ, _≤_, _≃_) via toℚᵘ / fromℚᵘ #2113
Description
This ought to be low-hanging fruit (UPDATED; but I'm not sure that it is, entirely, or at least, it's an amount of work to put it all together, so dropping that label for now), but would streamline 'transfer' arguments about instances of the order relations between the two types, eg in the proof <-dense in Data.Rational.Properties in #2111.