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.
is_lawful_bifunctor: A typeclass asserting this bimap respects the bifunctor laws.

source

@[class]

structure bifunctor (F : Type u₀ → Type u₁ → Type u₂) :

Type (max (u₀+1) (u₁+1) u₂)

bimap : Π {α α' : Type ?} {β β' : Type ?}, (α → α') → (β → β') → F α β → F α' β'

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

Instances

source

@[class]

structure is_lawful_bifunctor (F : Type u₀ → Type u₁ → Type u₂) [bifunctor F] :

Type

id_bimap : ∀ {α : Type ?} {β : Type ?} (x : F α β), bimap id id x = x
bimap_bimap : ∀ {α₀ α₁ α₂ : Type ?} {β₀ β₁ β₂ : Type ?} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x

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

Instances

source

theorem is_lawful_bifunctor.bimap_id_id {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [self : is_lawful_bifunctor F] {α : Type l_3} {β : Type l_2} :

bimap id id = id

source

theorem is_lawful_bifunctor.bimap_comp_bimap {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [self : is_lawful_bifunctor F] {α₀ α₁ α₂ : Type l_3} {β₀ β₁ β₂ : Type l_2} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) :

bimap f' g' ∘ bimap f g = bimap (f' ∘ f) (g' ∘ g)

source

def bifunctor.fst {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] {α α' : Type u₀} {β : Type u₁} (f : α → α') :

F α β → F α' β

Left map of a bifunctor.

Equations

bifunctor.fst f = bimap f id

source

def bifunctor.snd {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] {α : Type u₀} {β β' : Type u₁} (f : β → β') :

F α β → F α β'

Right map of a bifunctor.

Equations

bifunctor.snd f = bimap id f

source

theorem bifunctor.id_fst {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) :

bifunctor.fst id x = x

source

theorem bifunctor.fst_id {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α : Type l_3} {β : Type l_2} :

bifunctor.fst id = id

source

theorem bifunctor.snd_id {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α : Type l_3} {β : Type l_2} :

bifunctor.snd id = id

source

theorem bifunctor.id_snd {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) :

bifunctor.snd id x = x

source

theorem bifunctor.fst_comp_fst {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ α₂ : Type l_3} {β : Type l_2} (f : α₀ → α₁) (f' : α₁ → α₂) :

bifunctor.fst f' ∘ bifunctor.fst f = bifunctor.fst (f' ∘ f)

source

theorem bifunctor.comp_fst {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ α₂ : Type u₀} {β : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (x : F α₀ β) :

bifunctor.fst f' (bifunctor.fst f x) = bifunctor.fst (f' ∘ f) x

source

theorem bifunctor.fst_snd {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁} (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀) :

bifunctor.fst f (bifunctor.snd f' x) = bimap f f' x

source

theorem bifunctor.fst_comp_snd {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ : Type l_3} {β₀ β₁ : Type l_2} (f : α₀ → α₁) (f' : β₀ → β₁) :

bifunctor.fst f ∘ bifunctor.snd f' = bimap f f'

source

theorem bifunctor.snd_comp_fst {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ : Type l_3} {β₀ β₁ : Type l_2} (f : α₀ → α₁) (f' : β₀ → β₁) :

bifunctor.snd f' ∘ bifunctor.fst f = bimap f f'

source

theorem bifunctor.snd_fst {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁} (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀) :

bifunctor.snd f' (bifunctor.fst f x) = bimap f f' x

source

theorem bifunctor.snd_comp_snd {F : Type l_3 → Type l_2 → Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α : Type l_3} {β₀ β₁ β₂ : Type l_2} (g : β₀ → β₁) (g' : β₁ → β₂) :

bifunctor.snd g' ∘ bifunctor.snd g = bifunctor.snd (g' ∘ g)

source

theorem bifunctor.comp_snd {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α : Type u₀} {β₀ β₁ β₂ : Type u₁} (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α β₀) :

bifunctor.snd g' (bifunctor.snd g x) = bifunctor.snd (g' ∘ g) x

source

@[protected, instance]

def prod.bifunctor :

bifunctor prod

Equations

prod.bifunctor = {bimap := prod.map}

source

@[protected, instance]

def prod.is_lawful_bifunctor :

is_lawful_bifunctor prod

Equations

prod.is_lawful_bifunctor = {id_bimap := prod.is_lawful_bifunctor._proof_1, bimap_bimap := prod.is_lawful_bifunctor._proof_2}

source

@[protected, instance]

def bifunctor.const :

bifunctor functor.const

Equations

bifunctor.const = {bimap := λ (α α' : Type u_1) (β β_1 : Type u_2) (f : α → α') (_x : β → β_1), f}

source

@[protected, instance]

def is_lawful_bifunctor.const :

is_lawful_bifunctor functor.const

Equations

is_lawful_bifunctor.const = {id_bimap := is_lawful_bifunctor.const._proof_1, bimap_bimap := is_lawful_bifunctor.const._proof_2}

source

@[protected, instance]

def bifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] :

bifunctor (flip F)

Equations

bifunctor.flip = {bimap := λ (α α' : Type u₁) (β β' : Type u₀) (f : α → α') (f' : β → β') (x : flip F α β), bimap f' f x}

source

@[protected, instance]

def is_lawful_bifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] :

is_lawful_bifunctor (flip F)

Equations

is_lawful_bifunctor.flip = {id_bimap := _, bimap_bimap := _}

source

@[protected, instance]

def sum.bifunctor :

bifunctor sum

Equations

sum.bifunctor = {bimap := sum.map}

source

@[protected, instance]

def sum.is_lawful_bifunctor :

is_lawful_bifunctor sum

Equations

sum.is_lawful_bifunctor = {id_bimap := sum.is_lawful_bifunctor._proof_1, bimap_bimap := sum.is_lawful_bifunctor._proof_2}

source

@[protected, instance]

def bifunctor.functor {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] {α : Type u₀} :

functor (F α)

Equations

bifunctor.functor = {map := λ (_x _x_1 : Type u₁), bifunctor.snd, map_const := λ (α_1 β : Type u₁), bifunctor.snd ∘ function.const β}

source

@[protected, instance]

def bifunctor.is_lawful_functor {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α : Type u₀} :

is_lawful_functor (F α)

source

@[protected, instance]

def 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

function.bicompl.bifunctor G H = {bimap := λ (α α' : Type u_1) (β β' : Type u_2) (f : α → α') (f' : β → β') (x : function.bicompl F G H α β), bimap (functor.map f) (functor.map f') x}

source

@[protected, instance]

def function.bicompl.is_lawful_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] [is_lawful_functor G] [is_lawful_functor H] [is_lawful_bifunctor F] :

is_lawful_bifunctor (function.bicompl F G H)

Equations

function.bicompl.is_lawful_bifunctor G H = {id_bimap := _, bimap_bimap := _}

source

@[protected, instance]

def 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 := λ (α α' : Type u₀) (β β' : Type u₁) (f : α → α') (f' : β → β') (x : function.bicompr G F α β), bimap f f' <$> x}

source

@[protected, instance]

def function.bicompr.is_lawful_bifunctor {F : Type u₀ → Type u₁ → Type u₂} [bifunctor F] (G : Type u₂ → Type u_1) [functor G] [is_lawful_functor G] [is_lawful_bifunctor F] :

is_lawful_bifunctor (function.bicompr G F)

Equations

function.bicompr.is_lawful_bifunctor G = {id_bimap := _, bimap_bimap := _}