文章基本信息

标题：Internal Parametricity for Cubical Type Theory
本地全文：下载
作者：Evan Cavallo ; Robert Harper
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：152
页码：1-17
DOI：10.4230/LIPIcs.CSL.2020.13
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：parametricity; cubical type theory; higher inductive types