# Bitraversable type class #

Type class for traversing bifunctors.

Simple examples of Bitraversable are Prod and Sum. A more elaborate example is to define an a-list as:

def AList (key val : Type) := List (key × val)


Then we can use f : key → IO key' and g : val → IO val' to manipulate the AList's key and value respectively with Bitraverse f g : AList key val → IO (AList key' val').

## Main definitions #

• Bitraversable: Bare typeclass to hold the Bitraverse function.
• LawfulBitraversable: Typeclass for the laws of the Bitraverse function. Similar to LawfulTraversable.

## References #

The concepts and laws are taken from

## Tags #

traversable bitraversable iterator functor bifunctor applicative

class Bitraversable (t : Type u → Type u → Type u) extends :
Type (u + 1)

Lawless bitraversable bifunctor. This only holds data for the bimap and bitraverse.

• bimap : {α α' β β' : Type u} → (αα')(ββ')t α βt α' β'
• bitraverse : {m : Type u → Type u} → [inst : ] → {α α' β β' : Type u} → (αm α')(βm β')t α βm (t α' β')
Instances
def bisequence {t : Type u_1 → Type u_1 → Type u_1} {m : Type u_1 → Type u_1} [] [] {α : Type u_1} {β : Type u_1} :
t (m α) (m β)m (t α β)

A bitraversable functor commutes with all applicative functors.

Equations
Instances For
class LawfulBitraversable (t : Type u → Type u → Type u) [] extends :

Bifunctor. This typeclass asserts that a lawless bitraversable bifunctor is lawful.

• id_bimap : ∀ {α β : Type u} (x : t α β), bimap id id x = x
• bimap_bimap : ∀ {α₀ α₁ α₂ β₀ β₁ β₂ : Type u} (f : α₀α₁) (f' : α₁α₂) (g : β₀β₁) (g' : β₁β₂) (x : t α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' f) (g' g) x
• id_bitraverse : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
• comp_bitraverse : ∀ {F G : Type u → Type u} [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : ] {α α' β β' γ γ' : Type u} (f : βF γ) (f' : β'F γ') (g : αG β) (g' : α'G β') (x : t α α'), bitraverse (Functor.Comp.mk g) (Functor.Comp.mk g') x = Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x) • bitraverse_eq_bimap_id : ∀ {α α' β β' : Type u} (f : αβ) (f' : α'β') (x : t α α'), bitraverse (pure f) (pure f') x = pure (bimap f f' x) • binaturality : ∀ {F G : Type u → Type u} [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : ] (η : ) {α α' β β' : Type u} (f : αF β) (f' : α'F β') (x : t α α'), (fun {α : Type u} => η.app α) (bitraverse f f' x) = bitraverse ((fun {α : Type u} => η.app α) f) ((fun {α : Type u} => η.app α) f') x Instances theorem LawfulBitraversable.id_bitraverse {t : Type u → Type u → Type u} [] [self : ] {α : Type u} {β : Type u} (x : t α β) : bitraverse pure pure x = pure x theorem LawfulBitraversable.comp_bitraverse {t : Type u → Type u → Type u} [] [self : ] {F : Type u → Type u} {G : Type u → Type u} [] [] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} {γ : Type u} {γ' : Type u} (f : βF γ) (f' : β'F γ') (g : αG β) (g' : α'G β') (x : t α α') : bitraverse (Functor.Comp.mk g) (Functor.Comp.mk g') x = Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)
theorem LawfulBitraversable.bitraverse_eq_bimap_id {t : Type u → Type u → Type u} [] [self : ] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αβ) (f' : α'β') (x : t α α') :
bitraverse (pure f) (pure f') x = pure (bimap f f' x)
theorem LawfulBitraversable.binaturality {t : Type u → Type u → Type u} [] [self : ] {F : Type u → Type u} {G : Type u → Type u} [] [] (η : ) {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αF β) (f' : α'F β') (x : t α α') :
(fun {α : Type u} => η.app α) (bitraverse f f' x) = bitraverse ((fun {α : Type u} => η.app α) f) ((fun {α : Type u} => η.app α) f') x
theorem LawfulBitraversable.bitraverse_id_id {t : Type u → Type u → Type u} [] [self : ] {α : Type u} {β : Type u} :
bitraverse pure pure = pure
theorem LawfulBitraversable.bitraverse_comp {t : Type u → Type u → Type u} [] [self : ] {F : Type u → Type u} {G : Type u → Type u} [] [] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} {γ : Type u} {γ' : Type u} (f : βF γ) (f' : β'F γ') (g : αG β) (g' : α'G β') :
bitraverse (Functor.Comp.mk g) (Functor.Comp.mk g') = Functor.Comp.mk Functor.map (bitraverse f f') bitraverse g g'
theorem LawfulBitraversable.binaturality' {t : Type u → Type u → Type u} [] [self : ] {F : Type u → Type u} {G : Type u → Type u} [] [] (η : ) {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αF β) (f' : α'F β') :
(fun {α : Type u} => η.app α) bitraverse f f' = bitraverse ((fun {α : Type u} => η.app α) f) ((fun {α : Type u} => η.app α) f')
theorem LawfulBitraversable.bitraverse_eq_bimap_id' {t : Type u → Type u → Type u} [] [self : ] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αβ) (f' : α'β') :
bitraverse (pure f) (pure f') = pure bimap f f'