Can we fix Setoid and Quotient?

Stream: lean4

[François G. Dorais]

There are a lot of problems with these, mostly due to what is now archaic design (which made sense at the time!). I would like to collect those problems and potential solutions here so that we can propose a general solution that would work for Lean core, with a hopefully small enough amount of effort on their end.

[François G. Dorais]

To get started:

• I don't think Setoid needs to be a class.
• It should extend Equivalence so that refl, symm and trans fields are directly accessible.

[Yongle Hu]

I think @Yuyang Zhao

[Eric Wieser]

I don't see how extending Equivalence could work

[François G. Dorais]

structure Rel (α β) where r : α → β → Prop
structure Setoid (α) extends Rel α α, Equivalence toRel.r

[Eric Wieser]

Replacing docs#Rel I guess

[Andrew Yang]

That would cause friction on the Rel side though.
Why not just define lemma Setoid.refl (r) := r.is_equiv.refl etc?

[François G. Dorais]

Right, better not replace Rel then.

private structure Setoid.Rel (α) where r : α → α → Prop
structure Setoid (α) extends Setoid.Rel α, Equivalence toRel.r

The main point is to have a nice construction syntax:

def foo (α) : Setoid α where
  r x y := sorry
  refl := sorry
  symm := sorry
  trans := sorry

[Eric Wieser]

is_eqv.refl := sorry isn't much worse

[François G. Dorais]

I don't understand.

[François G. Dorais]

Ah! Do you mean this?

def foo (α) : Setoid α where
  r x y := sorry
  iseqv.refl := sorry
  iseqv.symm := sorry
  iseqv.trans := sorry

[François G. Dorais]

Surely Setoid.iseqvneeds to be corrected.

[Eric Wieser]

I agree that iseqv doesn't match #naming