EquivFunctor instances

We derive some EquivFunctor instances, to enable equiv_rw to rewrite under these functions.

ink

instance EquivFunctorUnique : EquivFunctor Unique

Equations

• EquivFunctorUnique = EquivFunctor.mk fun {α β} e => ↑(Equiv.uniqueCongr e)

ink

instance EquivFunctorPerm : EquivFunctor Equiv.Perm

Equations

• EquivFunctorPerm = EquivFunctor.mk fun {α β} e p => Equiv.trans (Equiv.trans (Equiv.symm e) p) e

ink

instance EquivFunctorFinset : EquivFunctor Finset

Equations

• EquivFunctorFinset = EquivFunctor.mk fun {α β} e s => Finset.map (Equiv.toEmbedding e) s

ink

instance EquivFunctorFintype : EquivFunctor Fintype

Equations

• EquivFunctorFintype = EquivFunctor.mk fun {α β} e s => Fintype.ofBijective ↑e (_ : Function.Bijective ↑e)