mathlib documentation

control.bitraversable.lemmas

Bitraversable Lemmas #

Main definitions #

Lemmas #

Combination of

with the applicatives id and comp

References #

Tags #

traversable bitraversable functor bifunctor applicative

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

traverse on the first functor argument

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

traverse on the second functor argument

Equations
theorem bitraversable.id_tfst {t : Type uType uType u} [bitraversable t] [is_lawful_bitraversable t] {α β : Type u} (x : t α β) :
theorem bitraversable.tfst_id {t : Type l_1Type l_1Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α β : Type l_1} :
theorem bitraversable.id_tsnd {t : Type uType uType u} [bitraversable t] [is_lawful_bitraversable t] {α β : Type u} (x : t α β) :
theorem bitraversable.tsnd_id {t : Type l_1Type l_1Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α β : Type l_1} :
theorem bitraversable.tfst_comp_tfst {t : Type l_1Type l_1Type l_1} [bitraversable t] {F G : Type l_1Type l_1} [applicative F] [applicative G] [is_lawful_bitraversable t] [is_lawful_applicative F] [is_lawful_applicative G] {α₀ α₁ α₂ β : Type l_1} (f : α₀ → F α₁) (f' : α₁ → G α₂) :
theorem bitraversable.comp_tfst {t : Type uType uType u} [bitraversable t] {F G : Type uType 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.tfst_comp_tsnd {t : Type l_1Type l_1Type l_1} [bitraversable t] {F G : Type l_1Type l_1} [applicative F] [applicative G] [is_lawful_bitraversable t] [is_lawful_applicative F] [is_lawful_applicative G] {α₀ α₁ β₀ β₁ : Type l_1} (f : α₀ → F α₁) (f' : β₀ → G β₁) :
theorem bitraversable.tfst_tsnd {t : Type uType uType u} [bitraversable t] {F G : Type uType 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.tsnd_comp_tfst {t : Type l_1Type l_1Type l_1} [bitraversable t] {F G : Type l_1Type l_1} [applicative F] [applicative G] [is_lawful_bitraversable t] [is_lawful_applicative F] [is_lawful_applicative G] {α₀ α₁ β₀ β₁ : Type l_1} (f : α₀ → F α₁) (f' : β₀ → G β₁) :
theorem bitraversable.tsnd_tfst {t : Type uType uType u} [bitraversable t] {F G : Type uType 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 uType uType u} [bitraversable t] {F G : Type uType 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.tsnd_comp_tsnd {t : Type l_1Type l_1Type l_1} [bitraversable t] {F G : Type l_1Type l_1} [applicative F] [applicative G] [is_lawful_bitraversable t] [is_lawful_applicative F] [is_lawful_applicative G] {α β₀ β₁ β₂ : Type l_1} (g : β₀ → F β₁) (g' : β₁ → G β₂) :
theorem bitraversable.tfst_eq_fst_id' {t : Type l_1Type l_1Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α α' β : Type l_1} (f : α → α') :
theorem bitraversable.tfst_eq_fst_id {t : Type uType uType u} [bitraversable t] [is_lawful_bitraversable t] {α α' β : Type u} (f : α → α') (x : t α β) :
theorem bitraversable.tsnd_eq_snd_id' {t : Type l_1Type l_1Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α β β' : Type l_1} (f : β → β') :
theorem bitraversable.tsnd_eq_snd_id {t : Type uType uType u} [bitraversable t] [is_lawful_bitraversable t] {α β β' : Type u} (f : β → β') (x : t α β) :