# mathlibdocumentation

control.traversable.equiv

# Transferring traversable instances along isomorphisms #

This file allows to transfer traversable instances along isomorphisms.

## Main declarations #

• equiv.map: Turns functorially a function α → β into a function t' α → t' β using the functor t and the equivalence Π α, t α ≃ t' α.
• equiv.functor: equiv.map as a functor.
• equiv.traverse: Turns traversably a function α → m β into a function t' α → m (t' β) using the traversable functor t and the equivalence Π α, t α ≃ t' α.
• equiv.traversable: equiv.traverse as a traversable functor.
• equiv.is_lawful_traversable: equiv.traverse as a lawful traversable functor.
@[protected]
def equiv.map {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] {α β : Type u} (f : α → β) (x : 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
@[protected]
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
@[protected]
theorem equiv.id_map {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] {α : Type u} (x : t' α) :
equiv.map eqv id x = x
@[protected]
theorem equiv.comp_map {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] {α β γ : Type u} (g : α → β) (h : β → γ) (x : t' α) :
equiv.map eqv (h g) x = equiv.map eqv h (equiv.map eqv g x)
@[protected]
theorem equiv.is_lawful_functor {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t]  :
@[protected]
theorem equiv.is_lawful_functor' {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [functor t] [F : functor t'] (h₀ : ∀ {α β : Type u} (f : α → β), = equiv.map eqv f) (h₁ : ∀ {α β : Type u} (f : β), = (equiv.map eqv f) :
@[protected]
def equiv.traverse {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] {m : Type uType u} [applicative m] {α β : Type u} (f : α → m β) (x : 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
@[protected]
def equiv.traversable {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] :

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

Equations
@[protected]
theorem equiv.id_traverse {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] {α : Type u} (x : t' α) :
x = x
@[protected]
theorem equiv.traverse_eq_map_id {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] {α β : Type u} (f : α → β) (x : t' α) :
(id.mk f) x = id.mk (equiv.map eqv f x)
@[protected]
theorem equiv.comp_traverse {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] {F G : Type uType u} [applicative F] [applicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t' α) :
@[protected]
theorem equiv.naturality {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] {F G : Type uType u} [applicative F] [applicative G] (η : G) {α β : Type u} (f : α → F β) (x : t' α) :
η (equiv.traverse eqv f x) = (η f) x
@[protected]
def equiv.is_lawful_traversable {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [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
@[protected]
def equiv.is_lawful_traversable' {t t' : Type uType u} (eqv : Π (α : Type u), t α t' α) [traversable t] [traversable t'] (h₀ : ∀ {α β : Type u} (f : α → β), = equiv.map eqv f) (h₁ : ∀ {α β : Type u} (f : β), = (equiv.map eqv f) (h₂ : ∀ {F : Type uType u} [_inst_7 : [_inst_8 : {α β : Type u} (f : α → F β), ) :

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 fact that t is a lawful traversable functor carries over as well.

Equations