## Stream: Is there code for X?

### Topic: quotient by bottom setoid

#### Bhavik Mehta (Jul 09 2020 at 17:14):

Is there anything in mathlib about what happens when I quotient by the bottom setoid (ie equality)?

#### Bhavik Mehta (Jul 09 2020 at 17:15):

I'd be happy with an equivalence between the original type and the quotiented type

#### Yury G. Kudryashov (Jul 09 2020 at 18:50):

Can't find it in data/equiv/basic and data/setoid/basic, so I guess we don't have this equivalence.

#### Yury G. Kudryashov (Jul 09 2020 at 18:50):

But it should be easy to write it.

#### Bhavik Mehta (Jul 09 2020 at 19:12):

def quotient_bot_equiv (α : Type*) : quotient (⊥ : setoid α) ≃ α :=
{ to_fun := λ x, quotient.lift_on' x id (λ _ _, id),
inv_fun := quotient.mk',
left_inv := λ x,
begin
apply quotient.induction_on' x,
intro x,
refl,
end,
right_inv := λ x, rfl }


Yeah I ended up doing it

Last updated: May 16 2021 at 05:21 UTC