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

source
class Bifunctor (F : Type u₀ → Type u₁ → Type u₂) :
Type (max (max (u₀ + 1) (u₁ + 1)) u₂)

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

- bimap {α α' : Type u₀} {β β' : Type u₁} : (α → α') → (β → β') → F α β → F α' β'

Instances

source
class LawfulBifunctor (F : Type u₀ → Type u₁ → Type u₂) [Bifunctor F] :
Prop

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

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

Instances

source
theorem LawfulBifunctor.bimap_id_id {F : Type u₀ → Type u₁ → Type u₂} {inst✝ : Bifunctor F} [self : LawfulBifunctor F] {α : Type u₀} {β : Type u₁} :
bimap id id = id
source
theorem LawfulBifunctor.bimap_comp_bimap {F : Type u₀ → Type u₁ → Type u₂} {inst✝ : Bifunctor F} [self : LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) :
bimap f' g' ∘ bimap f g = bimap (f' ∘ f) (g' ∘ g)
source
@[reducible, inline]
abbrev 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

Instances For

source
@[reducible, inline]
abbrev 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

Instances For

source
theorem Bifunctor.id_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) :
fst id x = x
source
theorem Bifunctor.fst_id {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} :
fst id = id
source
theorem Bifunctor.id_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} (x : F α β) :
snd id x = x
source
theorem Bifunctor.snd_id {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁} :
snd id = id
source
theorem Bifunctor.comp_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (x : F α₀ β) :
fst f' (fst f x) = fst (f' ∘ f) x
source
theorem Bifunctor.fst_comp_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) :
fst f' ∘ fst f = fst (f' ∘ f)
source
theorem Bifunctor.fst_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁} (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀) :
fst f (snd f' x) = bimap f f' x
source
theorem Bifunctor.fst_comp_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁} (f : α₀ → α₁) (f' : β₀ → β₁) :
fst f ∘ snd f' = bimap f f'
source
theorem Bifunctor.snd_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁} (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀) :
snd f' (fst f x) = bimap f f' x
source
theorem Bifunctor.snd_comp_fst {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁} (f : α₀ → α₁) (f' : β₀ → β₁) :
snd f' ∘ fst f = bimap f f'
source
theorem Bifunctor.comp_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β₀ β₁ β₂ : Type u₁} (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α β₀) :
snd g' (snd g x) = snd (g' ∘ g) x
source
theorem Bifunctor.snd_comp_snd {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β₀ β₁ β₂ : Type u₁} (g : β₀ → β₁) (g' : β₁ → β₂) :
snd g' ∘ snd g = snd (g' ∘ g)
source
instance Prod.bifunctor :
Bifunctor Prod
Equations

- Prod.bifunctor = { bimap := @Prod.map }

source
instance Prod.lawfulBifunctor :
LawfulBifunctor Prod
source
instance Bifunctor.const :
Bifunctor Functor.Const
Equations

- Bifunctor.const = { bimap := fun {α α' : Type ?u.13} {β β' : Type ?u.12} (f : α → α') (x : β → β') => f }

source
instance LawfulBifunctor.const :
LawfulBifunctor Functor.Const
source
instance Bifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] :
Bifunctor (_root_.flip F)
Equations

- Bifunctor.flip = { bimap := fun {_α α' : Type ?u.25} {_β β' : Type ?u.26} (f : _α → α') (f' : _β → β') (x : flip F _α _β) => bimap f' f x }

source
instance LawfulBifunctor.flip {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] :
LawfulBifunctor (_root_.flip F)
source
instance Sum.bifunctor :
Bifunctor Sum
Equations

- Sum.bifunctor = { bimap := @Sum.map }

source
instance Sum.lawfulBifunctor :
LawfulBifunctor Sum
source
@[instance 10]
instance Bifunctor.functor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] {α : Type u₀} :
Functor (F α)
Equations

- Bifunctor.functor = { map := fun {α_1 β : Type ?u.28} (f : α_1 → β) (x : F α α_1) => Bifunctor.snd f x }

source
@[instance 10]
instance Bifunctor.lawfulFunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] {α : Type u₀} :
LawfulFunctor (F α)
source
instance 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 (bicompl F G H)
Equations

- One or more equations did not get rendered due to their size.

source
instance Function.bicompl.lawfulBifunctor {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] [LawfulFunctor G] [LawfulFunctor H] [LawfulBifunctor F] :
LawfulBifunctor (bicompl F G H)
source
instance Function.bicompr.bifunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u₂ → Type u_1) [Functor G] :
Bifunctor (bicompr G F)
Equations

- Function.bicompr.bifunctor G = { bimap := fun {_α α' : Type ?u.47} {_β β' : Type ?u.46} (f : _α → α') (f' : _β → β') (x : Function.bicompr G F _α _β) => bimap f f' <$> x }

source
instance Function.bicompr.lawfulBifunctor {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u₂ → Type u_1) [Functor G] [LawfulFunctor G] [LawfulBifunctor F] :
LawfulBifunctor (bicompr G F)