Comment on Velma can't math.

Gobbel2000@programming.dev ⁨19⁩ ⁨hours⁩ ago

• Crazazy@feddit.nl ⁨19⁩ ⁨hours⁩ ago

  quotient equivalence under an equivalence class “a” en.wikipedia.org/wiki/Quotient_type

  source

  • Gobbel2000@programming.dev ⁨10⁩ ⁨hours⁩ 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 ⁨9⁩ ⁨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

      source

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

        source