Zulip Chat Archive

Stream: general

Topic: local attribute instance setoid

Yury G. Kudryashov (Jan 29 2022 at 23:03):

Some parts of the library define non-canonical setoids (e.g., docs#uniform_space.separation_setoid or docs#path.homotopic.setoid) then use local attribute [instance] *setoid to deal with the corresponding quotients.

Yury G. Kudryashov (Jan 29 2022 at 23:04):

I don't like this design choice for the following reason: once you want to deal with two non-canonical setoids on a space, you just can't do it.

Mario Carneiro (Jan 29 2022 at 23:05):

better yet, remove setoid and quotient taking it as a type class altogether

Mario Carneiro (Jan 29 2022 at 23:06):

I don't think it's ever done me any favors

Yury G. Kudryashov (Jan 29 2022 at 23:06):

This way we loose [[x]], what else?

Mario Carneiro (Jan 29 2022 at 23:07):

not necessarily; you could still have quotient.mk {A} {r : A -> A -> Prop} {h : equivalence r} : A -> quotient A r

Reid Barton (Jan 29 2022 at 23:07):

Would it possible for the relation in question to be inferred from the expected type of [[x]], rather than the type of x?

Mario Carneiro (Jan 29 2022 at 23:07):

it would often not be usable because it has to infer the type from the outside but I think that's par for the course

Yury G. Kudryashov (Jan 29 2022 at 23:08):

Actually, we can use quot.mk and have an argument [is_equivalence α r] in some lemmas.

Mario Carneiro (Jan 29 2022 at 23:08):

not to mention that best practice is to alias quot.mk for each individual quotient anyway

Yury G. Kudryashov (Jan 29 2022 at 23:09):

Adding aliases for quot.mk is what I was going to propose.

Yury G. Kudryashov (Jan 29 2022 at 23:10):

(side note: am I right that docs#pseudo_metric.dist_setoid and docs#uniform_space.separation_setoid are equivalent?)

Eric Wieser (Jan 29 2022 at 23:51):

What's the advantage of removing setoid instead of just making it a non-class?

Mario Carneiro (Jan 29 2022 at 23:52):

It's not very useful on its own, docs#equivalence and/or docs#is_equiv seem to be reasonable replacements

Yury G. Kudryashov (Jan 29 2022 at 23:55):

We have some theory of bundled setoids but I think that we should use quot.* + [is_equiv α r] in lemmas that need r to be an equivalence relation + instances [is_equiv] for setoid (no longer a typeclass), con etc.

Eric Wieser (Jan 29 2022 at 23:57):

Right, I had the lattice structures on bundled setoids in mind

Kevin Buzzard (Jan 29 2022 at 23:57):

(Just to remark that Leo recently changed setoid in lean 4 not to be a class IIRC)

Eric Wieser (Jan 29 2022 at 23:59):

Isn't [is_equiv α r] going to run into the same problems as [is_monoid_hom f] did?

Mario Carneiro (Jan 30 2022 at 00:02):

It's not like there are a lot of equivalence combinators

Yury G. Kudryashov (Jan 30 2022 at 01:35):

Usually it will find a high priority instance for this particular relation.

Yaël Dillies (Jan 30 2022 at 06:50):

Yury G. Kudryashov said:

Some parts of the library define non-canonical setoids (e.g., docs#uniform_space.separation_setoid or docs#path.homotopic.setoid) then use local attribute [instance] *setoid to deal with the corresponding quotients.

#11728 does precisely that and I don't like it either.