# Functor and bifunctors can be applied to Equivs. #

We define

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


and

def Bifunctor.mapEquiv (F : Type u → Type v → Type w) [Bifunctor F] [LawfulBifunctor F] :
α ≃ β → α' ≃ β' → F α α' ≃ F β β'

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

Apply a functor to an Equiv.

Equations
• = { toFun := , invFun := Functor.map h.symm, left_inv := , right_inv := }
Instances For
@[simp]
theorem Functor.mapEquiv_apply {α : Type u} {β : Type u} (f : Type u → Type v) [] [] (h : α β) (x : f α) :
(Functor.mapEquiv f h) x = h <$> x @[simp] theorem Functor.mapEquiv_symm_apply {α : Type u} {β : Type u} (f : Type u → Type v) [] [] (h : α β) (y : f β) : (Functor.mapEquiv f h).symm y = h.symm <$> y
@[simp]
theorem Functor.mapEquiv_refl {α : Type u} (f : Type u → Type v) [] [] :
= Equiv.refl (f α)
def Bifunctor.mapEquiv {α : Type u} {β : Type u} {α' : Type v} {β' : Type v} (F : Type u → Type v → Type w) [] [] (h : α β) (h' : α' β') :
F α α' F β β'

Apply a bifunctor to a pair of Equivs.

Equations
• = { toFun := bimap h h', invFun := bimap h.symm h'.symm, left_inv := , right_inv := }
Instances For
@[simp]
theorem Bifunctor.mapEquiv_apply {α : Type u} {β : Type u} {α' : Type v} {β' : Type v} (F : Type u → Type v → Type w) [] [] (h : α β) (h' : α' β') (x : F α α') :
(Bifunctor.mapEquiv F h h') x = bimap (⇑h) (⇑h') x
@[simp]
theorem Bifunctor.mapEquiv_symm_apply {α : Type u} {β : Type u} {α' : Type v} {β' : Type v} (F : Type u → Type v → Type w) [] [] (h : α β) (h' : α' β') (y : F β β') :
(Bifunctor.mapEquiv F h h').symm y = bimap (⇑h.symm) (⇑h'.symm) y
@[simp]
theorem Bifunctor.mapEquiv_refl_refl {α : Type u} {α' : Type v} (F : Type u → Type v → Type w) [] [] :