Theorems · Inductive type

Traversable

(Type u → Type u) → Type (u + 1)

A traversable functor is a functor along with a way to commute with all applicative functors (see sequence). For example, if t is the traversable functor List and m is the applicative functor IO, then given a function f : α → IO β, the function Functor.map f is List α → List (IO β), but traverse f is List α → IO (List β).

Defined in

Mathlib.Control.Traversable.Basic

Cited by

38 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms