Internal Parametricity for Cubical Type Theory

05/22/2020
by   Evan Cavallo, et al.
0

We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We abstract a formal interface to the computational interpretation and show that this also has a presheaf model, and we explore cohesive type theory as a means of connecting parametric and non-parametric theories.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset