Theorems · Theorem · combinatorics

List.Vector.naturality

∀ {n : ℕ} {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G]
  [LawfulApplicative F] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : List.Vector α n),
  (fun {α} => η.app α) (List.Vector.traverse f x) = List.Vector.traverse ((fun {α} => η.app α) ∘ f) x

Defined in

Mathlib.Data.Vector.Basic

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

ApplicativeApplicativeLawfulApplicativeLawfulApplicative