Mental model for Setoid vs Equiv

Stream: new members

[Dan Abramov]

I'm going through exercises in Tao's Analysis, and at some point there's a custom Setoid instance set up via Set cardinality equality:

abbrev SetTheory.Set.EqualCard (X Y:Set) : Prop := ∃ f : X → Y, Function.Bijective f

-- ...

instance SetTheory.Set.EqualCard.inst_setoid : Setoid SetTheory.Set := ⟨ EqualCard, {refl, symm, trans} ⟩

Later in exercises, we sometimes use ≃ to set up bijections between sets (which I understand to be Equiv), and sometimes we use ≈ (which I understand to be Setoid). Due to similar notation, I often confuse these.

I was wondering if there's a good mental model for whether one is more "powerful" than the other in some way. At least in the exercises in that chapter, I'm able to freely convert between the two. For example, this typechecks:

  have hequiv : Permutations (n + 1) ≃ Fin (n + 1) ×ˢ (Permutations n) := by
    sorry -- doesn't matter

  have hsetoid : Permutations (n + 1) ≈ Fin (n + 1) ×ˢ (Permutations n) := by
    use hequiv -- can rely on this one
    apply Equiv.bijective

But this also typechecks:

  have hsetoid : Permutations (n + 1) ≈ Fin (n + 1) ×ˢ (Permutations n) := by
    sorry -- doesn't matter

  have hequiv : Permutations (n + 1) ≃ Fin (n + 1) ×ˢ (Permutations n) := by
    exact Equiv.ofBijective hsetoid.choose hsetoid.choose_spec -- can rely on this one

So they seem to be "equally powerful" concepts in this case (and just mean a bijection).

Is this because of how my instance is set up, and not true in general? If it's not true in general, is there some mental model for how to think when to "reach for" Equiv vs Setoid?

Thanks.

[Dan Abramov]

I guess maybe Equiv generally represents a bijection between two types, whereas Setoid in general is just an equality-shaped relationship, and in this case the relation happens to be "having equal cardinality" which corresponds to a bijection.

I'm still not sure what this says about Equiv vs Setoid in general, e.g. in other cases is it possible to get one from the other, or are these unrelated concepts that happen to overlap here.

[Yakov Pechersky]

Equiv is data: it is a bijective function to convert from a term of one typex : A to another type n : B. Setoid is also data: is a relation between x y : A such that x and y are fuzzy-equal.

[Yakov Pechersky]

Ah, you just said that.

[Dan Abramov]

Is it possible to turn one into the other in the general case? Or are they orthogonal and just happen to overlap in my specific instance?

[Yakov Pechersky]

One would say x ≈ y (term-level), the notation is a relation between terms.

[Yakov Pechersky]

In your case, you have a "relationship" between types. So an Equiv is "more" informative because not only does it say that the two types are kinda the same, it even says how to convert a p : Perm (n + 1) to pair : Fin (n + 1) x Perm n

[Yakov Pechersky]

It's fuzzier in the Analysis context since you're building up set theory, which is a bit muddled when doing via type theory.

[Robin Arnez]

Setoid is more general since it describes some equivalence relation; the main point of it is to build a quotient type later, e.g. docs#Cardinal using the type setoid or docs#Multiset using the list setoid. In this case α ≈ β happens to defined as Nonempty (α ≃ β) (docs#Cardinal.isEquivalent).

[Dan Abramov]

Ah ok, so Setoid doesn't have to represent a bijection because it's often used to "crunch" things into being equal (via quotients).

[Aaron Liu]

If I have X Y : Set and I have hxy : X ≈ Y then I know that there exists a function f : X → Y such that f is bijective (but I don't know which one).
If I have X Y : Set and I have equivXY : X ≃ Y, then that means I have a function ⇑equivXY : X → Y and I have a function ⇑equivXY.symm : Y → X and I know these are two-sided inverses.

[Aaron Liu]

if I define an Equiv and then use it later, I know the function I get out is the same function I put in

[Rado Kirov]

So one can go from Setoid to Equiv with classical.choose?

[Robin Arnez]

A better alternative in proofs would be obtain ⟨eqv⟩ := h though

[Rado Kirov]

Obtain only works for getting Props out (I have gotten this error a few times)

[Matt Diamond]

maybe this is obvious, but I didn't see anyone mention the fact that Setoid is a relation within a type, whereas Equiv is a relation between types

[Dan Abramov]

Ah interesting, I guess in this formalization it kinda works both ways because we have Sets but they're also treated as Types (there's a coe).

[Matt Diamond]

also, types themselves are members of a type (Type), which explains why an Equiv can be viewed as the basis of a Setoid for the type Type (which is docs#Cardinal.isEquivalent)

[Matt Diamond]

but that's a whole other thing

[Alfredo Moreira-Rosa]

For me Equiv is a way to say two different types have a bijection between them, while Setoid says two instances of a type have a weak equality that you can make into an equality by using a quotient.

[Matt Diamond]

yeah, like you could have a Setoid on the natural numbers by saying odd numbers are equivalent and even numbers are equivalent, but it wouldn't make sense to say that a bijection exists between two numbers... a Setoid is about relating terms, not (necessarily) types

[Dan Abramov]

Thanks, this is all very helpful, I think it makes sense to me now.