Typal heterogeneous equality types

DOI10.1145/3379447MaRDI QIDQ5121276zbMATH OpenOpenAlexFDO

Authors Andrew M. Pitts

Publication date 11 September 2020

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1907.07501

zbMATH Keywords

type theoryequality typesheterogeneous equality

Mathematics Subject Classification ID

Type theory (03B38)

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.

Recommendations

• A coherence theorem for Martin-Löf's type theory
• scientific article; zbMATH DE number 1302059
• Theory of dependent types and axiom of univalence
• Homotopy theoretic models of identity types
• On the strength of dependent products in the type theory of Martin-Löf

This page was built for publication: Typal heterogeneous equality types

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