# mathlibdocumentation

control.bitraversable.instances

# Bitraversable instances #

This file provides bitraversable instances for concrete bifunctors:

• prod
• sum
• functor.const
• flip
• function.bicompl
• function.bicompr

## Tags #

traversable bitraversable functor bifunctor applicative

def prod.bitraverse {F : Type uType u} [applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') :
α × βF (α' × β')

The bitraverse function for α × β.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def sum.bitraverse {F : Type uType u} [applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') :
α βF (α' β')

The bitraverse function for α ⊕ β.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[nolint]
def const.bitraverse {F : Type uType u} [applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') :
F β')

The bitraverse function for const. It throws away the second map.

Equations
• f' = f
@[protected, instance]
Equations
@[protected, instance]
Equations
def flip.bitraverse {t : Type uType uType u} {F : Type uType u} [applicative F] {α α' β β' : Type u} (f : α → F α') (f' : β → F β') :
flip t α βF (flip t α' β')

The bitraverse function for flip.

Equations
• f' =
@[protected, instance]
def bitraversable.flip {t : Type uType uType u}  :
Equations
@[protected, instance]
def is_lawful_bitraversable.flip {t : Type uType uType u}  :
Equations
@[protected, instance]
def bitraversable.traversable {t : Type uType uType u} {α : Type u} :
Equations
@[protected, instance]
def bitraversable.is_lawful_traversable {t : Type uType uType u} {α : Type u} :
Equations
def bicompl.bitraverse {t : Type uType uType u} (F G : Type uType u) [traversable F] [traversable G] {m : Type uType u} [applicative m] {α β α' β' : Type u} (f : α → m β) (f' : α' → m β') :
G α α'm F G β β')

The bitraverse function for bicompl.

Equations
@[protected, instance]
def function.bicompl.bitraversable {t : Type uType uType u} (F G : Type uType u) [traversable F] [traversable G] :
Equations
@[protected, instance]
def function.bicompl.is_lawful_bitraversable {t : Type uType uType u} (F G : Type uType u) [traversable F] [traversable G]  :
Equations
def bicompr.bitraverse {t : Type uType uType u} (F : Type uType u) [traversable F] {m : Type uType u} [applicative m] {α β α' β' : Type u} (f : α → m β) (f' : α' → m β') :
α α'm t β β')

The bitraverse function for bicompr.

Equations
@[protected, instance]
def function.bicompr.bitraversable {t : Type uType uType u} (F : Type uType u) [traversable F] :
Equations
@[protected, instance]
def function.bicompr.is_lawful_bitraversable {t : Type uType uType u} (F : Type uType u) [traversable F]  :
Equations