mathlib3 documentation

control.bifunctor

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

Main declarations #

@[class]
structure bifunctor (F : Type u₀ Type u₁ Type u₂) :
Type (max (u₀+1) (u₁+1) u₂)

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]
structure is_lawful_bifunctor (F : Type u₀ Type u₁ Type u₂) [bifunctor F] :

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_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} :
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' : β₁ β₂) :
@[reducible]
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
@[reducible]
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
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_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 α β) :
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' : α₁ α₂) :
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_3 Type l_2 Type l_1} [bifunctor F] [is_lawful_bifunctor F] {α₀ α₁ : Type l_3} {β₀ β₁ : Type l_2} (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' : β₀ β₁) :
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_3 Type l_2 Type 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 α β₀) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def bifunctor.flip {F : Type u₀ Type u₁ Type u₂} [bifunctor F] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def bifunctor.functor {F : Type u₀ Type u₁ Type u₂} [bifunctor F] {α : Type u₀} :
functor (F α)
Equations
@[protected, instance]
def bifunctor.is_lawful_functor {F : Type u₀ Type u₁ Type u₂} [bifunctor F] [is_lawful_bifunctor F] {α : Type u₀} :
@[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] :
Equations
@[protected, instance]
def function.bicompr.bifunctor {F : Type u₀ Type u₁ Type u₂} [bifunctor F] (G : Type u₂ Type u_1) [functor G] :
Equations