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

DOI10.1017/S0956796820000155zbMath1479.03010OpenAlexW3036161949WikidataQ123188673 ScholiaQ123188673MaRDI QIDQ5120232

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

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

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

Uses Software

• Agda
• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• The Girard-Reynolds isomorphism (second edition)
• Pattern matching without K
• Proofs for free
• Unifiers as equivalences: proof-relevant unification of dependently typed data
• Categorical data types in parametric polymorphism
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Parametricity and dependent types
• A relationally parametric model of dependent type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• A presheaf model of parametric type theory