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.
@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.13, author = {Cavallo, Evan and Harper, Robert}, title = {{Internal Parametricity for Cubical Type Theory}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {13:1--13:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.13}, URN = {urn:nbn:de:0030-drops-116564}, doi = {10.4230/LIPIcs.CSL.2020.13}, annote = {Keywords: parametricity, cubical type theory, higher inductive types} }
Feedback for Dagstuhl Publishing