Better Universe Minimization ToSet Heuristics

[JasonGross]

I think it might be useful to have a setting that turns off minimization to Set during proof mode, and applies minimization only to irrelevant and covariant universes in top-level definitions.

---

I do think it's an interesting case study that might suggest a better heuristic for minimization to Set (cc @SkySkimmer @mattam82 ?), namely that if universe cumulativity and variance is extended from inductives to constants, then it always makes sense to minimize irrelevant universes to Set, and when you know a universe is only going to be used covariantly in a top-level definition, then it's okay to minimize to Set. I think this means in proof mode we should only ever minimize universes to Set if the universe is irrelevant for the goal and context, and most minimization to Set should happen at definition closing time? (Maybe an easy intermediate heuristic would be Set Minimization ToSet In Non Proof Mode Only or something?)

Originally posted by @JasonGross in HoTT/Coq-HoTT#1723 (comment)