EquivFunctor instances

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

instance EquivFunctorUnique : EquivFunctor Unique

Equations

• EquivFunctorUnique = { map := fun {α β : Type u_1} (e : α ≃ β) => ⇑e.uniqueCongr, map_refl' := EquivFunctorUnique.proof_1, map_trans' := EquivFunctorUnique.proof_2 }

instance EquivFunctorPerm : EquivFunctor Equiv.Perm

Equations

• EquivFunctorPerm = { map := fun {α β : Type u_1} (e : α ≃ β) (p : Equiv.Perm α) => (e.symm.trans p).trans e, map_refl' := EquivFunctorPerm.proof_1, map_trans' := @EquivFunctorPerm.proof_2 }

instance EquivFunctorFinset : EquivFunctor Finset

Equations

• EquivFunctorFinset = { map := fun {α β : Type u_1} (e : α ≃ β) (s : Finset α) => Finset.map e.toEmbedding s, map_refl' := EquivFunctorFinset.proof_1, map_trans' := @EquivFunctorFinset.proof_2 }

instance EquivFunctorFintype : EquivFunctor Fintype

Equations

• One or more equations did not get rendered due to their size.