bitraversable instances
Instances
- prod
- sum
- const
- flip
- bicompl
- bicompr
References
Tags
traversable bitraversable functor bifunctor applicative
def
prod.bitraverse
{F : Type u → Type u}
[applicative F]
{α : Type u_1}
{α' : Type u}
{β : Type u_2}
{β' : Type u} :
Equations
- prod.bitraverse f f' (x, y) = prod.mk <$> f x <*> f' y
@[instance]
Equations
@[instance]
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}
def
sum.bitraverse
{F : Type u → Type u}
[applicative F]
{α : Type u_1}
{α' : Type u}
{β : Type u_2}
{β' : Type u} :
Equations
- sum.bitraverse f f' (sum.inr x) = sum.inr <$> f' x
- sum.bitraverse f f' (sum.inl x) = sum.inl <$> f x
@[instance]
Equations
@[instance]
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}
def
const.bitraverse
{F : Type u → Type u}
[applicative F]
{α : Type u_1}
{α' : Type u}
{β : Type u_2}
{β' : Type u} :
(α → F α') → (β → F β') → functor.const α β → F (functor.const α' β')
Equations
- const.bitraverse f f' = f
@[instance]
Equations
@[instance]
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}
def
flip.bitraverse
{t : Type u → Type u → Type u}
[bitraversable t]
{F : Type u → Type u}
[applicative F]
{α α' β β' : Type u} :
Equations
- flip.bitraverse f f' = bitraversable.bitraverse f' f
@[instance]
Equations
@[instance]
def
is_lawful_bitraversable.flip
{t : Type u → Type u → Type u}
[bitraversable t]
[is_lawful_bitraversable t] :
Equations
@[instance]
def
bitraversable.traversable
{t : Type u → Type u → Type u}
[bitraversable t]
{α : Type u} :
traversable (t α)
Equations
@[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 := _}
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} :
(α → m β) → (α' → m β') → function.bicompl t F G α α' → m (function.bicompl t F G β β')
Equations
- bicompl.bitraverse F G f f' = bitraversable.bitraverse (traversable.traverse f) (traversable.traverse f')
@[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}
@[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] :
Equations
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} :
(α → m β) → (α' → m β') → function.bicompr F t α α' → m (function.bicompr F t β β')
Equations
- bicompr.bitraverse F f f' = traversable.traverse (bitraversable.bitraverse f f')
@[instance]
def
function.bicompr.bitraversable
{t : Type u → Type u → Type u}
[bitraversable t]
(F : Type u → Type u)
[traversable F] :
Equations
@[instance]
def
function.bicompr.is_lawful_bitraversable
{t : Type u → Type u → Type u}
[bitraversable t]
(F : Type u → Type u)
[traversable F]
[is_lawful_traversable F]
[is_lawful_bitraversable t] :