Quotient that identifies all the members of a set

Stream: Is there code for X?

[Chris Wong]

Hi all, is there a quotient type that treats all members of a particular subset as equal, leaving the remaining values unchanged?

I remember a discussion thread on this a while ago but I can't find the right keywords for it :sweat_smile:

#xy: I'm looking into graph contraction (for minors). If I want to contract a set of vertices, I can do that by identifying them all and removing loops. I want to see how practical it is to use quotients for this.

[Timo Carlin-Burns]

docs#Trunc

[Chris Wong]

Trunc flattens all values. I only want to flatten those in a particular subset.

[Yaël Dillies]

@Yury G. Kudryashov, did this ever land?

[Yury G. Kudryashov]

AFAIK, no

[Yury G. Kudryashov]

AFAIR, there was a discussion about different ways to do it but I don't remember it landing.

[Kyle Miller]

Previous discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Equivalence.20Relation.20associated.20to.20a.20subset/near/409633101

I'll mention again that the API I think would be nice would be that you give it a S : Set (Set α) of some collection of sets to collapse. Yury had a possible implementation there, Setoid.map (.ker Sigma.fst) fun x : Σ i : S, i.1 => x.2.1.

[Chris Wong]

Thanks Kyle, I replied in the thread you linked.