# 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 u → Type u} [] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : αF α') (f' : βF β') :
α × βF (α' × β')

The bitraverse function for α × β.

Equations
Instances For
Equations
def Sum.bitraverse {F : Type u → Type u} [] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : αF α') (f' : βF β') :
α βF (α' β')

The bitraverse function for α ⊕ β.

Equations
Instances For
Equations
Equations
def Const.bitraverse {F : Type u → Type u} [] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : αF α') (f' : βF β') :
F (Functor.Const α' β')

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

Equations
Instances For
Equations
def flip.bitraverse {t : Type u → Type u → Type u} [] {F : Type u → Type u} [] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αF α') (f' : βF β') :
flip t α βF (flip t α' β')

The bitraverse function for flip.

Equations
Instances For
instance Bitraversable.flip {t : Type u → Type u → Type u} [] :
Equations
instance LawfulBitraversable.flip {t : Type u → Type u → Type u} [] :
Equations
• =
@[instance 10]
instance Bitraversable.traversable {t : Type u → Type u → Type u} [] {α : Type u} :
Equations
@[instance 10]
instance Bitraversable.isLawfulTraversable {t : Type u → Type u → Type u} [] {α : Type u} :
Equations
• =
def Bicompl.bitraverse {t : Type u → Type u → Type u} [] (F : Type u → Type u) (G : Type u → Type u) [] [] {m : Type u → Type u} [] {α : Type u} {β : Type u} {α' : Type u} {β' : Type u} (f : αm β) (f' : α'm β') :
Function.bicompl t F G α α'm (Function.bicompl t F G β β')

The bitraverse function for bicompl.

Equations
Instances For
instance instBitraversableBicompl {t : Type u → Type u → Type u} [] (F : Type u → Type u) (G : Type u → Type u) [] [] :
Equations
instance instLawfulBitraversableBicomplOfLawfulTraversable {t : Type u → Type u → Type u} [] (F : Type u → Type u) (G : Type u → Type u) [] [] :
Equations
• =
def Bicompr.bitraverse {t : Type u → Type u → Type u} [] (F : Type u → Type u) [] {m : Type u → Type u} [] {α : Type u} {β : Type u} {α' : Type u} {β' : Type u} (f : αm β) (f' : α'm β') :
Function.bicompr F t α α'm (Function.bicompr F t β β')

The bitraverse function for bicompr.

Equations
Instances For
instance instBitraversableBicompr {t : Type u → Type u → Type u} [] (F : Type u → Type u) [] :
Equations
instance instLawfulBitraversableBicomprOfLawfulTraversable {t : Type u → Type u → Type u} [] (F : Type u → Type u) [] :
Equations
• =