Typal Heterogeneous Equality Types
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Pitts, Andrew https://orcid.org/0000-0001-7775-3471
Abstract
The usual homogeneous form of equality type in Martin-L"of Type Theory contains identifications between elements of the same type. By contrast, the heterogeneous form of equality contains identifications between elements of possibly different types. This paper introduces a simple set of axioms for such types. The axioms are equivalent to the combination of systematic elimination rules for both forms of equality, albeit with typal (also known as "propositional") computation properties, together with Streicher's Axiom K, or equivalently, the principle of uniqueness of identity proofs.
Description
Keywords
type theory, equality types, heterogeneous equality
Journal Title
ACM Transactions on Computational Logic
Conference Name
Journal ISSN
1529-3785
1557-945X
1557-945X
Volume Title
21
Publisher
ACM
Publisher DOI
Rights
All rights reserved