Use modules for reflective subuniverses and modalities

This is option (4) at #596.  It's still a bit annoying, but I think it's made manageable by the technique of making the module types represent a _family_ of subuniverses or modalities.  The universe polymorphism is fiddly when defining particular examples, but once they are defined, it's basically invisible, which is how it should be.  Note that hardly any of the substantial code has to be modified; most of the changes are in the boilerplate.  There are a couple of minor anomalies that have to be worked around (still working on bug reports), but nothing too major.  Right now I think this is probably the way to go -- I don't even know how to do option (3) for lex modalities -- but I'd be interested in what others think.  I'm also very open to feedback on the best way to name and manage the modules; I proposed one possible convention, but I don't know that it's the best.
I have some sympathy for using `Check` for automatic testing. Perhaps, we
should leave it as it is.

On Tue, Nov 18, 2014 at 2:06 PM, Mike Shulman <notifications@github.com>
wrote:

> In theories/Modality.v:
>
> > @@ -34,124 +179,165 @@ However, our definition is more convenient in formalized applications because in
> >
> >  On the other hand, in other examples (such as [~~] and open modalities) it is easier to construct the latter weaker induction principle.  Thus, we now show how to get from that to our definition of modality. *)
> >
> > -Section EasyModality.
> > +Module Type EasyModalities.
> > +
> > +  Parameter Modality : Type2@{u a}.
> > +  Check Modality@{u a}.
> > +
> > +  Parameter O_reflector : forall (O : Modality@{u a}),
> > +                            Type2le@{i a} -> Type2le@{i a}.
> > +  Check O_reflector@{u a i}.
>
> Is there another way to document the number of universe parameters and
> have Coq verify that it's correct?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/614/files#r20503468>.
>