eliminate funext (mostly) from reflective subuniverses

One more redesign of reflective subuniverses: rather than assume that precomposition with units is an equivalence, we give two eliminators and their computation rules: one non-dependent recursion principle and one induction principle that only eliminates into path types of a certain form.  Together these four rules are essentially equivalent to the original definition, but they can be formulated in an entirely "pointwise" manner that avoids the need for funext in most places (while the equivalence with the original definition requires funext in _both_ directions).  As described in the comments, the advantages of this are:

1. It avoids funext redexes, thereby simplifying the proofs and proof terms.

2. It avoids [Funext] hypotheses in some constructions of reflective subuniverses, particularly the construction from a [Modality].  This enables us to declare such constructions as coercions without running afoul of Coq's "uniform inheritance condition", so that a modality can be used directly as a reflective subuniverse.

3. The data of a reflective subuniverse according to the new definition is precisely a couple of special cases of the data of a modality.  Thus, all theorems about reflective subuniverses will, when interpreted for a modality, reduce definitionally to "the way we would have proved them directly for a modality".

Of course, funext is still needed for a few results, such as closure of a reflective subuniverse under Pi-types.  It's also used in the proof that the reflector preserves products; I don't currently know whether to expect that it is necessary there.  Comments on that or anything else are welcome.  I hope that this will be the last basic redesign for a while, at least!  (-:

We all have days like that.  (-:

Awesome!  It'll probably be a little while before I manage to have a look; maybe we could get this PR merged for now and then whichever of us gets around first to making a new PR for your improvement can do it.

I had the thought while proving all the functoriality lemmas that there's probably a fairly simple tactic that could do them all, since they all follow the same pattern: apply `O_rectpaths`, unfold everything, then use `O_rectnd_beta`.