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} (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} (f : α → F α') : t β α → F (t β α')

traverse on the second functor argument

Equations

• Bitraversable.tsnd f = bitraverse pure f

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

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

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

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

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

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

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

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

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

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

theorem Bitraversable.comp_tsnd {t : Type u → Type u → Type u} [Bitraversable t] {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α β₀ β₁ β₂ : Type u} (g : β₀ → F β₁) (g' : β₁ → G β₂) (x : t α β₀) : Functor.Comp.mk (tsnd g' <$> tsnd g x) = tsnd (Functor.Comp.mk ∘ Functor.map g' ∘ g) x

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

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

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

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

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