mathlib3 documentation

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 #

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} [bitraversable t] [applicative m] {α β : Type u_1} :
t (m α) (m β) m (t α β)

A bitraversable functor commutes with all applicative functors.

Equations
@[class]

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.binaturality' {t : Type l_1 Type l_1 Type l_1} [bitraversable t] [self : is_lawful_bitraversable t] {F G : Type l_1 Type l_1} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] (η : applicative_transformation F G) {α α' β β' : Type l_1} (f : α F β) (f' : α' F β') :
theorem is_lawful_bitraversable.bitraverse_eq_bimap_id' {t : Type l_1 Type l_1 Type l_1} [bitraversable t] [self : is_lawful_bitraversable t] {α α' β β' : Type l_1} (f : α β) (f' : α' β') :