Internal Parametricity for Cubical Type Theory

DOI10.4230/LIPICS.CSL.2020.13MaRDI QIDQ5874199zbMATH OpenOpenAlexFDO

Authors Evan Cavallo, Robert Harper

Publication date 7 February 2023

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2020/11656/pdf/LIPIcs-CSL-2020-13.pdf/

zbMATH Keywords

cubical type theoryhigher inductive typesparametricity

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Internal parametricity for cubical type theory
• Internal type theory
• Canonicity for cubical type theory
• Constructing inductive-inductive types in cubical type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• On higher inductive types in cubical type theory
• On the internal structures of inductive types
• Internalising modified realisability in constructive type theory
• Type theories from Barendregt's cube for theorem provers
• Unifying Cubical Models of Univalent Type Theory

Cited in

(7)

• Parametricity for Haskell with Imprecise Error Semantics
• Internal parametricity for cubical type theory
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Parametricity via cohesion
• A parametricity-based formalization of semi-simplicial and semi-cubical sets
• Symmetric monoidal smash products in homotopy type theory

This page was built for publication: Internal Parametricity for Cubical Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5874199)