Equivalences between containers induced elementwise

Stream: Is there code for X?

[Eric Wieser]

Do we have any of the following?

• α ≃ β → list α ≃ list β
• α ≃ β → multiset α ≃ multiset β
• α ≃ β → finset α ≃ finset β

[Kevin Buzzard]

Is there a tactic which does all these?

[Eric Wieser]

Probably more a metaprogram like to_additive

[Eric Wieser]

I think we might have docs#equiv_functor or similar, but it's not universe polymorphic so isn't as strong as the defs above would be

[Floris van Doorn]

There is docs#equiv.finset_congr

[Eric Wieser]

Well that's one out of three...

[Yury G. Kudryashov]

docs#equiv.list_equiv_of_equiv

[Yury G. Kudryashov]

And we don't have a version for multiset. Could you please add it as an add_equiv?

[Kevin Buzzard]

I read that as "add it with @[to_additive]" and I thought "but we don't have addtisets"

[Yaël Dillies]

Overadditivization :rofl:
Have a look at docs#add_salem_spencer.sum

[Yaël Dillies]

to_additive tricked me on that one.

[Eric Wieser]

@Huỳnh Trần Khanh, this is in the context of the α ≃ β → sym α n ≃ sym β n def I asked for in your stars and bars PR. It looks like equiv.sym_congr might be a better name than sym.map_equiv.

[Eric Wieser]

Are you happy to add equiv.multiset_congr : α ≃ β → multiset α ≃+ multiset β at the same time?