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) [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.
Instances For
    @[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] :
    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.
    Instances For
      @[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] :