Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman <shulman@sandiego.edu>]

[-- Attachment #1: Type: text/plain, Size: 1550 bytes --]

On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling <jon@jonmsterling.com> 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.

[-- Attachment #2: Type: text/html, Size: 2268 bytes --]