functor map equiv

Stream: general

[Johan Commelin]

Is there some control.functor fu that will give me

e : σ ≃ τ
⊢ finset σ ≃ finset τ

for free?

[Kevin Buzzard]

tactic#equiv_rw_type

[Kevin Buzzard]

Does this actually work? From the man page: have e' : option α ≃ option β := by equiv_rw_type e

[Scott Morrison]

I should have made the docs clearer; generally equiv_rw_type is "for internal use only", and I'd typically imagined users to just useequiv_rw.

[Scott Morrison]

If it were option here, either of these would work:

[Scott Morrison]

import tactic.equiv_rw

example (σ τ : Type) (e : σ ≃ τ) : option σ ≃ option τ :=
by { equiv_rw e, refl, }

example (σ τ : Type) (e : σ ≃ τ) : option σ ≃ option τ :=
by { equiv_rw_type e, }

[Scott Morrison]

However it doesn't work out of the box with finset. Let me look into that.

[Scott Morrison]

Nope, I'm not going to have a quick answer for you. :-) I haven't thought about using equiv_rw for quotient types yet.

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

Sorry, my solution above was completely dumb. (It was me attempting to "be a robot", but I neither managed to avoid using any human knowledge of finset and multiset, or write something sensible.)

[Scott Morrison]

What you want is just this:

import data.finset
import tactic.equiv_rw

instance : equiv_functor multiset :=
{ map := λ α β e s, s.map e, }

@[simp]
lemma equiv.refl_to_embedding {α : Type*} :
  (equiv.refl α).to_embedding = function.embedding.refl α := rfl

attribute [simp] finset.map_refl

instance : equiv_functor finset :=
{ map := λ α β e s, s.map e.to_embedding, }

example (σ τ : Type) (e : σ ≃ τ) : finset σ ≃ finset τ :=
by { equiv_rw e, refl, }

[Scott Morrison]

#2997