Functors can be applied to Equiv
s. #
def functor.map_equiv (f : Type u → Type v) [functor f] [LawfulFunctor f] :
α ≃ β → f α ≃ f β
@[simp]
theorem
Functor.map_equiv_apply
(f : Type u → Type v)
[inst : Functor f]
[inst : LawfulFunctor f]
{α : Type u}
{β : Type u}
(h : α ≃ β)
(x : f α)
:
↑(Functor.map_equiv f h) x = ↑h <$> x
@[simp]
theorem
Functor.map_equiv_symm_apply
(f : Type u → Type v)
[inst : Functor f]
[inst : LawfulFunctor f]
{α : Type u}
{β : Type u}
(h : α ≃ β)
(y : f β)
:
↑(Equiv.symm (Functor.map_equiv f h)) y = ↑(Equiv.symm h) <$> y