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 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