Hi
Mike, thanks for your comments — regarding modal type theory, please
note that there are state of the art general modal type theories that do
not employ admissible substitution! MTT is one of them.
Split-context
modal type theories can also be presented without admissible
substitutions. Making substitutions explicit is easy; it's making them
admissible that's hard. And as far as I understand it, MTT does satisfy
the primary desideratum when making substitutions admissible, namely
that all rules have a fully general context in their conclusion.
MTT
is also not equivalent to split-context theories, and IMHO is less
pleasant to work with in practice. I believe there should be some way
to combine the ideas of the two theories.
By
the way, in the followup paper "Modalities and parametric adjoints" by
Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also
authors of the MTT paper) we read "The admissibility of substitution is a
central property of type theory, and indeed of all logic" (section IB).