  We prove normalization for MTT, a general multimodal dependent type theory
capable of expressing modal type theories for guarded recursion, internalized
parametricity, and various other prototypical modal situations. We prove that
deciding type checking and conversion in MTT can be reduced to deciding the
equality of modalities in the underlying modal situation, immediately yielding
a type checking algorithm for all instantiations of MTT in the literature.
  This proof uses a generalization of synthetic Tait computability -- an
abstract approach to gluing proofs -- to account for modalities. This extension
is based on MTT itself, so that this proof also constitutes a significant case
study of MTT.
