Traversing collections #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves basic properties of traversable and applicative functors and defines
pure_transformation F, the natural applicative transformation from the identity functor to F.
References #
Inspired by The Essence of the Iterator Pattern.
def
traversable.pure_transformation
(F : Type u → Type u)
[applicative F]
[is_lawful_applicative F] :
The natural applicative transformation from the identity functor
to F, defined by pure : Π {α}, α → F α.
Equations
@[simp]
theorem
traversable.pure_transformation_apply
(F : Type u → Type u)
[applicative F]
[is_lawful_applicative F]
{α : Type u}
(x : id α) :
theorem
traversable.map_eq_traverse_id
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{β γ : Type u}
(f : β → γ) :
functor.map f = traversable.traverse (id.mk ∘ f)
theorem
traversable.map_traverse
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
{α β γ : Type u}
(g : α → F β)
(f : β → γ)
(x : t α) :
functor.map f <$> traversable.traverse g x = traversable.traverse (functor.map f ∘ g) x
theorem
traversable.traverse_map
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
{α β γ : Type u}
(f : β → F γ)
(g : α → β)
(x : t α) :
traversable.traverse f (g <$> x) = traversable.traverse (f ∘ g) x
theorem
traversable.pure_traverse
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
{α : Type u}
(x : t α) :
theorem
traversable.id_sequence
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{α : Type u}
(x : t α) :
theorem
traversable.comp_sequence
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α : Type u}
(x : t (F (G α))) :
theorem
traversable.naturality'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α : Type u}
(η : applicative_transformation F G)
(x : t (F α)) :
theorem
traversable.traverse_id
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{α : Type u} :
theorem
traversable.traverse_comp
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α β γ : Type u}
(g : α → F β)
(h : β → G γ) :
theorem
traversable.traverse_eq_map_id'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{β γ : Type u}
(f : β → γ) :
traversable.traverse (id.mk ∘ f) = id.mk ∘ functor.map f
theorem
traversable.traverse_map'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{G : Type u → Type u}
[applicative G]
[is_lawful_applicative G]
{α β γ : Type u}
(g : α → β)
(h : β → G γ) :
traversable.traverse (h ∘ g) = traversable.traverse h ∘ functor.map g
theorem
traversable.map_traverse'
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{G : Type u → Type u}
[applicative G]
[is_lawful_applicative G]
{α β γ : Type u}
(g : α → G β)
(h : β → γ) :
traversable.traverse (functor.map h ∘ g) = functor.map (functor.map h) ∘ traversable.traverse g
theorem
traversable.naturality_pf
{t : Type u → Type u}
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[is_lawful_applicative F]
[applicative G]
[is_lawful_applicative G]
{α β : Type u}
(η : applicative_transformation F G)
(f : α → F β) :
traversable.traverse (⇑η ∘ f) = ⇑η ∘ traversable.traverse f