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

• respects the identity: bimap id id = id
• composes in the obvious way: (bimap f' g') ∘ (bimap f g) = bimap (f' ∘ f) (g' ∘ g)

Main declarations

• Bifunctor: A typeclass for the bare bimap of a bifunctor.
• LawfulBifunctor: A typeclass asserting this bimap respects the bifunctor laws.

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 α' β'

class LawfulBifunctor (F : Type u₀ → Type u₁ → Type u₂) [Bifunctor F] : Prop

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

theorem LawfulBifunctor.id_bimap {F : Type u₀ → Type u₁ → Type u₂} [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₂} [Bifunctor F] [self : LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {α₂ : Type u₀} {β₀ : Type u₁} {β₁ : 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₂} [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₂} [Bifunctor F] [self : LawfulBifunctor F] {α₀ : Type u₀} {α₁ : Type u₀} {α₂ : Type u₀} {β₀ : Type u₁} {β₁ : 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

• Bifunctor.fst f = bimap f id

@[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

• Bifunctor.snd f = bimap id f

theorem Bifunctor.fst_id {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} : Bifunctor.fst id = id

theorem Bifunctor.id_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) : Bifunctor.fst id x = x

theorem Bifunctor.snd_id {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} : Bifunctor.snd id = id

theorem Bifunctor.id_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) : Bifunctor.snd id x = x

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' : α₁ → α₂) : Bifunctor.fst f' ∘ Bifunctor.fst f = Bifunctor.fst (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 α₀ β) : Bifunctor.fst f' (Bifunctor.fst f x) = Bifunctor.fst (f' ∘ f) x

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' : β₀ → β₁) : Bifunctor.fst f ∘ Bifunctor.snd f' = bimap 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 α₀ β₀) : Bifunctor.fst f (Bifunctor.snd f' x) = bimap f f' x

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' : β₀ → β₁) : Bifunctor.snd f' ∘ Bifunctor.fst f = bimap 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 α₀ β₀) : Bifunctor.snd f' (Bifunctor.fst f x) = bimap f f' x

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' : β₁ → β₂) : Bifunctor.snd g' ∘ Bifunctor.snd g = Bifunctor.snd (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 α β₀) : Bifunctor.snd g' (Bifunctor.snd g x) = Bifunctor.snd (g' ∘ g) x

instance Prod.bifunctor : Bifunctor Prod

Equations

• Prod.bifunctor = { bimap := @Prod.map }

instance Prod.lawfulBifunctor : LawfulBifunctor Prod

Equations

• Prod.lawfulBifunctor = ⋯

instance Bifunctor.const : Bifunctor Functor.Const

Equations

• Bifunctor.const = { bimap := fun {α α' : Type u_1} {β β' : Type u_2} (f : α → α') (x : β → β') => f }

instance LawfulBifunctor.const : LawfulBifunctor Functor.Const

Equations

• LawfulBifunctor.const = ⋯

instance Bifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] : Bifunctor (flip F)

Equations

• Bifunctor.flip = { bimap := fun {_α α' : Type u₁} {_β β' : Type u₀} (f : _α → α') (f' : _β → β') (x : flip F _α _β) => bimap f' f x }

instance LawfulBifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] : LawfulBifunctor (flip F)

Equations

• ⋯ = ⋯

instance Sum.bifunctor : Bifunctor Sum

Equations

• Sum.bifunctor = { bimap := @Sum.map }

instance Sum.lawfulBifunctor : LawfulBifunctor Sum

Equations

• Sum.lawfulBifunctor = ⋯

@[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₀} : LawfulFunctor (F α)

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] : Bifunctor (Function.bicompl F G 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] : LawfulBifunctor (Function.bicompl F G H)

Equations

• ⋯ = ⋯

instance Function.bicompr.bifunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u₂ → Type u_1) [Functor G] : Bifunctor (Function.bicompr G F)

Equations

• Function.bicompr.bifunctor G = { bimap := fun {_α α' : Type u₀} {_β β' : Type u₁} (f : _α → α') (f' : _β → β') (x : Function.bicompr G F _α _β) => bimap f f' <$> x }

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] : LawfulBifunctor (Function.bicompr G F)

Equations

• ⋯ = ⋯