Theorems · Theorem

Traversable.naturality_pf

∀ {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}
  (η : ApplicativeTransformation F G) (f : α → F β),
  traverse ((fun {α} => η.app α) ∘ f) = (fun {α} => η.app α) ∘ traverse f

Defined in

Mathlib.Control.Traversable.Lemmas

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses Quot.sound

Assumes

TraversableLawfulTraversableApplicativeLawfulApplicativeApplicativeLawfulApplicative