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.

def Traversable.PureTransformation (F : Type u → Type u) [Applicative F] [LawfulApplicative F] : ApplicativeTransformation Id F

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

Equations

• Traversable.PureTransformation F = { app := @pure F inst✝¹.toPure, preserves_pure' := ⋯, preserves_seq' := ⋯ }

@[simp]

theorem Traversable.pureTransformation_apply (F : Type u → Type u) [Applicative F] [LawfulApplicative F] {α : Type u} (x : id α) : (fun {α : Type u} => (PureTransformation F).app α) x = pure x

theorem Traversable.map_eq_traverse_id {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {β γ : Type u} (f : β → γ) : Functor.map f = Id.run ∘ traverse (pure ∘ 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} (g : α → F β) (f : β → γ) (x : t α) : Functor.map f <$> traverse g x = traverse (Functor.map f ∘ g) x

theorem Traversable.traverse_map {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F : Type u → Type u} [Applicative F] [LawfulApplicative F] {α β γ : 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 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 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 G : Type u → Type u} [Applicative F] [LawfulApplicative F] [Applicative G] [LawfulApplicative G] {α β γ : 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} (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} (g : α → β) (h : β → G γ) : traverse (h ∘ g) = traverse h ∘ Functor.map 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} (g : α → G β) (h : β → γ) : traverse (Functor.map h ∘ g) = Functor.map (Functor.map h) ∘ traverse g

theorem Traversable.naturality_pf {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {F G : Type u → Type u} [Applicative F] [LawfulApplicative F] [Applicative G] [LawfulApplicative G] {α β : Type u} (η : ApplicativeTransformation F G) (f : α → F β) : traverse ((fun {α : Type u} => η.app α) ∘ f) = (fun {α : Type u} => η.app α) ∘ traverse f