Typal Heterogeneous Equality Types

The usual homogeneous form of equality type in Martin-Lof 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 Streichers Axiom K, or equivalently, the principle of uniqueness of identity proofs.