Quotient inductive types?

Stream: general

[Jonathan Osser]

Will lean ever support quotient inductive types and quotient inductive-inductive types? I feel that they may be more ergonomic than quotient types as they are implemented currently.

[Mario Carneiro]

The theory behind these types is quite complex and would increase the trust base / axiomatic strength of lean a lot, so I would prefer to perform constructions of these types where applicable (which can be done in most cases)