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.