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

["'Thorsten Altenkirch' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.com>]

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

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.

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