Theorems · Inductive type

LawfulTraversable

(t : Type u → Type u) → [Traversable t] → Prop

A traversable functor is lawful if its traverse satisfies a number of additional properties. It must send pure : α → Id α to pure, send the composition of applicative functors to the composition of the traverse of each, send each function f to fun x ↦ f <$> x, and satisfy a naturality condition with respect to applicative transformations.

Defined in

Mathlib.Control.Traversable.Basic

Cited by

37 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Traversable