Leibniz equality is isomorphic to Martin-Löf identity, parametrically

DOI10.1017/S0956796820000155MaRDI QIDQ5120232zbMATH OpenOpenAlexWikidataFDO

Authors Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler

Publication date 9 September 2020

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796820000155

Mathematics Subject Classification ID

Type theory (03B38) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On the conservativity of Leibniz equality
• The Marriage of Univalence and Parametricity
• Parametricity as isomorphism
• Parametricity, type equality, and higher-order polymorphism
• A coherence theorem for Martin-Löf's type theory

Cites work

• A presheaf model of parametric type theory
• A relationally parametric model of dependent type theory
• Categorical data types in parametric polymorphism
• Cubical type theory: a constructive interpretation of the univalence axiom
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• Parametricity and dependent types
• Pattern matching without K
• Proofs for free. Parametricity for dependent types
• The Girard-Reynolds isomorphism (second edition)
• Unifiers as equivalences: proof-relevant unification of dependently typed data

Cited in

(2)

• The Marriage of Univalence and Parametricity
• On the conservativity of Leibniz equality

Describes a project that uses

Uses Software

• Agda
• cubicaltt

This page was built for publication: Leibniz equality is isomorphic to Martin-Löf identity, parametrically

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