# Bitraversable Lemmas #

## Main definitions #

• tfst - traverse on first functor argument
• tsnd - traverse on second functor argument

## Lemmas #

Combination of

• bitraverse
• tfst
• tsnd

with the applicatives id and comp

• Hackage:

## Tags #

traversable bitraversable functor bifunctor applicative

@[reducible]
def Bitraversable.tfst {t : Type u → Type u → Type u} [] {β : Type u} {F : Type u → Type u} [] {α : Type u} {α' : Type u} (f : αF α') :
t α βF (t α' β)

traverse on the first functor argument

Equations
Instances For
@[reducible]
def Bitraversable.tsnd {t : Type u → Type u → Type u} [] {β : Type u} {F : Type u → Type u} [] {α : Type u} {α' : Type u} (f : αF α') :
t β αF (t β α')

traverse on the second functor argument

Equations
Instances For
theorem Bitraversable.tfst_id {t : Type u → Type u → Type u} [] {α : Type u} {β : Type u} :
= pure
theorem Bitraversable.id_tfst {t : Type u → Type u → Type u} [] {α : Type u} {β : Type u} (x : t α β) :
theorem Bitraversable.tsnd_id {t : Type u → Type u → Type u} [] {α : Type u} {β : Type u} :
= pure
theorem Bitraversable.id_tsnd {t : Type u → Type u → Type u} [] {α : Type u} {β : Type u} (x : t α β) :
theorem Bitraversable.tfst_comp_tfst {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α₀ : Type u} {α₁ : Type u} {α₂ : Type u} {β : Type u} (f : α₀F α₁) (f' : α₁G α₂) :
Functor.Comp.mk = Bitraversable.tfst (Functor.Comp.mk f)
theorem Bitraversable.comp_tfst {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α₀ : Type u} {α₁ : Type u} {α₂ : Type u} {β : Type u} (f : α₀F α₁) (f' : α₁G α₂) (x : t α₀ β) :
= Bitraversable.tfst (Functor.Comp.mk f) x
theorem Bitraversable.tfst_comp_tsnd {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀F α₁) (f' : β₀G β₁) :
Functor.Comp.mk = bitraverse (Functor.Comp.mk pure f) (Functor.Comp.mk Functor.map pure f')
theorem Bitraversable.tfst_tsnd {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀F α₁) (f' : β₀G β₁) (x : t α₀ β₀) :
= bitraverse (Functor.Comp.mk pure f) (Functor.Comp.mk Functor.map pure f') x
theorem Bitraversable.tsnd_comp_tfst {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀F α₁) (f' : β₀G β₁) :
Functor.Comp.mk = bitraverse (Functor.Comp.mk Functor.map pure f) (Functor.Comp.mk pure f')
theorem Bitraversable.tsnd_tfst {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀F α₁) (f' : β₀G β₁) (x : t α₀ β₀) :
= bitraverse (Functor.Comp.mk Functor.map pure f) (Functor.Comp.mk pure f') x
theorem Bitraversable.tsnd_comp_tsnd {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α : Type u} {β₀ : Type u} {β₁ : Type u} {β₂ : Type u} (g : β₀F β₁) (g' : β₁G β₂) :
Functor.Comp.mk = Bitraversable.tsnd (Functor.Comp.mk g)
theorem Bitraversable.comp_tsnd {t : Type u → Type u → Type u} [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α : Type u} {β₀ : Type u} {β₁ : Type u} {β₂ : Type u} (g : β₀F β₁) (g' : β₁G β₂) (x : t α β₀) :
= Bitraversable.tsnd (Functor.Comp.mk g) x
theorem Bitraversable.tfst_eq_fst_id' {t : Type u → Type u → Type u} [] {α : Type u} {α' : Type u} {β : Type u} (f : αα') :
Bitraversable.tfst (pure f) = pure
theorem Bitraversable.tfst_eq_fst_id {t : Type u → Type u → Type u} [] {α : Type u} {α' : Type u} {β : Type u} (f : αα') (x : t α β) :
theorem Bitraversable.tsnd_eq_snd_id' {t : Type u → Type u → Type u} [] {α : Type u} {β : Type u} {β' : Type u} (f : ββ') :
Bitraversable.tsnd (pure f) = pure
theorem Bitraversable.tsnd_eq_snd_id {t : Type u → Type u → Type u} [] {α : Type u} {β : Type u} {β' : Type u} (f : ββ') (x : t α β) :