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

source

@[class]

structure bitraversable (t : Type u → Type u → Type u) :

Type (u+1)

to_bifunctor : bifunctor t
bitraverse : Π {m : Type ? → Type ?} [_inst_1 : applicative m] {α α' β β' : 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

source

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

bisequence = bitraversable.bitraverse id id

source

@[class]

structure is_lawful_bitraversable (t : Type u → Type u → Type u) [bitraversable t] :

Type

to_is_lawful_bifunctor : is_lawful_bifunctor t
id_bitraverse : ∀ {α β : Type ?} (x : t α β), bitraversable.bitraverse id.mk id.mk x = id.mk x
comp_bitraverse : ∀ {F G : Type ? → Type ?} [_inst_1_1 : applicative F] [_inst_2 : applicative G] [_inst_3 : is_lawful_applicative F] [_inst_4 : is_lawful_applicative G] {α α' β β' γ γ' : Type ?} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'), bitraversable.bitraverse (functor.comp.mk ∘ functor.map f ∘ g) (functor.comp.mk ∘ functor.map f' ∘ g') x = functor.comp.mk (bitraversable.bitraverse f f' <$> bitraversable.bitraverse g g' x)
bitraverse_eq_bimap_id : ∀ {α α' β β' : Type ?} (f : α → β) (f' : α' → β') (x : t α α'), bitraversable.bitraverse (id.mk ∘ f) (id.mk ∘ f') x = id.mk (bifunctor.bimap f f' x)
binaturality : ∀ {F G : Type ? → Type ?} [_inst_1_1 : applicative F] [_inst_2 : applicative G] [_inst_3 : is_lawful_applicative F] [_inst_4 : is_lawful_applicative G] (η : applicative_transformation F G) {α α' β β' : Type ?} (f : α → F β) (f' : α' → F β') (x : t α α'), ⇑η (bitraversable.bitraverse f f' x) = bitraversable.bitraverse (⇑η ∘ f) (⇑η ∘ 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

source

theorem is_lawful_bitraversable.bitraverse_id_id {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] [self : is_lawful_bitraversable t] {α β : Type l_1} :

bitraversable.bitraverse id.mk id.mk = id.mk

source

theorem is_lawful_bitraversable.bitraverse_comp {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] {α α' β β' γ γ' : Type l_1} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') :

bitraversable.bitraverse (functor.comp.mk ∘ functor.map f ∘ g) (functor.comp.mk ∘ functor.map f' ∘ g') = functor.comp.mk ∘ functor.map (bitraversable.bitraverse f f') ∘ bitraversable.bitraverse g g'

source

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 β') :

⇑η ∘ bitraversable.bitraverse f f' = bitraversable.bitraverse (⇑η ∘ f) (⇑η ∘ f')

source

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' : α' → β') :

bitraversable.bitraverse (id.mk ∘ f) (id.mk ∘ f') = id.mk ∘ bifunctor.bimap f f'