mathlib3 documentation

control.bitraversable.lemmas

Bitraversable Lemmas #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Lemmas #

Combination of

with the applicatives id and comp

References #

Tags #

traversable bitraversable functor bifunctor applicative

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

traverse on the first functor argument

Equations
@[reducible]
def bitraversable.tsnd {t : Type u Type u Type u} [bitraversable t] {β : Type u} {F : Type u Type u} [applicative F] {α α' : Type u} (f : α F α') :
t β α F (t β α')

traverse on the second functor argument

Equations
theorem bitraversable.id_tfst {t : Type u Type u Type u} [bitraversable t] [is_lawful_bitraversable t] {α β : Type u} (x : t α β) :
theorem bitraversable.id_tsnd {t : Type u Type u Type u} [bitraversable t] [is_lawful_bitraversable t] {α β : Type u} (x : t α β) :
theorem bitraversable.comp_tfst {t : Type u Type u Type u} [bitraversable t] {F G : Type u Type u} [applicative F] [applicative G] [is_lawful_bitraversable t] [is_lawful_applicative F] [is_lawful_applicative G] {α₀ α₁ α₂ β : Type u} (f : α₀ F α₁) (f' : α₁ G α₂) (x : t α₀ β) :
theorem bitraversable.comp_tsnd {t : Type u Type u Type u} [bitraversable t] {F G : Type u Type u} [applicative F] [applicative G] [is_lawful_bitraversable t] [is_lawful_applicative F] [is_lawful_applicative G] {α β₀ β₁ β₂ : Type u} (g : β₀ F β₁) (g' : β₁ G β₂) (x : t α β₀) :
theorem bitraversable.tfst_eq_fst_id {t : Type u Type u Type u} [bitraversable t] [is_lawful_bitraversable t] {α α' β : Type u} (f : α α') (x : t α β) :
theorem bitraversable.tsnd_eq_snd_id {t : Type u Type u Type u} [bitraversable t] [is_lawful_bitraversable t] {α β β' : Type u} (f : β β') (x : t α β) :