Oh yeah was a bit sleepy and thought you could just put arbitrary expressions in the numerator instead of just the type.

But consider this: heterogeneous propositional equality type of types x and b under equivalence relation a, which is bound somewhere else in the aether that we can't see in the screenshot

Constructors of this equality type? No fucking clue but I'm sure there exist some to make the need for an equivalence relation make sense