Indexed equality

Stream: Is there code for X?

[Eric Wieser]

Floris van Doorn said:

This lemma talks about equality of types, which is "evil".

If equality of types is evil, then should we replace heq (which implies type equality) with the following, which can be varied to mean some other kind of equality?

universes ui ui' u u'
variables {ι : Sort ui} {A : ι → Sort u}

/-- Indexed equality; `(ai : A i) =ᵢ (aj : A j)` if `i = j` -/
inductive indeq {i : ι} (ai : A i) : Π {j} (aj : A j), Prop
| refl [] : indeq ai

Has something like this been explored before? I explore this a little more in #10712, but I'm not sure if it's more useful than directly working with equalities of sigma types.

[Eric Rodriguez]

I'm curious, is this useful for the original purpose?