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.8} (e : α ≃ β) => ⇑e.uniqueCongr, map_refl' := ⋯, map_trans' := EquivFunctorUnique._proof_3 }

instance EquivFunctorPerm : EquivFunctor Equiv.Perm

Equations

• EquivFunctorPerm = { map := fun {α β : Type ?u.13} (e : α ≃ β) (p : Equiv.Perm α) => (e.symm.trans p).trans e, map_refl' := ⋯, map_trans' := ⋯ }

instance EquivFunctorFinset : EquivFunctor Finset

Equations

• EquivFunctorFinset = { map := fun {α β : Type ?u.13} (e : α ≃ β) (s : Finset α) => Finset.map e.toEmbedding s, map_refl' := ⋯, map_trans' := ⋯ }

instance EquivFunctorFintype : EquivFunctor Fintype

Equations

• EquivFunctorFintype = { map := fun {α β : Type ?u.9} (e : α ≃ β) (x : Fintype α) => Fintype.ofBijective ⇑e ⋯, map_refl' := ⋯, map_trans' := EquivFunctorFintype._proof_3 }