Zulip Chat Archive

Stream: Is there code for X?

Topic: quotient by bottom setoid


view this post on Zulip 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)?

view this post on Zulip Bhavik Mehta (Jul 09 2020 at 17:15):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 09 2020 at 18:50):

But it should be easy to write it.

view this post on Zulip 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