Typal Heterogeneous Equality Types
Andrew Pitts
Mar 17, 2020
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...