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

source
@[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
source
@[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
source
theorem bitraversable.id_tfst {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] {α β : Type u} (x : t α β) :
bitraversable.tfst id.mk x = id.mk x
source
theorem bitraversable.tfst_id {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α β : Type l_1} :
bitraversable.tfst id.mk = id.mk
source
theorem bitraversable.id_tsnd {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] {α β : Type u} (x : t α β) :
bitraversable.tsnd id.mk x = id.mk x
source
theorem bitraversable.tsnd_id {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α β : Type l_1} :
bitraversable.tsnd id.mk = id.mk
source
theorem bitraversable.tfst_comp_tfst {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] {F G : Type l_1 → Type 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 α₂) :
functor.comp.mk ∘ functor.map (bitraversable.tfst f') ∘ bitraversable.tfst f = bitraversable.tfst (functor.comp.mk ∘ functor.map f' ∘ f)
source
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 α₀ β) :
functor.comp.mk (bitraversable.tfst f' <$> bitraversable.tfst f x) = bitraversable.tfst (functor.comp.mk ∘ functor.map f' ∘ f) x
source
theorem bitraversable.tfst_comp_tsnd {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] {F G : Type l_1 → Type 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 β₁) :
functor.comp.mk ∘ functor.map (bitraversable.tfst f) ∘ bitraversable.tsnd f' = bitraversable.bitraverse (functor.comp.mk ∘ has_pure.pure ∘ f) (functor.comp.mk ∘ functor.map has_pure.pure ∘ f')
source
theorem bitraversable.tfst_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} (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀) :
functor.comp.mk (bitraversable.tfst f <$> bitraversable.tsnd f' x) = bitraversable.bitraverse (functor.comp.mk ∘ has_pure.pure ∘ f) (functor.comp.mk ∘ functor.map has_pure.pure ∘ f') x
source
theorem bitraversable.tsnd_comp_tfst {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] {F G : Type l_1 → Type 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 β₁) :
functor.comp.mk ∘ functor.map (bitraversable.tsnd f') ∘ bitraversable.tfst f = bitraversable.bitraverse (functor.comp.mk ∘ functor.map has_pure.pure ∘ f) (functor.comp.mk ∘ has_pure.pure ∘ f')
source
theorem bitraversable.tsnd_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 α₀ β₀) :
functor.comp.mk (bitraversable.tsnd f' <$> bitraversable.tfst f x) = bitraversable.bitraverse (functor.comp.mk ∘ functor.map has_pure.pure ∘ f) (functor.comp.mk ∘ has_pure.pure ∘ f') x
source
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 α β₀) :
functor.comp.mk (bitraversable.tsnd g' <$> bitraversable.tsnd g x) = bitraversable.tsnd (functor.comp.mk ∘ functor.map g' ∘ g) x
source
theorem bitraversable.tsnd_comp_tsnd {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] {F G : Type l_1 → Type 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 β₂) :
functor.comp.mk ∘ functor.map (bitraversable.tsnd g') ∘ bitraversable.tsnd g = bitraversable.tsnd (functor.comp.mk ∘ functor.map g' ∘ g)
source
theorem bitraversable.tfst_eq_fst_id' {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α α' β : Type l_1} (f : α → α') :
bitraversable.tfst (id.mk ∘ f) = id.mk ∘ bifunctor.fst f
source
theorem bitraversable.tfst_eq_fst_id {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] {α α' β : Type u} (f : α → α') (x : t α β) :
bitraversable.tfst (id.mk ∘ f) x = id.mk (bifunctor.fst f x)
source
theorem bitraversable.tsnd_eq_snd_id' {t : Type l_1 → Type l_1 → Type l_1} [bitraversable t] [is_lawful_bitraversable t] {α β β' : Type l_1} (f : β → β') :
bitraversable.tsnd (id.mk ∘ f) = id.mk ∘ bifunctor.snd f
source
theorem bitraversable.tsnd_eq_snd_id {t : Type u → Type u → Type u} [bitraversable t] [is_lawful_bitraversable t] {α β β' : Type u} (f : β → β') (x : t α β) :
bitraversable.tsnd (id.mk ∘ f) x = id.mk (bifunctor.snd f x)