Modalities

[lkstl]

I started another implementation of modal operators and modalities, more closely modelend on the canonical resource for modalities in HoTT:

https://arxiv.org/abs/1706.07526

Maybe this should be unified with the existing implementations of modalities in the future.

[felixwellen]

Nice! Please go on ;-) I think the old modalities code should be replaced as soon as this one covers the same functionality (and no problems with the Typeω come up) - it was always an ad hoc thing...