# Documentation

Mathlib.Control.Traversable.Lemmas

# Traversing collections #

This file proves basic properties of traversable and applicative functors and defines PureTransformation F, the natural applicative transformation from the identity functor to F.

## References #

Inspired by [The Essence of the Iterator Pattern][gibbons2009].

def Traversable.PureTransformation (F : Type u → Type u) [inst : ] [inst : ] :

The natural applicative transformation from the identity functor to F, defined by pure : Π {α}, α → F α→ F α.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Traversable.pureTransformation_apply (F : Type u → Type u) [inst : ] [inst : ] {α : Type u} (x : id α) :
(fun {α} => ) α x = pure x
theorem Traversable.map_eq_traverse_id {t : Type u → Type u} [inst : ] [inst : ] {β : Type u} {γ : Type u} (f : βγ) :
= traverse (pure f)
theorem Traversable.map_traverse {t : Type u → Type u} [inst : ] [inst : ] {F : Type u → Type u} [inst : ] [inst : ] {α : Type u} {β : Type u} {γ : Type u} (g : αF β) (f : βγ) (x : t α) :
<$> traverse g x = traverse ( g) x theorem Traversable.traverse_map {t : Type u → Type u} [inst : ] [inst : ] {F : Type u → Type u} [inst : ] [inst : ] {α : Type u} {β : Type u} {γ : Type u} (f : βF γ) (g : αβ) (x : t α) : traverse f (g <$> x) = traverse (f g) x
theorem Traversable.pure_traverse {t : Type u → Type u} [inst : ] [inst : ] {F : Type u → Type u} [inst : ] [inst : ] {α : Type u} (x : t α) :
traverse pure x = pure x
theorem Traversable.id_sequence {t : Type u → Type u} [inst : ] [inst : ] {α : Type u} (x : t α) :
sequence (pure <$> x) = pure x theorem Traversable.comp_sequence {t : Type u → Type u} [inst : ] [inst : ] {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type u} (x : t (F (G α))) : sequence (Functor.Comp.mk <$> x) = Functor.Comp.mk (sequence <$> ) theorem Traversable.naturality' {t : Type u → Type u} [inst : ] [inst : ] {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type u} (η : ) (x : t (F α)) : (fun {α} => ) (t α) () = sequence ((fun {α} => ) α <$> x)
theorem Traversable.traverse_id {t : Type u → Type u} [inst : ] [inst : ] {α : Type u} :
traverse pure = pure
theorem Traversable.traverse_comp {t : Type u → Type u} [inst : ] [inst : ] {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type u} {β : Type u} {γ : Type u} (g : αF β) (h : βG γ) :
traverse (Functor.Comp.mk g) = Functor.Comp.mk
theorem Traversable.traverse_eq_map_id' {t : Type u → Type u} [inst : ] [inst : ] {β : Type u} {γ : Type u} (f : βγ) :
traverse (pure f) = pure
theorem Traversable.traverse_map' {t : Type u → Type u} [inst : ] [inst : ] {G : Type u → Type u} [inst : ] [inst : ] {α : Type u} {β : Type u} {γ : Type u} (g : αβ) (h : βG γ) :
traverse (h g) =
theorem Traversable.map_traverse' {t : Type u → Type u} [inst : ] [inst : ] {G : Type u → Type u} [inst : ] [inst : ] {α : Type u} {β : Type u} {γ : Type u} (g : αG β) (h : βγ) :
traverse ( g) =
theorem Traversable.naturality_pf {t : Type u → Type u} [inst : ] [inst : ] {F : Type u → Type u} {G : Type u → Type u} [inst : ] [inst : ] [inst : ] [inst : ] {α : Type u} {β : Type u} (η : ) (f : αF β) :
traverse ((fun {α} => ) β f) = (fun {α} => ) (t β)