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
Tags
traversable bitraversable functor bifunctor applicative
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 α')
(a : t α β) :
F (t α' β)
traverse on the first functor argument
Equations
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 α')
(a : t β α) :
F (t β α')
traverse on the second functor argument
Equations
theorem
bitraversable.id_tfst
{t : Type u → Type u → Type u}
[bitraversable t]
[is_lawful_bitraversable t]
{α β : Type u}
(x : t α β) :
theorem
bitraversable.tfst_id
{t : Type l_1 → Type l_1 → Type l_1}
[bitraversable t]
[is_lawful_bitraversable t]
{α β : Type l_1} :
theorem
bitraversable.id_tsnd
{t : Type u → Type u → Type u}
[bitraversable t]
[is_lawful_bitraversable t]
{α β : Type u}
(x : t α β) :
theorem
bitraversable.tsnd_id
{t : Type l_1 → Type l_1 → Type l_1}
[bitraversable t]
[is_lawful_bitraversable t]
{α β : Type l_1} :
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 α₂) :
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
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' = 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 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) = bitraverse (functor.comp.mk ∘ pure ∘ f) (functor.comp.mk ∘ functor.map pure ∘ f') x
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 = 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 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) = bitraverse (functor.comp.mk ∘ functor.map pure ∘ f) (functor.comp.mk ∘ pure ∘ f') x
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
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 β₂) :
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
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)
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
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)