Normalization for multimodal type theory

Daniel Gratzer

We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various…