@[class]
- bimap : Π {α α' : Type ?} {β β' : Type ?}, (α → α') → (β → β') → F α β → F α' β'
@[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
def
bifunctor.fst
{F : Type u₀ → Type u₁ → Type u₂}
[bifunctor F]
{α α' : Type u₀}
{β : Type u₁} :
(α → α') → F α β → F α' β
Equations
def
bifunctor.snd
{F : Type u₀ → Type u₁ → Type u₂}
[bifunctor F]
{α : Type u₀}
{β β' : Type u₁} :
(β → β') → F α β → F α β'
Equations
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.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_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.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_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_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_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
@[instance]
Equations
@[instance]
Equations
- prod.is_lawful_bifunctor = {id_bimap := prod.is_lawful_bifunctor._proof_1, bimap_bimap := prod.is_lawful_bifunctor._proof_2}
@[instance]
Equations
- bifunctor.const = {bimap := λ (α α' : Type u_1) (β β_1 : Type u_2) (f : α → α') (_x : β → β_1), f}
@[instance]
Equations
- is_lawful_bifunctor.const = {id_bimap := is_lawful_bifunctor.const._proof_1, bimap_bimap := is_lawful_bifunctor.const._proof_2}
@[instance]
Equations
- bifunctor.flip = {bimap := λ (α α' : Type u₁) (β β' : Type u₀) (f : α → α') (f' : β → β') (x : flip F α β), bifunctor.bimap f' f x}
@[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 := _}
@[instance]
Equations
- sum.is_lawful_bifunctor = {id_bimap := sum.is_lawful_bifunctor._proof_1, bimap_bimap := sum.is_lawful_bifunctor._proof_2}
@[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 β}
@[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 α)
Equations
@[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}
@[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 := _}
@[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}
@[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 := _}