mathlib documentation

control.bifunctor

@[class]
structure bifunctor  :
(Type u₀Type u₁Type u₂)Type (max (u₀+1) (u₁+1) u₂)
  • bimap : Π {α α' : Type ?} {β β' : Type ?}, (α → α')(β → β')F α βF α' β'

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

Instances
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 α β) :

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

theorem bifunctor.snd_id {F : Type l_3Type l_2Type 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 α β) :

theorem bifunctor.fst_comp_fst {F : Type l_3Type l_2Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ α₂ : Type l_3} {β : Type l_2} (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 α₀ β) :

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 α₀ β₀) :

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

theorem bifunctor.snd_comp_fst {F : Type l_3Type l_2Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ : Type l_3} {β₀ β₁ : Type l_2} (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 α₀ β₀) :

theorem bifunctor.snd_comp_snd {F : Type l_3Type l_2Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α : Type l_3} {β₀ β₁ β₂ : Type l_2} (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 α β₀) :

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
  • bifunctor.const = {bimap := λ (α α' : Type u_1) (β β_1 : Type u_2) (f : α → α') (_x : β → β_1), f}
@[instance]

Equations
@[instance]
def bifunctor.flip {F : Type u₀Type u₁Type u₂} [bifunctor F] :

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

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def bifunctor.functor {F : Type u₀Type u₁Type u₂} [bifunctor F] {α : Type u₀} :
functor (F α)

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

@[instance]
def function.bicompl.bifunctor {F : Type u₀Type u₁Type u₂} [bifunctor F] (G : Type u_1Type u₀) (H : Type u_2Type u₁) [functor G] [functor H] :

Equations
@[instance]
def function.bicompl.is_lawful_bifunctor {F : Type u₀Type u₁Type u₂} [bifunctor F] (G : Type u_1Type u₀) (H : Type u_2Type u₁) [functor G] [functor H] [is_lawful_functor G] [is_lawful_functor H] [is_lawful_bifunctor F] :

Equations
@[instance]
def function.bicompr.bifunctor {F : Type u₀Type u₁Type u₂} [bifunctor F] (G : Type u₂Type u_1) [functor G] :

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