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) [Functor f] [LawfulFunctor f] (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.mapEquiv_apply {α : Type u} {β : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (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) [Functor f] [LawfulFunctor f] (h : α ≃ β) (y : f β) : ↑(Functor.mapEquiv f h).symm y = ↑h.symm <$> y

@[simp]

theorem Functor.mapEquiv_refl {α : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] : Functor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

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

Apply a bifunctor to a pair of Equivs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bifunctor.mapEquiv_apply {α : Type u} {β : Type u} {α' : Type v} {β' : Type v} (F : Type u → Type v → Type w) [Bifunctor F] [LawfulBifunctor F] (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) [Bifunctor F] [LawfulBifunctor F] (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) [Bifunctor F] [LawfulBifunctor F] : Bifunctor.mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')