quot.lift₂

Stream: Is there code for X?

[Bhavik Mehta]

There's quotient.lift₂ but I can't see a quot version - does this indicate I should be using quotient instead of quot in my definitions?

[Kevin Buzzard]

You should be using quotient' ;-) except that you can't have the notation with that

[Bhavik Mehta]

Where's quotient'?

[Chris Hughes]

I think quot.lift2 isn't even true. I remember thinking about this once. quotient.lift' and variants use implicit brackets for the setoid argument.

[Mario Carneiro]

In case it wasn't obvious, you can always define a binary function on quotients by iterated quot.lift, but you get different proof obligations than the hypothetical quot.lift2.

[Mario Carneiro]

You should generally use quotient instead of quot if your relation is in fact an equivalence relation

[Bhavik Mehta]

Mario Carneiro said:

In case it wasn't obvious, you can always define a binary function on quotients by iterated quot.lift, but you get different proof obligations than the hypothetical quot.lift2.

Yeah this was why I was initially surprised by not having quot.lift2

[Bhavik Mehta]

Mario Carneiro said:

You should generally use quotient instead of quot if your relation is in fact an equivalence relation

Is there a particular reason for this?

[Mario Carneiro]

there are better lemmas, like quotient.sound

[Mario Carneiro]

and quotient.lift2 for that matter

[Bhavik Mehta]

Alright, I was refactoring some definitions code where I used quotient so was thinking about if this would be better - i'll keep the quotients as they are then!

[Yury G. Kudryashov]

If you use quotient or quotient', then you tell Lean that your relation is already already an equivalence relation, and later you (and Lean) can use this information to use a simpler reasoning.