Internal Parametricity for Cubical Type Theory

TL;DR

This paper introduces a new computational type theory that integrates cubical type theory with internal parametricity, supporting univalence and relativity, and explores their interactions and models.

Contribution

It combines cubical type theory with internal parametricity primitives, enabling analysis of polymorphic functions and establishing formal models.

Findings

Supports both univalence and relativity in the combined theory.

Analyzes polymorphic functions between higher inductive types.

Provides a presheaf model for the formal interface.

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.