Documentation

Mathlib.Control.Bifunctor

Functors with two arguments #

This file defines bifunctors.

A bifunctor is a function F : Type* → Type* → Type* along with a bimap which turns F α βinto F α' β' given two functions α → α' and β → β'. It further

Main declarations #

class Bifunctor (F : Type u₀ → Type u₁ → Type u₂) :
Type (max (max (u₀ + 1) (u₁ + 1)) u₂)

Lawless bifunctor. This typeclass only holds the data for the bimap.

  • bimap : {α α' : Type u₀} → {β β' : Type u₁} → (αα')(ββ')F α βF α' β'
Instances
    class LawfulBifunctor (F : Type u₀ → Type u₁ → Type u₂) [Bifunctor F] :

    Bifunctor. This typeclass asserts that a lawless Bifunctor is lawful.

    • id_bimap : ∀ {α : Type u₀} {β : Type u₁} (x : F α β), bimap id id x = x
    • bimap_bimap : ∀ {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀α₁) (f' : α₁α₂) (g : β₀β₁) (g' : β₁β₂) (x : F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' f) (g' g) x
    Instances
      theorem LawfulBifunctor.id_bimap {F : Type u₀ → Type u₁ → Type u₂} :
      ∀ {inst : Bifunctor F} [self : LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β), bimap id id x = x
      theorem LawfulBifunctor.bimap_bimap {F : Type u₀ → Type u₁ → Type u₂} :
      ∀ {inst : Bifunctor F} [self : LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀α₁) (f' : α₁α₂) (g : β₀β₁) (g' : β₁β₂) (x : F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' f) (g' g) x
      theorem LawfulBifunctor.bimap_id_id {F : Type u₀ → Type u₁ → Type u₂} :
      ∀ {inst : Bifunctor F} [self : LawfulBifunctor F] {α : Type u₀} {β : Type u₁}, bimap id id = id
      theorem LawfulBifunctor.bimap_comp_bimap {F : Type u₀ → Type u₁ → Type u₂} :
      ∀ {inst : Bifunctor F} [self : LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀α₁) (f' : α₁α₂) (g : β₀β₁) (g' : β₁β₂), bimap f' g' bimap f g = bimap (f' f) (g' g)
      @[reducible, inline]
      abbrev Bifunctor.fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] {α : Type u₀} {α' : Type u₀} {β : Type u₁} (f : αα') :
      F α βF α' β

      Left map of a bifunctor.

      Equations
      Instances For
        @[reducible, inline]
        abbrev Bifunctor.snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] {α : Type u₀} {β : Type u₁} {β' : Type u₁} (f : ββ') :
        F α βF α β'

        Right map of a bifunctor.

        Equations
        Instances For
          theorem Bifunctor.fst_id {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} :
          theorem Bifunctor.id_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) :
          theorem Bifunctor.snd_id {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} :
          theorem Bifunctor.id_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) :
          theorem Bifunctor.fst_comp_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {α₂ : Type u₀} {β : Type u₁} (f : α₀α₁) (f' : α₁α₂) :
          theorem Bifunctor.comp_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {α₂ : Type u₀} {β : Type u₁} (f : α₀α₁) (f' : α₁α₂) (x : F α₀ β) :
          theorem Bifunctor.fst_comp_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {β₀ : Type u₁} {β₁ : Type u₁} (f : α₀α₁) (f' : β₀β₁) :
          theorem Bifunctor.fst_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {β₀ : Type u₁} {β₁ : Type u₁} (f : α₀α₁) (f' : β₀β₁) (x : F α₀ β₀) :
          theorem Bifunctor.snd_comp_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {β₀ : Type u₁} {β₁ : Type u₁} (f : α₀α₁) (f' : β₀β₁) :
          theorem Bifunctor.snd_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {β₀ : Type u₁} {β₁ : Type u₁} (f : α₀α₁) (f' : β₀β₁) (x : F α₀ β₀) :
          theorem Bifunctor.snd_comp_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β₀ : Type u₁} {β₁ : Type u₁} {β₂ : Type u₁} (g : β₀β₁) (g' : β₁β₂) :
          theorem Bifunctor.comp_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β₀ : Type u₁} {β₁ : Type u₁} {β₂ : Type u₁} (g : β₀β₁) (g' : β₁β₂) (x : F α β₀) :
          Equations
          instance Bifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] :
          Equations
          • Bifunctor.flip = { bimap := fun {α' : Type ?u.30} {β' : Type ?u.31} (f : α') (f' : β') (x : flip F ) => bimap f' f x }
          instance LawfulBifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] :
          Equations
          • =
          Equations
          @[instance 10]
          instance Bifunctor.functor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] {α : Type u₀} :
          Functor (F α)
          Equations
          • One or more equations did not get rendered due to their size.
          @[instance 10]
          instance Bifunctor.lawfulFunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} :
          Equations
          • =
          instance Function.bicompl.bifunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u_1 → Type u₀) (H : Type u_2 → Type u₁) [Functor G] [Functor H] :
          Equations
          • One or more equations did not get rendered due to their size.
          instance Function.bicompl.lawfulBifunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u_1 → Type u₀) (H : Type u_2 → Type u₁) [Functor G] [Functor H] [LawfulFunctor G] [LawfulFunctor H] [LawfulBifunctor F] :
          Equations
          • =
          instance Function.bicompr.bifunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u₂ → Type u_1) [Functor G] :
          Equations
          instance Function.bicompr.lawfulBifunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u₂ → Type u_1) [Functor G] [LawfulFunctor G] [LawfulBifunctor F] :
          Equations
          • =