Theorems · Theorem

Traversable.traverse_comp

∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F G : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] [inst_4 : Applicative G] [LawfulApplicative G] {α β γ : Type u} (g : α → F β) (h : β → G γ),
  traverse (Functor.Comp.mk ∘ Functor.map h ∘ g) = Functor.Comp.mk ∘ Functor.map (traverse h) ∘ traverse g

Defined in

Mathlib.Control.Traversable.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses Quot.sound

Assumes

TraversableLawfulTraversableApplicativeLawfulApplicativeApplicativeLawfulApplicative