# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: quot.lift₂

#### Bhavik Mehta (May 23 2020 at 19:06):

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 (May 23 2020 at 19:41):

You should be using `quotient'`

;-) except that you can't have the notation with that

#### Bhavik Mehta (May 23 2020 at 19:43):

Where's `quotient'`

?

#### Chris Hughes (May 23 2020 at 19:46):

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 (May 23 2020 at 19:58):

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 (May 23 2020 at 19:59):

You should generally use `quotient`

instead of `quot`

if your relation is in fact an equivalence relation

#### Bhavik Mehta (May 23 2020 at 20:00):

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 (May 23 2020 at 20:00):

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 (May 23 2020 at 20:04):

there are better lemmas, like `quotient.sound`

#### Mario Carneiro (May 23 2020 at 20:04):

and `quotient.lift2`

for that matter

#### Bhavik Mehta (May 23 2020 at 20:05):

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 (May 23 2020 at 21:29):

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.

Last updated: May 17 2021 at 15:13 UTC