Evan Cavallo ; Robert Harper - Internal Parametricity for Cubical Type Theory

lmcs:6503 - Logical Methods in Computer Science, November 3, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:5)2021
Internal Parametricity for Cubical Type TheoryArticle

Authors: Evan Cavallo ORCID; Robert Harper

    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.


    Volume: Volume 17, Issue 4
    Published on: November 3, 2021
    Accepted on: May 7, 2021
    Submitted on: May 25, 2020
    Keywords: Computer Science - Logic in Computer Science,F.3.2,D.3.1

    1 Document citing this article

    Consultation statistics

    This page has been seen 1327 times.
    This article's PDF has been downloaded 536 times.