mathlib documentation

control.bitraversable.basic

Bitraversable type class

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

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

Tags

traversable bitraversable iterator functor bifunctor applicative

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

Instances
def bisequence {t : Type u_1Type u_1Type u_1} {m : Type u_1Type u_1} [bitraversable t] [applicative m] {α β : Type u_1} :
t (m α) (m β)m (t α β)

Equations
@[class]
structure is_lawful_bitraversable (t : Type uType uType u) [bitraversable t] :
Type

Instances
theorem is_lawful_bitraversable.bitraverse_id_id {t : Type l_1Type l_1Type l_1} [bitraversable t] [c : is_lawful_bitraversable t] {α β : Type l_1} :

theorem is_lawful_bitraversable.bitraverse_comp {t : Type l_1Type l_1Type l_1} [bitraversable t] [c : is_lawful_bitraversable t] {F G : Type l_1Type l_1} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_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} [bitraversable t] [c : is_lawful_bitraversable t] {F G : Type l_1Type 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 β') :
η bitraverse f f' = bitraverse (η f) (η f')

theorem is_lawful_bitraversable.bitraverse_eq_bimap_id' {t : Type l_1Type l_1Type l_1} [bitraversable t] [c : is_lawful_bitraversable t] {α α' β β' : Type l_1} (f : α → β) (f' : α' → β') :