Documentation

Mathlib.Control.Traversable.Equiv

Transferring Traversable instances along isomorphisms #

This file allows to transfer Traversable instances along isomorphisms.

Main declarations #

def Equiv.map {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Functor t] {α : Type u} {β : Type u} (f : αβ) (x : t' α) :
t' β

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

Equations
def Equiv.functor {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Functor t] :

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

Equations
theorem Equiv.id_map {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Functor t] [inst : LawfulFunctor t] {α : Type u} (x : t' α) :
Equiv.map eqv id x = x
theorem Equiv.comp_map {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Functor t] [inst : LawfulFunctor t] {α : Type u} {β : Type u} {γ : Type u} (g : αβ) (h : βγ) (x : t' α) :
Equiv.map eqv (h g) x = Equiv.map eqv h (Equiv.map eqv g x)
theorem Equiv.lawfulFunctor {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Functor t] [inst : LawfulFunctor t] :
LawfulFunctor fun α => t' α
theorem Equiv.lawfulFunctor' {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Functor t] [inst : LawfulFunctor t] [F : Functor t'] (h₀ : ∀ {α β : Type u} (f : αβ), Functor.map f = Equiv.map eqv f) (h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv Function.const α) f) :
def Equiv.traverse {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] {m : Type u → Type u} [inst : Applicative m] {α : Type u} {β : Type u} (f : αm β) (x : t' α) :
m (t' β)

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

Equations
def Equiv.traversable {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] :

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

Equations
theorem Equiv.id_traverse {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] [inst : IsLawfulTraversable t] {α : Type u} (x : t' α) :
Equiv.traverse eqv pure x = x
theorem Equiv.traverse_eq_map_id {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] [inst : IsLawfulTraversable t] {α : Type u} {β : Type u} (f : αβ) (x : t' α) :
Equiv.traverse eqv (pure f) x = pure (Equiv.map eqv f x)
theorem Equiv.comp_traverse {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] [inst : IsLawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [inst : Applicative F] [inst : Applicative G] [inst : LawfulApplicative F] [inst : LawfulApplicative G] {α : Type u} {β : Type u} {γ : 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)
theorem Equiv.naturality {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] [inst : IsLawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [inst : Applicative F] [inst : Applicative G] [inst : LawfulApplicative F] [inst : LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u} {β : Type u} (f : αF β) (x : t' α) :
(fun {α} => ApplicativeTransformation.app η α) (t' β) (Equiv.traverse eqv f x) = Equiv.traverse eqv ((fun {α} => ApplicativeTransformation.app η α) β f) x
def Equiv.isLawfulTraversable {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] [inst : IsLawfulTraversable 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
  • One or more equations did not get rendered due to their size.
def Equiv.isLawfulTraversable' {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [inst : Traversable t] [inst : IsLawfulTraversable t] [inst : Traversable t'] (h₀ : ∀ {α β : Type u} (f : αβ), Functor.map f = Equiv.map eqv f) (h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv Function.const α) f) (h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : αF β), 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
  • One or more equations did not get rendered due to their size.