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) [Applicative F] [LawfulApplicative F] : ApplicativeTransformation Id F

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

@[simp]

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

theorem Traversable.map_eq_traverse_id {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {β : Type u} {γ : Type u} (f : β → γ) : Functor.map f = 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} {β : Type u} {γ : 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} {β : 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 {α} => ApplicativeTransformation.app η α) (t α) (sequence x) = sequence ((fun {α} => ApplicativeTransformation.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 γ) : 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} {β : Type u} {γ : 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 : 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 {α} => ApplicativeTransformation.app η α) β ∘ f) = (fun {α} => ApplicativeTransformation.app η α) (t β) ∘ traverse f