mathlib documentation

control.traversable.equiv

def equiv.map {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] {α β : Type u} :
(α → β)t' αt' β

Given a functor t, a function t' : Type u → Type u, and equivalences t α ≃ t' α for all α, then every function α → β can be mapped to a function t' α → t' β functorially (see equiv.functor).

Equations
def equiv.functor {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] :

The function equiv.map transfers the functoriality of t to t' using the equivalences eqv.

Equations
theorem equiv.id_map {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] [is_lawful_functor t] {α : Type u} (x : t' α) :
equiv.map eqv id x = x

theorem equiv.comp_map {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] [is_lawful_functor t] {α β γ : Type u} (g : α → β) (h : β → γ) (x : t' α) :
equiv.map eqv (h g) x = equiv.map eqv h (equiv.map eqv g x)

theorem equiv.is_lawful_functor {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] [is_lawful_functor t] :

theorem equiv.is_lawful_functor' {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] [is_lawful_functor t] [F : functor t'] :
(∀ {α β : Type u} (f : α → β), functor.map f = equiv.map eqv f)(∀ {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv function.const α) f)is_lawful_functor t'

def equiv.traverse {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] {m : Type uType u} [applicative m] {α β : Type u} :
(α → m β)t' αm (t' β)

Like equiv.map, a function t' : Type u → Type u can be given the structure of a traversable functor using a traversable functor t' and equivalences t α ≃ t' α for all α. See equiv.traversable.

Equations
def equiv.traversable {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] :

The function equiv.tranverse transfers a traversable functor instance across the equivalences eqv.

Equations
theorem equiv.id_traverse {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] {α : Type u} (x : t' α) :

theorem equiv.traverse_eq_map_id {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] {α β : Type u} (f : α → β) (x : t' α) :
equiv.traverse eqv (id.mk f) x = id.mk (equiv.map eqv f x)

theorem equiv.comp_traverse {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t' α) :

theorem equiv.naturality {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (f : α → F β) (x : t' α) :
η (equiv.traverse eqv f x) = equiv.traverse eqv (η f) x

def equiv.is_lawful_traversable {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] :

The fact that t is a lawful traversable functor carries over the equivalences to t', with the traversable functor structure given by equiv.traversable.

Equations
def equiv.is_lawful_traversable' {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] [traversable t'] :
(∀ {α β : Type u} (f : α → β), functor.map f = equiv.map eqv f)(∀ {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv function.const α) f)(∀ {F : Type uType u} [_inst_7 : applicative F] [_inst_8 : is_lawful_applicative F] {α β : Type u} (f : α → F β), traverse f = equiv.traverse eqv f)is_lawful_traversable t'

If the traversable t' instance has the properties that map, map_const, and traverse are equal to the ones that come from carrying the traversable functor structure from t over the equivalences, then the the fact t is a lawful traversable functor carries over as well.

Equations