unique for two elements

Stream: general

[Eric Wieser]

In #12671, I state things about indexed families where the indexing family has exactly two elements (and I need to refer explicitly to those elements).

For one element, we can use unique X and default.

Whats's the preferred way to refer to this type of thing for two elements?

1. {i j : ι} (hij : i ≠ j) (h : (set.univ : set ι) = {i, j}) : foo i j
2. [fintype ι] {i j : ι} (hij : i ≠ j) (h : (finset.univ : set ι) = {i, j}) : foo i j
3. {i j : ι} (hij : i ≠ j) (h : ∀ k, k = i ∨ k = j) : foo i j
4. [almost_unique ι] : foo default other_default

[Eric Wieser]

Currently I've gone with 1, but 2 has the benefit that h is often true by rfl

[Junyan Xu]

X ≃ bool or fin 2? f : bool → X function.bijective f?

[Eric Rodriguez]

I was thinking that maybe it's better to state the result for fin 2 first and do an equivalence, too

[Eric Rodriguez]

fin 2 also has some sort of an API, which is nice (like the fin 3 stuff earlier)

[Eric Wieser]

I guess I only really care about zmod 2 and units ℤ

[Eric Wieser]

Another one is punit ⊕ punit