Functors can be applied to Equivs.

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

ink

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.

ink

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

ink

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