# mathlib3documentation

control.bitraversable.basic

# Bitraversable type class #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
• is_lawful_bitraversable: Typeclass for the laws of the bitraverse function. Similar to is_lawful_traversable.

## 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 u Type u Type u) :
Type (u+1)

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_1 Type u_1 Type u_1} {m : Type u_1 Type 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 u Type u Type u)  :
• 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_1 Type l_1 Type l_1} [self : is_lawful_bitraversable t] {α β : Type l_1} :
theorem is_lawful_bitraversable.bitraverse_comp {t : Type l_1 Type l_1 Type l_1} [self : is_lawful_bitraversable t] {F G : Type l_1 Type 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_1 Type l_1 Type l_1} [self : is_lawful_bitraversable t] {F G : Type l_1 Type 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_1 Type l_1 Type l_1} [self : is_lawful_bitraversable t] {α α' β β' : Type l_1} (f : α β) (f' : α' β') :
(id.mk f') =