Stream: general

Topic: functor map equiv

Johan Commelin (Jun 08 2020 at 20:44):

Is there some control.functor fu that will give me

e : σ ≃ τ
⊢ finset σ ≃ finset τ


Kevin Buzzard (Jun 08 2020 at 20:46):

tactic#equiv_rw_type

Kevin Buzzard (Jun 08 2020 at 20:47):

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

Scott Morrison (Jun 09 2020 at 01:27):

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 (Jun 09 2020 at 01:27):

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

Scott Morrison (Jun 09 2020 at 01:28):

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 (Jun 09 2020 at 01:28):

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

Scott Morrison (Jun 09 2020 at 01:32):

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

(deleted)

(deleted)

(deleted)

(deleted)

(deleted)

(deleted)

Scott Morrison (Jun 09 2020 at 03:01):

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 (Jun 09 2020 at 03:01):

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 (Jun 09 2020 at 03:30):

#2997

Last updated: Dec 20 2023 at 11:08 UTC