HoTT/HoTT — pull request #507 by mikeshulman (2014-09-16 14:10:19+00:00)
Title: 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! (-: