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

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

@[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