From: Jon Sterling <jon@jonmsterling.com>
To: Michael Shulman <shulman@sandiego.edu>
Cc: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>,
"andrej.bauer" <andrej.bauer@andrej.com>,
Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory
Date: Fri, 18 Nov 2022 11:22:56 -0500 [thread overview]
Message-ID: <4D4B5058-E159-4139-8713-979EC5E1D3BA@jonmsterling.com> (raw)
In-Reply-To: <CADYavpwz_Y61ST5eauZiH1b9E79BF--oroXinvzd2odHsycyjg@mail.gmail.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 --]
next prev parent reply other threads:[~2022-11-18 16:23 UTC|newest]
Thread overview: 24+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-11-11 22:53 Madeleine Birchfield
2022-11-11 23:47 ` Michael Shulman
2022-11-15 22:38 ` andrej.bauer
2022-11-16 9:52 ` 'Thorsten Altenkirch' via Homotopy Type Theory
2022-11-17 13:36 ` Jon Sterling
2022-11-18 2:35 ` Michael Shulman
2022-11-18 6:19 ` Tom Hirschowitz
2022-11-18 10:58 ` Jon Sterling
2022-11-18 16:16 ` Michael Shulman
2022-11-18 16:22 ` Jon Sterling [this message]
2022-11-18 11:35 ` 'Thorsten Altenkirch' via Homotopy Type Theory
2022-11-18 12:47 ` Jon Sterling
2022-11-18 13:05 ` Jon Sterling
2022-11-18 16:25 ` Michael Shulman
2022-11-18 16:38 ` Jon Sterling
2022-11-18 16:56 ` Michael Shulman
2022-11-18 16:59 ` Jon Sterling
2022-11-18 17:14 ` Michael Shulman
2022-12-01 14:40 ` Andreas Nuyts
2022-12-01 15:54 ` Jon Sterling
2022-12-01 15:57 ` Andreas Nuyts
2022-12-01 16:09 ` Andreas Nuyts
2022-12-01 18:00 ` Michael Shulman
2022-11-18 14:21 ` andrej.bauer
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=4D4B5058-E159-4139-8713-979EC5E1D3BA@jonmsterling.com \
--to=jon@jonmsterling.com \
--cc=HomotopyTypeTheory@googlegroups.com \
--cc=Thorsten.Altenkirch@nottingham.ac.uk \
--cc=andrej.bauer@andrej.com \
--cc=shulman@sandiego.edu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).