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

[Michael Shulman <shulman@sandiego.edu>]

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

Substitution and weakening hold for all types with the restriction that
only crisp terms (i.e. those involving only crisp variables) can be
substituted for crisp variables.  This restriction is mentioned in the
beginning of section 2.

On Fri, Nov 11, 2022 at 3:14 PM Madeleine Birchfield <
madeleinebirchfield@gmail.com> wrote:

> In Mike Shulman's presentation of cohesive homotopy type theory in his
> 2018 article Brouwer’s fixed-point theorem in real-cohesive homotopy type
> theory, he states in section 2 that "All the ordinary rules of type
> theory (∏-types, ∑-types, =-types, W -types, HITs) are imported into our
> theory only in the world of cohesive variables." Does this also include
> the structural rules of type theory such as the substitution and weakening
> rules?
>
> Madeleine Birchfield
>
> --
> 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/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googlegroups.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>

-- 
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/CADYavpymP9gVGU8oy-m-NKtS_8f7fgR5WRBoMaY3NUSRfPejFQ%40mail.gmail.com.

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