quotient.exists_rep without a typeclass instance

Stream: Is there code for X?

[Eric Wieser]

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]

docs#quotient.exists_rep' ?

[Adam Topaz]

no :(

Then docs#quot.exists_rep

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

Oh, the problem is this code is all in core

[Eric Wieser]

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

[Adam Topaz]

src#quotient.lift_on'

[Adam Topaz]

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

[Eric Wieser]

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

[Adam Topaz]

It could use quotient.mk'

[Adam Topaz]

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

[Eric Wieser]

Oh, which infers s from the rhs

[Adam Topaz]

It infers S from the type of x

[Eric Wieser]

Right, I mean the inferred argument to mk'

[Eric Wieser]

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

[Adam Topaz]

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