Zulip Chat Archive

Stream: Is there code for X?

Topic: quotient.exists_rep without a typeclass instance


Eric Wieser (Dec 07 2020 at 17:32):

Is there a reason docs#quotient.exists_rep takes [s : setoid A] and not {s : setoid A}? I have a quotient constructed from a non-canonical setoid, so I don't have a global instance available.

Adam Topaz (Dec 07 2020 at 17:33):

docs#quotient.exists_rep' ?

Adam Topaz (Dec 07 2020 at 17:33):

no :(

Then docs#quot.exists_rep

Eric Wieser (Dec 07 2020 at 17:33):

I wonder what breaks if those arguments all become implicit...

Adam Topaz (Dec 07 2020 at 17:34):

I don't think anything breaks. quotient.mk' is defeq to quot.mk _

Eric Wieser (Dec 07 2020 at 17:35):

Oh, the problem is this code is all in core

Eric Wieser (Dec 07 2020 at 17:35):

So changing it to take {} arguments is harder to test

Adam Topaz (Dec 07 2020 at 17:36):

src#quotient.lift_on'

Adam Topaz (Dec 07 2020 at 17:36):

That's from mathlib, and it looks like a few other quotient.foo' things are missing as well.

Eric Wieser (Dec 07 2020 at 17:39):

Ugh, I guess exists_rep' is difficult because the ⟦a⟧ notation used in its statement isn't available without the typeclass instance.

Adam Topaz (Dec 07 2020 at 17:40):

It could use quotient.mk'

Adam Topaz (Dec 07 2020 at 17:42):

def quotient.exists_rep' {α : Type*} {S : setoid α} (x : quotient S) :  (a : α), quotient.mk' a = x :=
  quot.exists_rep _

Eric Wieser (Dec 07 2020 at 18:00):

Oh, which infers s from the rhs

Adam Topaz (Dec 07 2020 at 19:00):

It infers S from the type of x

Eric Wieser (Dec 07 2020 at 20:36):

Right, I mean the inferred argument to mk'

Eric Wieser (Dec 07 2020 at 22:04):

Thanks for the tip to use the quot versions anyway, that tidied up my proof nicely.

Adam Topaz (Dec 07 2020 at 22:13):

IMO the main point where quotient is useful over quot is if you have to use quotient.exact. quot.exact spits out something with eqv_gen which is annoying if you already have an equivalence relation


Last updated: Dec 20 2023 at 11:08 UTC