mathlib documentation

control.traversable.lemmas

Traversing collections #

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.

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

Equations
@[simp]
theorem traversable.pure_transformation_apply (F : Type uType u) [applicative F] [is_lawful_applicative F] {α : Type u} (x : id α) :
theorem traversable.map_eq_traverse_id {t : Type uType u} [traversable t] [is_lawful_traversable t] {β γ : Type u} (f : β → γ) :
theorem traversable.map_traverse {t : Type uType u} [traversable t] [is_lawful_traversable t] {F : Type uType u} [applicative F] [is_lawful_applicative F] {α β γ : Type u} (g : α → F β) (f : β → γ) (x : t α) :
theorem traversable.traverse_map {t : Type uType u} [traversable t] [is_lawful_traversable t] {F : Type uType u} [applicative F] [is_lawful_applicative F] {α β γ : Type u} (f : β → F γ) (g : α → β) (x : t α) :
theorem traversable.pure_traverse {t : Type uType u} [traversable t] [is_lawful_traversable t] {F : Type uType u} [applicative F] [is_lawful_applicative F] {α : Type u} (x : t α) :
theorem traversable.id_sequence {t : Type uType u} [traversable t] [is_lawful_traversable t] {α : Type u} (x : t α) :
theorem traversable.comp_sequence {t : Type uType u} [traversable t] [is_lawful_traversable t] {F G : Type uType u} [applicative F] [is_lawful_applicative F] [applicative G] [is_lawful_applicative G] {α : Type u} (x : t (F (G α))) :
theorem traversable.naturality' {t : Type uType u} [traversable t] [is_lawful_traversable t] {F G : Type uType 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 uType u} [traversable t] [is_lawful_traversable t] {α : Type u} :
theorem traversable.traverse_comp {t : Type uType u} [traversable t] [is_lawful_traversable t] {F G : Type uType 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 uType u} [traversable t] [is_lawful_traversable t] {β γ : Type u} (f : β → γ) :
theorem traversable.traverse_map' {t : Type uType u} [traversable t] [is_lawful_traversable t] {G : Type uType u} [applicative G] [is_lawful_applicative G] {α β γ : Type u} (g : α → β) (h : β → G γ) :
theorem traversable.map_traverse' {t : Type uType u} [traversable t] [is_lawful_traversable t] {G : Type uType u} [applicative G] [is_lawful_applicative G] {α β γ : Type u} (g : α → G β) (h : β → γ) :
theorem traversable.naturality_pf {t : Type uType u} [traversable t] [is_lawful_traversable t] {F G : Type uType u} [applicative F] [is_lawful_applicative F] [applicative G] [is_lawful_applicative G] {α β : Type u} (η : applicative_transformation F G) (f : α → F β) :