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.isLawfulTraversable: Equiv.traverse as a lawful traversable functor.
def Equiv.map {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [] {α : Type u} {β : 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
Instances For
def Equiv.functor {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [] :

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

Equations
Instances For
theorem Equiv.id_map {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α 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' α) [] [] {α : 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' α) [] [] :
LawfulFunctor fun (α : Type u) => t' α
theorem Equiv.lawfulFunctor' {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [] [] [F : Functor t'] (h₀ : ∀ {α β : Type u} (f : αβ), = Equiv.map eqv f) (h₁ : ∀ {α β : Type u} (f : β), = (Equiv.map eqv ) f) :
def Equiv.traverse {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [] {m : Type u → Type u} [] {α : Type u} {β : 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
Instances For
theorem Equiv.traverse_def {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [] {m : Type u → Type u} [] {α : Type u} {β : Type u} (f : αm β) (x : t' α) :
Equiv.traverse eqv f x = (eqv β) <$> traverse f ((eqv α).symm x) def Equiv.traversable {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [] : The function Equiv.traverse transfers a traversable functor instance across the equivalences eqv. Equations Instances For theorem Equiv.id_traverse {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α 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' α) [] {α : 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' α) [] {F : Type u → Type u} {G : Type u → Type u} [] [] {α : Type u} {β : Type u} {γ : Type u} (f : βF γ) (g : αG β) (x : t' α) : Equiv.traverse eqv (Functor.Comp.mk 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' α) [] {F : Type u → Type u} {G : Type u → Type u} [] [] (η : ) {α : Type u} {β : Type u} (f : αF β) (x : t' α) :
(fun {α : Type u} => η.app α) (Equiv.traverse eqv f x) = Equiv.traverse eqv ((fun {α : Type u} => η.app α) f) x
theorem Equiv.isLawfulTraversable {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α 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.

theorem Equiv.isLawfulTraversable' {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [] [] (h₀ : ∀ {α β : Type u} (f : αβ), = Equiv.map eqv f) (h₁ : ∀ {α β : Type u} (f : β), = (Equiv.map eqv ) f) (h₂ : ∀ {F : Type u → Type u} [inst : ] [inst_1 : ] {α β : Type u} (f : α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.