Evan Cavallo: Internal parametricity and cubical type theory
Tid: On 2021-03-10 kl 13.30 - 15.30
Föreläsare: Evan Cavallo
Reynolds' parametricity gives a model of type theory that interprets types as relations. This means in particular that all polymorphic (i.e., type-indexed) terms have an action on relations, a fact that can be exploited to "automatically" obtain useful naturality properties. More recently, Bernardy and Moulin have developed a type theory that internalizes its own relational model, making the consequences of parametricity accessible within the theory. I will introduce this type theory and discuss its relationship to cubical type theory; the two have similar structures but differ in key aspects. I will then present a combined parametric cubical type theory, which I have developed in joint work with Robert Harper. We will see how parametricity can be applied to problems in higher-dimensional type theory and how cubical equality can clarify the structure of internally parametric type theory.