Typal Heterogeneous Equality Types

TL;DR

This paper introduces a set of axioms for heterogeneous equality types in Martin-Löf Type Theory, enabling identifications between elements of different types, and explores their logical properties and equivalences.

Contribution

It formalizes axioms for heterogeneous equality types and demonstrates their equivalence to elimination rules combined with Streicher's Axiom K.

Findings

Axioms for heterogeneous equality types are consistent and well-defined.

Heterogeneous equality axioms are equivalent to elimination rules plus Streicher's Axiom K.

The approach clarifies the logical structure of heterogeneous equality in type theory.

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.