On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling wrote: > 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). -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpwz_Y61ST5eauZiH1b9E79BF--oroXinvzd2odHsycyjg%40mail.gmail.com.