A ≃ (set.univ A)

Stream: Is there code for X?

[Eric Wieser]

I can't find any of these:

example {A : Type*} : A ≃ (set.univ A) := by library_search
example {A : Type*} : A ≃ (finset.univ : finset A) := by library_search
example {A : Type*} : A ≃ subtype (λ a : A, true) := by library_search

[Eric Wieser]

They all fall out as something like:

example {A : Type*} : (finset.univ : finset A) ≃ A := {
      to_fun := coe,
      inv_fun := λ a, ⟨a, finset.mem_univ _⟩,
      left_inv := λ a, subtype.ext rfl,
      right_inv := λ a, rfl }

[Anatole Dedecker]

Did you see docs#equiv.subtype_univ_equiv ?

[Anatole Dedecker]

Or even better, docs#equiv.set.univ

[Eric Wieser]

That's exactly what I wanted, thanks

[Eric Wieser]

Unfortunately the definition doesn't work in my proof unless I make it reducible...

[Eric Wieser]

Ah, the reason was because I needed the equiv to unfold to coe during typeclass search, which only happens if its reducible. The fix was easy - add a letI that does that unfolding. Thanks again, that let me tie up #8070