I have a development where I use extensionality and the propositional truncation, some parts of the code use instances of univalence (introduced as assumptions), and some parts use instances of UIP (also introduced as assumptions). I think it would be nice if there was a variant of Cubical Agda that was consistent with UIP. What would this take? I imagine that it does not suffice to have a flag that disables the primitives and builtins related to univalence.