Hale.Base.Data.Bifunctor

class Data.Bifunctor (F : Type u → Type v → Type w) :

Type (max (max (u + 1) (v + 1)) w)

A bifunctor is a type constructor $F : \mathsf{Type} \to \mathsf{Type} \to \mathsf{Type}$ that is functorial in both arguments. Given morphisms $f : \alpha \to \gamma$ and $g : \beta \to \delta$, we obtain:

$$\text{bimap}\; f\; g : F\;\alpha\;\beta \to F\;\gamma\;\delta$$

bimap {α γ : Type u} {β δ : Type v} : (α → γ) → (β → δ) → F α β → F γ δ
Map over both arguments simultaneously: $\text{bimap}\; f\; g : F\;\alpha\;\beta \to F\;\gamma\;\delta$.
mapFst {α γ : Type u} {β : Type v} : (α → γ) → F α β → F γ β
Map over the first argument only: $\text{mapFst}\; f = \text{bimap}\; f\; \text{id}$.
mapSnd {β δ : Type v} {α : Type u} : (β → δ) → F α β → F α δ
Map over the second argument only: $\text{mapSnd}\; g = \text{bimap}\; \text{id}\; g$.

Instances

source

class Data.LawfulBifunctor (F : Type u → Type v → Type w) [Bifunctor F] :

Prop

Laws that a well-behaved Bifunctor must satisfy:

Identity: $\text{bimap}\;\text{id}\;\text{id} = \text{id}$
Composition: $\text{bimap}\;(f_1 \circ f_2)\;(g_1 \circ g_2) = \text{bimap}\;f_1\;g_1 \circ \text{bimap}\;f_2\;g_2$

bimap_id {α : Type u} {β : Type v} (x : F α β) : Bifunctor.bimap id id x = x
Identity law: $\text{bimap}\;\text{id}\;\text{id}\;x = x$.
bimap_comp {γ δ α : Type u} {ε ζ β : Type v} (f₁ : γ → δ) (f₂ : α → γ) (g₁ : ε → ζ) (g₂ : β → ε) (x : F α β) : Bifunctor.bimap (f₁ ∘ f₂) (g₁ ∘ g₂) x = Bifunctor.bimap f₁ g₁ (Bifunctor.bimap f₂ g₂ x)
Composition law: $\text{bimap}\;(f_1 \circ f_2)\;(g_1 \circ g_2)\;x = \text{bimap}\;f_1\;g_1\;(\text{bimap}\;f_2\;g_2\;x)$.