In the type theory literature, there are different kinds of types which are called heterogeneous equality types:
heterogeneous identity types are a variant of identity types but parameterized over pairs of possibly different types,
John Major equality types are the dependent sum of heterogeneous identity types over all relevant identifications.
Last revised on September 17, 2023 at 05:29:44. See the history of this page for a list of all contributions to it.