Generic logic

This is perhaps not optimally polished, but I'm putting it out here for feedback.  The idea is that a "logic" is essentially a modality, and we can define all the logical operations relative to "a logic", with PAT-logic and (-1)-logic as important special cases.  More description can be found in the comments.  I included LEM as an example of how to use this kind of generic logic; next up would be AC, which is potentially parametrized by 2 or 3 different modalities/logics.

I had to make a bunch of choices about how to implement it, and my only indication that they're the right ones is that nothing else I tried worked as well.  So I'm very open to suggestions, up to and including "this is a terrible idea".

One particular infelicity is that this change slows down the compilation of `V.v` by almost a factor of 3.  I don't have any idea why that might be, but if it's going to consistently do that whenever we make heavy use of `hexists` (which `V.v` is currently the only theory that does), then one might argue that this is not worth it.
Yes, of course, the closed subtopos. The open one is working under a
hypothesis, I believe.

On Thu, Sep 25, 2014 at 7:20 PM, Mike Shulman <notifications@github.com>
wrote:

> In theories/Logic/Generic.v:
>
> > +
> > +Definition truncated_logic (n : trunc_index) : Logic.
> > +Proof.
> > +  refine (Build_Logic (truncation_modality n) _).
> > +  - destruct n.
> > +    + exact (inr tt).
> > +    + apply inl; simpl; exact _.
> > +Defined.
> > +
> > +Coercion truncated_logic : trunc_index >-> Logic.
> > +
> > +Global Notation oo := PAT_logic.
> > +
> > +Definition notnot_logic `{Funext} : Logic
> > +  := Build_Logic notnot_modality (inl _).
> > +
>
> Hmm, according to the wikipedia page it looks like that should be the
> *closed* subtopos?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/524/files#r18045873>.
>