Functors with two arguments #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[class]
Lawless bifunctor. This typeclass only holds the data for the bimap.
Instances of this typeclass
Instances of other typeclasses for bifunctor
- bifunctor.has_sizeof_inst
@[class]
- id_bimap : ∀ {α : Type ?} {β : Type ?} (x : F α β), bifunctor.bimap id id x = x
- bimap_bimap : ∀ {α₀ α₁ α₂ : Type ?} {β₀ β₁ β₂ : Type ?} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α₀ β₀), bifunctor.bimap f' g' (bifunctor.bimap f g x) = bifunctor.bimap (f' ∘ f) (g' ∘ g) x
Bifunctor. This typeclass asserts that a lawless bifunctor is lawful.
Instances of this typeclass
Instances of other typeclasses for is_lawful_bifunctor
- is_lawful_bifunctor.has_sizeof_inst
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' : β₁ → β₂) :
bifunctor.bimap f' g' ∘ bifunctor.bimap f g = bifunctor.bimap (f' ∘ f) (g' ∘ g)
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
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} :
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} :
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
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)
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
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) = bifunctor.bimap f f' x
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' = bifunctor.bimap f f'
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 = bifunctor.bimap f f'
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) = bifunctor.bimap f f' x
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)
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
@[protected, instance]
Equations
@[protected, instance]
Equations
- prod.is_lawful_bifunctor = {id_bimap := prod.is_lawful_bifunctor._proof_1, bimap_bimap := prod.is_lawful_bifunctor._proof_2}
@[protected, instance]
@[protected, instance]
Equations
- is_lawful_bifunctor.const = {id_bimap := is_lawful_bifunctor.const._proof_1, bimap_bimap := is_lawful_bifunctor.const._proof_2}
@[protected, instance]
def
is_lawful_bifunctor.flip
{F : Type u₀ → Type u₁ → Type u₂}
[bifunctor F]
[is_lawful_bifunctor F] :
Equations
- is_lawful_bifunctor.flip = {id_bimap := _, bimap_bimap := _}
@[protected, instance]
Equations
- sum.bifunctor = {bimap := sum.map}
@[protected, instance]
Equations
- sum.is_lawful_bifunctor = {id_bimap := sum.is_lawful_bifunctor._proof_1, bimap_bimap := sum.is_lawful_bifunctor._proof_2}
@[protected, instance]
Equations
- bifunctor.functor = {map := λ (_x _x_1 : Type u₁), bifunctor.snd, map_const := λ (α_1 β : Type u₁), bifunctor.snd ∘ function.const β}
@[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 α)
@[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 α β), bifunctor.bimap (functor.map f) (functor.map f') x}
@[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 := _}
@[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 α β), bifunctor.bimap f f' <$> x}
@[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] :
Equations
- function.bicompr.is_lawful_bifunctor G = {id_bimap := _, bimap_bimap := _}