quotient by bottom setoid

Stream: Is there code for X?

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

But it should be easy to write it.

[Bhavik Mehta]

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