Decidable rels on a quotient

Stream: Is there code for X?

[Yaël Dillies]

Are we missing the decidable instances for docs#quotient.lift and docs#quotient.lift₂? Or do they not even theoretically exist?

[Yury G. Kudryashov]

Do you mean [i : setoid α] (p : α → Prop) [decidable_pred p] (hp : ∀ x y, x ≈ y → p x = p y) (a : quotient i) : decidable (quotient.lift p hp a)?

[Yury G. Kudryashov]

It should be possible to decide using recursion on a (another quotient.lift)

[Yury G. Kudryashov]

Or more generally, p depends on quotient.lift f hf a?

[Yaël Dillies]

Something along those lines, yeah. I can't tell you exactly offhand, because my use case is not the most general one.