# mathlibdocumentation

control.bitraversable.basic

# 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')

## References #

The concepts and laws are taken from https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html

## Tags #

traversable bitraversable iterator functor bifunctor applicative

@[class]
structure bitraversable (t : Type uType uType u) :
Type (u+1)
• to_bifunctor :
• bitraverse : Π {m : Type ?Type ?} [_inst_1 : {α α' β β' : Type ?}, (α → m α')(β → m β')t α βm (t α' β')

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

Instances of this typeclass
Instances of other typeclasses for bitraversable
• bitraversable.has_sizeof_inst
def bisequence {t : Type u_1Type u_1Type u_1} {m : Type u_1Type u_1} [applicative m] {α β : Type u_1} :
t (m α) (m β)m (t α β)

A bitraversable functor commutes with all applicative functors.

Equations
@[class]
structure is_lawful_bitraversable (t : Type uType uType u)  :
Type
• to_is_lawful_bifunctor :
• id_bitraverse : ∀ {α β : Type ?} (x : t α β),
• comp_bitraverse : ∀ {F G : Type ?Type ?} [_inst_1_1 : [_inst_2 : [_inst_3 : [_inst_4 : {α α' β β' γ γ' : Type ?} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'), (functor.comp.mk g') x =
• bitraverse_eq_bimap_id : ∀ {α α' β β' : Type ?} (f : α → β) (f' : α' → β') (x : t α α'), (id.mk f') x = id.mk f' x)
• binaturality : ∀ {F G : Type ?Type ?} [_inst_1_1 : [_inst_2 : [_inst_3 : [_inst_4 : (η : {α α' β β' : Type ?} (f : α → F β) (f' : α' → F β') (x : t α α'), η x) = (η f') x

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

Instances of this typeclass
Instances of other typeclasses for is_lawful_bitraversable
• is_lawful_bitraversable.has_sizeof_inst
theorem is_lawful_bitraversable.bitraverse_id_id {t : Type l_1Type l_1Type l_1} [self : is_lawful_bitraversable t] {α β : Type l_1} :
theorem is_lawful_bitraversable.bitraverse_comp {t : Type l_1Type l_1Type l_1} [self : is_lawful_bitraversable t] {F G : Type l_1Type l_1} [applicative F] [applicative G] {α α' β β' γ γ' : Type l_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') :
theorem is_lawful_bitraversable.binaturality' {t : Type l_1Type l_1Type l_1} [self : is_lawful_bitraversable t] {F G : Type l_1Type l_1} [applicative F] [applicative G] (η : G) {α α' β β' : Type l_1} (f : α → F β) (f' : α' → F β') :
= (η f')
theorem is_lawful_bitraversable.bitraverse_eq_bimap_id' {t : Type l_1Type l_1Type l_1} [self : is_lawful_bitraversable t] {α α' β β' : Type l_1} (f : α → β) (f' : α' → β') :
(id.mk f') =