典型的异构相等类型
Typal Heterogeneous Equality Types
摘要：
在马丁-洛夫类型论中，相等类型的通常齐次形式包含了相同类型的元素之间的同一性。相比之下，异质形式的相等包含可能不同类型的元素之间的标识。本文介绍了一组简单的公理，这样的类型。这些公理等价于两种形式的等式的系统消去规则的组合，尽管具有典型的（也称为“命题”）计算性质，以及Streicher公理K，或者等价地，恒等式证明的唯一性原则。
英文摘要：
The usual homogeneous form of equality type in Martin-Löf 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
