Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Typal Heterogeneous Equality Types
Typal Heterogeneous Equality Types
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.