Okay, but even if we assumed (x=b) to be a very small equivalence relation, it should appear in the denominator position to form an equivalence quotient.
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
Wrong formula aside, what is the meaning of dividing an entire equation? (x = b) / a
quotient equivalence under an equivalence relation “a” https://en.wikipedia.org/wiki/Quotient_type
Okay, but even if we assumed (x=b) to be a very small equivalence relation, it should appear in the denominator position to form an equivalence quotient.
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
You’re probably on the right track. Every hunk of symbols is probably a valid type expression in some system. Including a square root type.