Theorems · Theorem

Equiv.naturality

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

Defined in

Mathlib.Control.Traversable.Equiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

TraversableLawfulTraversableApplicativeApplicativeLawfulApplicativeLawfulApplicative