Comment on Velma can't math.

• Gobbel2000@programming.dev ⁨2⁩ ⁨weeks⁩ ago

  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.

  source

  • Crazazy@feddit.nl ⁨2⁩ ⁨weeks⁩ 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

    source

    • Gobbel2000@programming.dev ⁨2⁩ ⁨weeks⁩ 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.

      source