  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.
