mathlib3 documentation

control.traversable.equiv

Transferring traversable instances along isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file allows to transfer traversable instances along isomorphisms.

Main declarations #

@[protected]
def equiv.map {t t' : Type u Type 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 u Type 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 u Type u} (eqv : Π (α : Type u), t α t' α) [functor t] [is_lawful_functor t] {α : Type u} (x : t' α) :
equiv.map eqv id x = x
@[protected]
theorem equiv.comp_map {t t' : Type u Type 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)
@[protected]
theorem equiv.is_lawful_functor {t t' : Type u Type u} (eqv : Π (α : Type u), t α t' α) [functor t] [is_lawful_functor t] :
@[protected]
theorem equiv.is_lawful_functor' {t t' : Type u Type u} (eqv : Π (α : Type u), t α t' α) [functor t] [is_lawful_functor t] [F : functor t'] (h₀ : {α β : Type u} (f : α β), functor.map f = equiv.map eqv f) (h₁ : {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv function.const α) f) :
@[protected]
def equiv.traverse {t t' : Type u Type u} (eqv : Π (α : Type u), t α t' α) [traversable t] {m : Type u Type 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 u Type 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 u Type u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] {α : Type u} (x : t' α) :
@[protected]
theorem equiv.traverse_eq_map_id {t t' : Type u Type 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)
@[protected]
theorem equiv.comp_traverse {t t' : Type u Type u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] {F G : Type u Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α β γ : Type u} (f : β F γ) (g : α G β) (x : t' α) :
@[protected]
theorem equiv.naturality {t t' : Type u Type u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] {F G : Type u Type 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
@[protected]
def equiv.is_lawful_traversable {t t' : Type u Type 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
@[protected]
def equiv.is_lawful_traversable' {t t' : Type u Type u} (eqv : Π (α : Type u), t α t' α) [traversable t] [is_lawful_traversable t] [traversable t'] (h₀ : {α β : Type u} (f : α β), functor.map f = equiv.map eqv f) (h₁ : {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv function.const α) f) (h₂ : {F : Type u Type u} [_inst_7 : applicative F] [_inst_8 : is_lawful_applicative F] {α β : Type u} (f : α F β), traversable.traverse f = equiv.traverse eqv 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