setoid "glue this set into a pt"

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have the setoid with relation given by (x ∈ s ∧ y ∈ s) ∨ x = y?

[Yury G. Kudryashov]

If not, what would be a good name for this setoid?

[Eric Wieser]

I guess you can build it as the kernel of if x ∈ s then none else some x to avoid needing to show an equivalence

[Yury G. Kudryashov]

At least if I don't care about using Classical.choice

[Eric Wieser]

Ah, good point

[Pedro Sánchez Terraf]

Yury G. Kudryashov said:

If not, what would be a good name for this setoid?

First try: blow down (tbh, trying to remember the “blow up” name, the word implode arrived to my mind in first place).

[Kevin Buzzard]

Or contract

[Yaël Dillies]

I was about to say contract as well.

[Reid Barton]

In homotopy theory this construction always also means that, when s is empty, we adjoin a new point; is that something you want to do?

[Yury G. Kudryashov]

This won't be a Setoid on the original space. I don't know. I just saw a bunch of counterexamples of type "the quotient of real numbers by gluing all rational numbers in 1 point" and realized that we can't formalize them (yet).

[Kyle Miller]

We could have a variant of docs4#Setoid.mkClasses that says for every point there is at most one set from the collection containing it, and then extend that collection with singleton sets to form a partition. If it's called Setoid.mkWithClasses, then you could have Setoid.mkWithClass : Set X -> Setoid X as a special case.

[Kyle Miller]

This avoids this whole issue with the empty set, because Setoid.mkClasses basically ignores the empty class since it's irrelevant to the equivalence relation.

[Kyle Miller]

This naming also avoids that contract and collapse make it sound like there's some point everything's being collapsed to.