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

[Jon Sterling <jon@jonmsterling.com>]

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

Indeed, I echo Thorsten's comment — to put it another way, even being 
able to tell whether these rules are derivable or only admissible is 
like knowing what an angel's favorite TV show is (in other words, a form 
of knowledge that cannot be applied toward anything by human beings). At 
least for structural type theory, there is nothing worth saying that 
cannot be phrased in a way that does not depend on whether structural 
rules are admissible or derivable. It may be that admissiblity of 
structural rules starts to play a role in substructural type theory, 
however, but this is not my area of expertise.

It is revealing that nobody has proposed a notion of **model** of type 
theory in which the admissible structural rules do not hold; this would 
be the necessary form taken by any evidence for the thesis that it is 
important for structural rules to not be derivable. Absent such a notion 
of model and evidence that it is at all compelling/useful, we would have 
to conclude that worrying about admissibility vs. derivability of 
structural rules in the official presentation of type theory is 
fundementally misguided.


On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory 
wrote:

> That depends on what presentation of Type Theory you are using. Your 
> remarks apply to the extrinsic approach from the last millennium. More 
> recent presentation of Type Theory built in substitution and weakening 
> and use an intrinsic approach which avoids talking about preterms you 
> don’t really care about.
>
> https://dl.acm.org/doi/10.1145/2837614.2837638
>
> Cheers,
> Thorsten
>
> From: homotopytypetheory@googlegroups.com 
> <homotopytypetheory@googlegroups.com> on behalf of 
> andrej.bauer@andrej.com <andrej.bauer@andrej.com>
> Date: Tuesday, 15 November 2022 at 22:39
> To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
> Subject: Re: [HoTT] Question about the formal rules of cohesive 
> homotopy type theory
>>  Does this also include the structural rules of type theory such as 
>> the substitution and weakening rules?
>
> I would just like to point out that substutition and weakening 
> typically are not part of the rules. They are shown to be admissible. 
> In this spirit, the question should have been: what is the precise 
> version of substitution and weakening (which is a special case of 
> substitution) that is admissible in cohesive type theory?
>
> With kind regards,
>
> Andrej
>
> --
> 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/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> -- 
> 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/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com.

-- 
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/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com.

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