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 β β'
source
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
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem Functor.mapEquiv_refl {α : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] :
    Functor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
    source
    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
      source
      @[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
      source
      @[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
      source
      @[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 α α')