Internal Parametricity for Cubical Type Theory
arXiv:2005.11290 · doi:10.46298/lmcs-17(4:5)2021
Abstract
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 also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.
References in corpus (6)
- A dependent nominal type theory
- Axioms for Modelling Cubical Type Theory in a Topos
- Computational Higher Type Theory IV: Inductive Types
- On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
- The law of excluded middle in the simplicial model of type theory
- Parametricity, automorphisms of the universe, and excluded middle