Parametric Cubical Type Theory

TL;DR

This paper introduces a new computational type theory that integrates cubical and parametric features, supporting univalence and relativity, and demonstrates its application to polymorphic and inductive types.

Contribution

It presents a novel combined type theory merging cubical and parametric principles, enabling new ways to analyze polymorphic and inductive types.

Findings

Supports both univalence and relativity in the combined theory

Analyzes polymorphic types and functions between higher inductive types

Uses relativity to characterize relational interpretation of inductive types

Abstract

We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and distinctions between the two along the way. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic types, including functions between higher inductive types, and we show by example how relativity can be used to characterize the relational interpretation of inductive types.