Let the user define an Open Modality

[jonsterling]

I had a nice idea for a cool use of the cofibration machinery. If the user can declare a fresh cofibration, then this is basically enough to define a strict "open modality". Then we could potentially use cooltt to mechanize some neat artin gluing arguments.

[jonsterling]

So, in order for this to be useful for my purposes, i also need to extend cooltt with a type of "definitional isomorphisms". I have to think a bit about whether or not this breaks normalization / conversion.