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

References

• Hackage: https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html

Tags

traversable bitraversable functor bifunctor applicative

@[reducible, inline]

abbrev Bitraversable.tfst {t : Type u → Type u → Type u} [Bitraversable t] {β : Type u} {F : Type u → Type u} [Applicative F] {α : Type u} {α' : Type u} (f : α → F α') : t α β → F (t α' β)

traverse on the first functor argument

Equations

• Bitraversable.tfst f = bitraverse f pure

@[reducible, inline]

abbrev Bitraversable.tsnd {t : Type u → Type u → Type u} [Bitraversable t] {β : Type u} {F : Type u → Type u} [Applicative F] {α : Type u} {α' : Type u} (f : α → F α') : t β α → F (t β α')

traverse on the second functor argument

Equations

• Bitraversable.tsnd f = bitraverse pure f

theorem Bitraversable.tfst_id {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {β : Type u} : Bitraversable.tfst pure = pure

theorem Bitraversable.id_tfst {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {β : Type u} (x : t α β) : Bitraversable.tfst pure x = pure x

theorem Bitraversable.tsnd_id {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {β : Type u} : Bitraversable.tsnd pure = pure

theorem Bitraversable.id_tsnd {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {β : Type u} (x : t α β) : Bitraversable.tsnd pure x = pure x

theorem Bitraversable.tfst_comp_tfst {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ : Type u} {α₁ : Type u} {α₂ : Type u} {β : Type u} (f : α₀ → F α₁) (f' : α₁ → G α₂) : Functor.Comp.mk ∘ Functor.map (Bitraversable.tfst f') ∘ Bitraversable.tfst f = Bitraversable.tfst (Functor.Comp.mk ∘ Functor.map f' ∘ f)

theorem Bitraversable.comp_tfst {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ : Type u} {α₁ : Type u} {α₂ : Type u} {β : 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

theorem Bitraversable.tfst_comp_tsnd {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀ → F α₁) (f' : β₀ → G β₁) : Functor.Comp.mk ∘ Functor.map (Bitraversable.tfst f) ∘ Bitraversable.tsnd f' = bitraverse (Functor.Comp.mk ∘ pure ∘ f) (Functor.Comp.mk ∘ Functor.map pure ∘ f')

theorem Bitraversable.tfst_tsnd {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀) : Functor.Comp.mk (Bitraversable.tfst f <$> Bitraversable.tsnd f' x) = 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} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀ → F α₁) (f' : β₀ → G β₁) : Functor.Comp.mk ∘ Functor.map (Bitraversable.tsnd f') ∘ Bitraversable.tfst f = bitraverse (Functor.Comp.mk ∘ Functor.map pure ∘ f) (Functor.Comp.mk ∘ pure ∘ f')

theorem Bitraversable.tsnd_tfst {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ : Type u} {α₁ : Type u} {β₀ : Type u} {β₁ : Type u} (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀) : Functor.Comp.mk (Bitraversable.tsnd f' <$> Bitraversable.tfst f x) = 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} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α : Type u} {β₀ : Type u} {β₁ : Type u} {β₂ : Type u} (g : β₀ → F β₁) (g' : β₁ → G β₂) : Functor.Comp.mk ∘ Functor.map (Bitraversable.tsnd g') ∘ Bitraversable.tsnd g = Bitraversable.tsnd (Functor.Comp.mk ∘ Functor.map g' ∘ g)

theorem Bitraversable.comp_tsnd {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α : Type u} {β₀ : Type u} {β₁ : Type u} {β₂ : 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

theorem Bitraversable.tfst_eq_fst_id' {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {α' : Type u} {β : Type u} (f : α → α') : Bitraversable.tfst (pure ∘ f) = pure ∘ Bifunctor.fst f

theorem Bitraversable.tfst_eq_fst_id {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {α' : Type u} {β : Type u} (f : α → α') (x : t α β) : Bitraversable.tfst (pure ∘ f) x = pure (Bifunctor.fst f x)

theorem Bitraversable.tsnd_eq_snd_id' {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {β : Type u} {β' : Type u} (f : β → β') : Bitraversable.tsnd (pure ∘ f) = pure ∘ Bifunctor.snd f

theorem Bitraversable.tsnd_eq_snd_id {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} {β : Type u} {β' : Type u} (f : β → β') (x : t α β) : Bitraversable.tsnd (pure ∘ f) x = pure (Bifunctor.snd f x)