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} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (h : α ≃ β) : f α ≃ f β

Apply a functor to an Equiv.

Equations

• Functor.mapEquiv f h = { toFun := Functor.map ⇑h, invFun := Functor.map ⇑h.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Functor.mapEquiv_apply {α β : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (h : α ≃ β) (x : f α) : (mapEquiv f h) x = ⇑h <$> x

@[simp]

theorem Functor.mapEquiv_symm_apply {α β : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (h : α ≃ β) (y : f β) : (mapEquiv f h).symm y = ⇑h.symm <$> y

@[simp]

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

def Bifunctor.mapEquiv {α β : Type u} {α' β' : 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

• Bifunctor.mapEquiv F h h' = { toFun := bimap ⇑h ⇑h', invFun := bimap ⇑h.symm ⇑h'.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Bifunctor.mapEquiv_apply {α β : Type u} {α' β' : Type v} (F : Type u → Type v → Type w) [Bifunctor F] [LawfulBifunctor F] (h : α ≃ β) (h' : α' ≃ β') (x : F α α') : (mapEquiv F h h') x = bimap (⇑h) (⇑h') x

@[simp]

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