Comment by SabrinaJewson

It’s less nice from a computational perspective. But almost no mathematicians care about computation – they care about semantics, and there is no sense in which Lean’s quotients are a hack from a semantic perspective. I’m sure it makes computer scientists unhappy, but this isn’t a project for computer scientists.