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

instance EquivFunctorPerm : EquivFunctor Equiv.Perm

Equations

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

instance EquivFunctorFinset : EquivFunctor Finset

Equations

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

instance EquivFunctorFintype : EquivFunctor Fintype

Equations

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