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.
In fact, should both interpretations work? Using all modal types or using
only the hProps.
There should be some general results about combining modalities, in this
case, the closed subtopos-modality and the truncation-modality.

On Thu, Sep 25, 2014 at 7:16 PM, Bas Spitters <b.a.w.spitters@gmail.com>
wrote:

> http://en.wikipedia.org/wiki/Friedman_translation
>
> My guess is that the propositions are only the hprops. The A-translation
> is usually done for FOL, not for DTT.
> However, I should reread papers like Hugo's:
> http://pauillac.inria.fr/~herbelin/articles/lics-Her10-markov.pdf
>
> On Thu, Sep 25, 2014 at 7:10 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 _).
>> > +
>>
>> ("A-translation" is very hard to google for...)
>>
>> —
>> Reply to this email directly or view it on GitHub
>> <https://github.com/HoTT/HoTT/pull/524/files#r18045177>.
>>
>
>