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

[Jon Sterling <jon@jonmsterling.com>]

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

On 18 Nov 2022, at 11:16, Michael Shulman wrote:

> 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).


The real reason it is central is that making substitution admissible 
forces you to figure out the equational theory of substitutions (as I 
said), not the other way around. You are free to consult the other 
authors of that paper, and I guarantee to you that they will confirm my 
analysis. Admissibility seems to have been cargo-culted, as people 
forgot the reason why it was important in the first place.

It is important to recall that the first admissible rule was *cut* in 
Gentzen's analysis of sequent calculus, but Gentzen's cut-free sequent 
calculus is eliminating not only substitution but also all computational 
redexes simultaneously (this is due to the way that sequent calculus is 
arranged). This kind of admissibility is much more useful than mere 
admissibility of substitution, because it gives a normal-forms 
presentation, which (unlike mere admissible substitution) actually has a 
ton of practical applications (not just deciding equivalence, but also 
proof search, etc.).  So I would characterize my viewpoint as an 
essentially orthodox one, though the language we use to say these things 
in 2022 is very different from what was available in the 1930s.

-- 
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/4D4B5058-E159-4139-8713-979EC5E1D3BA%40jonmsterling.com.

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