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' α) [Functor 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

• Equiv.map eqv f x = (eqv β) (f <$> (eqv α).symm x)

def Equiv.functor {t : Type u → Type u} {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

• Equiv.functor eqv = { map := fun {α β : Type u} => Equiv.map eqv, mapConst := fun {α β : Type u} => Equiv.map eqv ∘ Function.const β }

theorem Equiv.id_map {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] [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' α) [Functor t] [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' α) [Functor t] [LawfulFunctor t] : LawfulFunctor fun (α : Type u) => t' α

theorem Equiv.lawfulFunctor' {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] [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) : LawfulFunctor t'

def Equiv.traverse {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Traversable t] {m : Type u → Type u} [Applicative m] {α : 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

• Equiv.traverse eqv f x = ⇑(eqv β) <$> traverse f ((eqv α).symm x)

theorem Equiv.traverse_def {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Traversable t] {m : Type u → Type u} [Applicative m] {α : 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' α) [Traversable t] : Traversable t'

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

Equations

• Equiv.traversable eqv = Traversable.mk fun {m : Type u → Type u} [Applicative m] {α β : Type u} => Equiv.traverse eqv

theorem Equiv.id_traverse {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Traversable t] [LawfulTraversable 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' α) [Traversable t] [LawfulTraversable 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' α) [Traversable t] [LawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [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' α) [Traversable t] [LawfulTraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α : 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' α) [Traversable t] [LawfulTraversable t] : LawfulTraversable 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' α) [Traversable t] [LawfulTraversable t] [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) : LawfulTraversable 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.