Uniformize reflective subuniverses and modalities

And also add a few more examples.  This closes #457.  The use of typeclasses is a bit hackish (see comments in `ReflectiveSubuniverse.v`), but it's the best way I've been able to think of to avoid having to pass the modality as an argument to everything all the time when there is only one modality hanging around.
What is statement of the generalization to modalities?

On Mon, Sep 8, 2014 at 10:16 AM, Bas Spitters <notifications@github.com>
wrote:

> In Makefile_targets.mk:
>
> >  	$(srcdir)/theories/hit/V.v \
> > -	$(srcdir)/theories/types/ObjectClassifier.v \
>
> Perhaps related, I just finished a proof of the existence of the subobject
> classifier.
> This naturally extends to modalities. I could try to prove it formally in
> that generality and put it in a file depending on both Objectclassifier and
> modalities. However, I could also prove a simpler statement with less
> dependencies.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/470/files#r17251955>.
>