Parametricity via cohesion

DOI10.46298/ENTICS.14710MaRDI QIDQ6831458zbMATH OpenFDO

Authors C. B. Aberlé

Publication date 2 April 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/ENTICS.14710

zbMATH Keywords

Agdacategory theorycohesionconstructive mathematicshomotopy type theoryparametricitytype theory

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites work

• Axiomatic cohesion
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• scientific article; zbMATH DE number 1722653 (Why is no real title available?)
• scientific article; zbMATH DE number 2172007 (Why is no real title available?)
• Impredicative encodings of (higher) inductive types
• Internal Parametricity for Cubical Type Theory
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Relational parametricity for higher kinds
• Syntax and models of Cartesian cubical type theory

This page was built for publication: Parametricity via cohesion

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