Theorems · Theorem

Traversable.map_traverse

∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] {α β γ : Type u} (g : α → F β) (f : β → γ) (x : t α),
  Functor.map f <$> traverse g x = traverse (Functor.map f ∘ g) x

Defined in

Mathlib.Control.Traversable.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

TraversableLawfulTraversableApplicativeLawfulApplicative