Theorems · Theorem

LawfulTraversable.naturality

∀ {t : Type u → Type u} {inst : Traversable t} [self : LawfulTraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α),
  (fun {α} => η.app α) (traverse f x) = traverse ((fun {α} => η.app α) ∘ f) x

The naturality axiom explaining how lawful traversable functors should play with lawful applicative functors.

Defined in

Mathlib.Control.Traversable.Basic

Cited by

6 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

LawfulTraversableApplicativeApplicativeLawfulApplicativeLawfulApplicative