mathlib docs: control.bitraversable.instances

source

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

F (α' × β')

Equations

prod.bitraverse f f' (x, y) = prod.mk <$> f x <*> f' y

source

@[instance]

def prod.bitraversable :

bitraversable prod

Equations

prod.bitraversable = {to_bifunctor := prod.bifunctor, bitraverse := prod.bitraverse}

source

@[instance]

def prod.is_lawful_bitraversable :

is_lawful_bitraversable prod

Equations

prod.is_lawful_bitraversable = {to_is_lawful_bifunctor := prod.is_lawful_bifunctor, id_bitraverse := prod.is_lawful_bitraversable._proof_1, comp_bitraverse := prod.is_lawful_bitraversable._proof_2, bitraverse_eq_bimap_id := prod.is_lawful_bitraversable._proof_3, binaturality := prod.is_lawful_bitraversable._proof_4}

source

def sum.bitraverse {F : Type u → Type u} [applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') (a : α ⊕ β) :

F (α' ⊕ β')

Equations

sum.bitraverse f f' (sum.inr x) = sum.inr <$> f' x
sum.bitraverse f f' (sum.inl x) = sum.inl <$> f x

source

@[instance]

def sum.bitraversable :

bitraversable sum

Equations

sum.bitraversable = {to_bifunctor := sum.bifunctor, bitraverse := sum.bitraverse}

source

@[instance]

def sum.is_lawful_bitraversable :

is_lawful_bitraversable sum

Equations

sum.is_lawful_bitraversable = {to_is_lawful_bifunctor := sum.is_lawful_bifunctor, id_bitraverse := sum.is_lawful_bitraversable._proof_1, comp_bitraverse := sum.is_lawful_bitraversable._proof_2, bitraverse_eq_bimap_id := sum.is_lawful_bitraversable._proof_3, binaturality := sum.is_lawful_bitraversable._proof_4}

source

def const.bitraverse {F : Type u → Type u} [applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') (a : functor.const α β) :

F (functor.const α' β')

Equations

const.bitraverse f f' = f

source

@[instance]

def bitraversable.const :

bitraversable functor.const

Equations

bitraversable.const = {to_bifunctor := bifunctor.const, bitraverse := const.bitraverse}

source

@[instance]

def is_lawful_bitraversable.const :

is_lawful_bitraversable functor.const

Equations

is_lawful_bitraversable.const = {to_is_lawful_bifunctor := is_lawful_bifunctor.const, id_bitraverse := is_lawful_bitraversable.const._proof_1, comp_bitraverse := is_lawful_bitraversable.const._proof_2, bitraverse_eq_bimap_id := is_lawful_bitraversable.const._proof_3, binaturality := is_lawful_bitraversable.const._proof_4}

source

def flip.bitraverse {t : Type u → Type u → Type u} [bitraversable t] {F : Type u → Type u} [applicative F] {α α' β β' : Type u} (f : α → F α') (f' : β → F β') (a : flip t α β) :

F (flip t α' β')

Equations

flip.bitraverse f f' = bitraverse f' f

source

@[instance]

def bitraversable.flip {t : Type u → Type u → Type u} [bitraversable t] :

bitraversable (flip t)

Equations

bitraversable.flip = {to_bifunctor := bifunctor.flip bitraversable.to_bifunctor, bitraverse := flip.bitraverse _inst_1}

source

@[instance]

def is_lawful_bitraversable.flip {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] :

is_lawful_bitraversable (flip t)

Equations

is_lawful_bitraversable.flip = {to_is_lawful_bifunctor := is_lawful_bifunctor.flip is_lawful_bitraversable.to_is_lawful_bifunctor, id_bitraverse := _, comp_bitraverse := _, bitraverse_eq_bimap_id := _, binaturality := _}

source

@[instance]

def bitraversable.traversable {t : Type u → Type u → Type u} [bitraversable t] {α : Type u} :

traversable (t α)

Equations

bitraversable.traversable = {to_functor := bifunctor.functor α, traverse := bitraversable.tsnd α}

source

@[instance]

def bitraversable.is_lawful_traversable {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] {α : Type u} :

is_lawful_traversable (t α)

Equations

bitraversable.is_lawful_traversable = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}

source

def bicompl.bitraverse {t : Type u → Type u → Type u} [bitraversable t] (F G : Type u → Type u) [traversable F] [traversable G] {m : Type u → Type u} [applicative m] {α β α' β' : Type u} (f : α → m β) (f' : α' → m β') (a : function.bicompl t F G α α') :

m (function.bicompl t F G β β')

Equations

bicompl.bitraverse F G f f' = bitraverse (traverse f) (traverse f')

source

@[instance]

def function.bicompl.bitraversable {t : Type u → Type u → Type u} [bitraversable t] (F G : Type u → Type u) [traversable F] [traversable G] :

bitraversable (function.bicompl t F G)

Equations

function.bicompl.bitraversable F G = {to_bifunctor := function.bicompl.bifunctor F G traversable.to_functor, bitraverse := bicompl.bitraverse F G _inst_3}

source

@[instance]

def function.bicompl.is_lawful_bitraversable {t : Type u → Type u → Type u} [bitraversable t] (F G : Type u → Type u) [traversable F] [traversable G] [is_lawful_traversable F] [is_lawful_traversable G] [is_lawful_bitraversable t] :

is_lawful_bitraversable (function.bicompl t F G)

Equations

function.bicompl.is_lawful_bitraversable F G = {to_is_lawful_bifunctor := function.bicompl.is_lawful_bifunctor F G is_lawful_bitraversable.to_is_lawful_bifunctor, id_bitraverse := _, comp_bitraverse := _, bitraverse_eq_bimap_id := _, binaturality := _}

source

def bicompr.bitraverse {t : Type u → Type u → Type u} [bitraversable t] (F : Type u → Type u) [traversable F] {m : Type u → Type u} [applicative m] {α β α' β' : Type u} (f : α → m β) (f' : α' → m β') (a : function.bicompr F t α α') :

m (function.bicompr F t β β')

Equations