Feature request: modalities

[anshwad10]

Add sharp and flat modalities (like in Agda flat). In the future we could support any modal type theory, but for now I think spatial type theory will be useful in most cases (e.g. formalizing https://arxiv.org/abs/1509.07584 or https://arxiv.org/abs/2205.15887)