Structures · Data types

LawfulTraversable

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

Shape

One type argument · adds id_traverse, comp_traverse, traverse_eq_map_id, naturality