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 : Functor f] [inst : 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) [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 β) :