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 #

source
@[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
source
@[protected]
def equiv.functor {t t' : Type u → Type u} (eqv : Π (α : Type u), t α ≃ t' α) [functor t] :
functor t'

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

Equations
source
@[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
source
@[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)
source
@[protected]
theorem equiv.is_lawful_functor {t t' : Type u → Type u} (eqv : Π (α : Type u), t α ≃ t' α) [functor t] [is_lawful_functor t] :
is_lawful_functor t'
source
@[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) :
is_lawful_functor t'
source
@[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
source
@[protected]
def equiv.traversable {t t' : Type u → Type u} (eqv : Π (α : Type u), t α ≃ t' α) [traversable t] :
traversable t'

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

Equations
source
@[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' α) :
equiv.traverse eqv id.mk x = x
source
@[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)
source
@[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' α) :
equiv.traverse eqv (functor.comp.mk ∘ functor.map f ∘ g) x = functor.comp.mk (equiv.traverse eqv f <$> equiv.traverse eqv g x)
source
@[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
source
@[protected]
def equiv.is_lawful_traversable {t t' : Type u → Type u} (eqv : Π (α : Type u), t α ≃ t' α) [traversable t] [is_lawful_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
source
@[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) :
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 fact that t is a lawful traversable functor carries over as well.

Equations