Comment on Velma can't math.
Gobbel2000@programming.dev 15 hours agoOkay, 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.
Comment on Velma can't math.
Gobbel2000@programming.dev 15 hours agoOkay, 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.
Crazazy@feddit.nl 15 hours ago
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
Gobbel2000@programming.dev 13 hours ago
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.