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.
Thanks, that was also left over from my not knowing about Local Instance.

On Mon, Sep 8, 2014 at 11:45 AM, Jason Gross <notifications@github.com>
wrote:

> In theories/ReflectiveSubuniverse.v:
>
> >
> > -    (** The second component of [subuniverse_Type] is unique *)
> > -    Definition path_SubuniverseType
> > -    : forall (T T' : SubuniverseType subU), T.1 = T'.1 -> T = T'.
> > -    Proof.
> > -      intros [T h] [T' h'] X.
> > -      apply (path_sigma _ _ _ X).
> > -      apply allpath_hprop.
> > -    Defined.
> > +  4. Inside a section (only!), specify that we will be applying the general theory of subuniverses only to a specific example, by declaring that example as an [Instance].  As long as you *don't* say [Global Instance], the instance won't outlast the section, but inside the section you won't have to give it as an explicit argument.
>
> This seems slightly inaccurate, given that we have Local Instance; it's
> not so much "Inside the section" that matters as "make the instance local",
> whether that means using Local (Existing) Instance at top-level, or (Local)
> (Existing) Instance inside a section.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/470/files#r17258119>.
>