# Documentation

Mathlib.Logic.Equiv.Functor

# 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.

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

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 α α') :
↑() 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 β β') :
().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) [] [] :
Bifunctor.mapEquiv F () () = Equiv.refl (F α α')