2026-07-22T09:08:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11656 2024-03-06T10:48:42Z ddc:004 open_access

Internal Parametricity for Cubical Type Theory Cavallo, Evan Harper, Robert parametricity cubical type theory higher inductive types 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, and we give an account of the identity extension lemma for internal parametricity. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Evan Cavallo and Robert Harper 2020 Is Part Of LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2020.13 urn:nbn:de:0030-drops-116564 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.13 eng https://creativecommons.org/licenses/by/3.0/legalcode