Zulip Chat Archive

Stream: general

Topic: Quotient inductive types?

Jonathan Osser (Jan 18 2021 at 14:01):

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 (Jan 18 2021 at 14:34):

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)

Last updated: Aug 03 2023 at 10:10 UTC