EquivFunctor instances

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

instance EquivFunctorUnique : EquivFunctor Unique

Equations

• EquivFunctorUnique = EquivFunctor.mk fun {α β : Type u_1} (e : α ≃ β) => ⇑(Equiv.uniqueCongr e)

instance EquivFunctorPerm : EquivFunctor Equiv.Perm

Equations

• EquivFunctorPerm = EquivFunctor.mk fun {α β : Type u_1} (e : α ≃ β) (p : Equiv.Perm α) => (e.symm.trans p).trans e

instance EquivFunctorFinset : EquivFunctor Finset

Equations

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

instance EquivFunctorFintype : EquivFunctor Fintype

Equations

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