equiv_functor instances #
We derive some equiv_functor instances, to enable equiv_rw to rewrite under these functions.
@[protected, instance]
Equations
- equiv_functor_unique = {map := λ (α β : Type u_1) (e : α ≃ β), ⇑(e.unique_congr), map_refl' := equiv_functor_unique._proof_1, map_trans' := equiv_functor_unique._proof_2}
@[protected, instance]
Equations
- equiv_functor_perm = {map := λ (α β : Type u_1) (e : α ≃ β) (p : equiv.perm α), (e.symm.trans p).trans e, map_refl' := equiv_functor_perm._proof_1, map_trans' := equiv_functor_perm._proof_2}
@[protected, instance]
Equations
- equiv_functor_finset = {map := λ (α β : Type u_1) (e : α ≃ β) (s : finset α), finset.map e.to_embedding s, map_refl' := equiv_functor_finset._proof_1, map_trans' := equiv_functor_finset._proof_2}
@[protected, instance]
Equations
- equiv_functor_fintype = {map := λ (α β : Type u_1) (e : α ≃ β) (s : fintype α), fintype.of_bijective ⇑e _, map_refl' := equiv_functor_fintype._proof_1, map_trans' := equiv_functor_fintype._proof_2}