844
Velma can't math. (mander.xyz)
submitted 1 year ago by to c/science_memes@mander.xyz
94 comments fedilink hide all child comments
 
you are viewing a single comment's thread
view the rest of the comments
[–] 8 points 1 year ago* (3 children)

quotient equivalence under an equivalence relation "a" https://en.wikipedia.org/wiki/Quotient_type

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 3 child comments
    •
  • [–] 2 points 1 year ago (2 children)

    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.

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 2 child comments
    •
  • [–] 2 points 1 year ago* (1 child)

    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

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 1 child comment
    •