Functors can be applied to Equivs.

def Functor.mapEquiv (f : Type u → Type v) [functor f] [LawfulFunctor f] :
    α ≃ β → f α ≃ f β

def Functor.map_equiv (f : Type u → Type v) [Functor f] [LawfulFunctor f] {α : Type u} {β : Type u} (h : α ≃ β) : f α ≃ f β

Apply a functor to an Equiv.

Equations

• Functor.map_equiv f h = { toFun := Functor.map ⇑h, invFun := Functor.map ⇑h.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Functor.map_equiv_apply (f : Type u → Type v) [Functor f] [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) [Functor f] [LawfulFunctor f] {α : Type u} {β : Type u} (h : α ≃ β) (y : f β) : (Functor.map_equiv f h).symm y = ⇑h.symm <$> y