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.

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

Equations
Instances For
    @[simp]
    theorem Traversable.pureTransformation_apply (F : Type u → Type u) [Applicative F] [LawfulApplicative F] {α : Type u} (x : id α) :
    (fun {α : Type u} => (Traversable.PureTransformation F).app α) x = pure x
    theorem Traversable.map_eq_traverse_id {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {β : Type u} {γ : Type u} (f : βγ) :
    theorem Traversable.map_traverse {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} [Applicative F] [LawfulApplicative F] {α : Type u} {β : Type u} {γ : Type u} (g : αF β) (f : βγ) (x : t α) :
    theorem Traversable.traverse_map {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} [Applicative F] [LawfulApplicative F] {α : 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} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} [Applicative F] [LawfulApplicative F] {α : Type u} (x : t α) :
    traverse pure x = pure x
    theorem Traversable.id_sequence {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {α : Type u} (x : t α) :
    sequence (pure <$> x) = pure x
    theorem Traversable.comp_sequence {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [LawfulApplicative F] [Applicative G] [LawfulApplicative G] {α : Type u} (x : t (F (G α))) :
    sequence (Functor.Comp.mk <$> x) = Functor.Comp.mk (sequence <$> sequence x)
    theorem Traversable.naturality' {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [LawfulApplicative F] [Applicative G] [LawfulApplicative G] {α : Type u} (η : ApplicativeTransformation F G) (x : t (F α)) :
    (fun {α : Type u} => η.app α) (sequence x) = sequence ((fun {α : Type u} => η.app α) <$> x)
    theorem Traversable.traverse_id {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {α : Type u} :
    traverse pure = pure
    theorem Traversable.traverse_comp {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [LawfulApplicative F] [Applicative G] [LawfulApplicative G] {α : Type u} {β : Type u} {γ : Type u} (g : αF β) (h : βG γ) :
    traverse (Functor.Comp.mk Functor.map h g) = Functor.Comp.mk Functor.map (traverse h) traverse g
    theorem Traversable.traverse_eq_map_id' {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {β : Type u} {γ : Type u} (f : βγ) :
    traverse (pure f) = pure Functor.map f
    theorem Traversable.traverse_map' {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {G : Type u → Type u} [Applicative G] [LawfulApplicative G] {α : Type u} {β : Type u} {γ : Type u} (g : αβ) (h : βG γ) :
    theorem Traversable.map_traverse' {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {G : Type u → Type u} [Applicative G] [LawfulApplicative G] {α : Type u} {β : Type u} {γ : Type u} (g : αG β) (h : βγ) :
    theorem Traversable.naturality_pf {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [LawfulApplicative F] [Applicative G] [LawfulApplicative G] {α : Type u} {β : Type u} (η : ApplicativeTransformation F G) (f : αF β) :
    traverse ((fun {α : Type u} => η.app α) f) = (fun {α : Type u} => η.app α) traverse f