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 α')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 α')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 α β) :