# Documentation

Mathlib.Data.Equiv.Functor

# Functors can be applied to Equivs. #

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

def Functor.map_equiv (f : Type u → Type v) [inst : ] [inst : ] {α : 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) [inst : ] [inst : ] {α : Type u} {β : Type u} (h : α β) (x : f α) :
↑() x = h <$> x @[simp] theorem Functor.map_equiv_symm_apply (f : Type u → Type v) [inst : ] [inst : ] {α : Type u} {β : Type u} (h : α β) (y : f β) : ↑() y = ↑() <$> y