arithmetic operations of Cubical.Data.Rationals is super slow about cubical HOT 1 OPEN

This might be due to overeager normalization of arithmetic in Agda? The standard library has a fix with some record prefixes and no-eta-equality, but this isn't the case for Cubical.

Also Cubical's rationals-as-a-set-quotient representation has arithmetic defined in a way that has some undesired usage of recursors that make computation clunky. The details are abstracted to try and reduce the problem, but it's still there until the implementation is updated to avoid calling the recursor entirely. Better to pattern-match so that the associativity proof doesn't get dragged around with every computational step, abstracted or otherwise.

from cubical.