definition of quotients

Stream: new members

[Mike Shulman]

With propext, funext, and proof-irrelevance, it should be possible to define the quotient of an equivalence relation to be its set of equivalence classes. Why does Lean take quotients to be primitive instead?

[Mario Carneiro]

because this gives a definitional equality for lift f (mk a) = f a

[Mario Carneiro]

also, funext isn't an axiom, it is proved... using quotients

[Mike Shulman]

Mario Carneiro said:

also, funext isn't an axiom, it is proved... using quotients

But since quotients are an axiom, that doesn't seem like a reason to do it one way or the other. This way, quotients are an axiom and you prove funext, but the other way, funext would be an axiom and you prove quotients. I don't see why one axiom is better than the other.

[Mike Shulman]

Mario Carneiro said:

because this gives a definitional equality for lift f (mk a) = f a

This is a surprising reason to hear, given that Lean generally seems to deprecate definitional equality. Are there places where the definitional nature of this equality is really used importantly?

[Junyan Xu]

Are there places where the definitional nature of this equality is really used importantly?

For example, docs#multiset is a quotient of docs#list, and with the computation rule lift f (mk x) = f x, h : multiset.mem a {1,2,3} reduces to h : a = 1 ∨ a = 2 ∨ a = 3 ∨ false, so you can do rcases h with (rfl|rfl|rfl|⟨⟨⟩⟩) which can be quite convenient.

[Reid Barton]

There are limits to de-emphasizing definitional equality. For example, we for sure want fst (x, y) to be definitionally equal to x.

[Reid Barton]

It's more for things like real and polynomial (where there is no unique obvious representation anyways) that we don't care so much about definitional equalities. And a lot of mathlib is about things like real and polynomial.
quot, like prod, is a quite basic thing where it's obvious what definitional equalities you would like; so we might as well have them.