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' β→ t' β using the functor t and the equivalence Π α, t α ≃ t' α≃ t' α.
• Equiv.functor: Equiv.map as a functor.
• Equiv.traverse: Turns traversably a function α → m β→ m β into a function t' α → m (t' β)→ m (t' β) using the traversable functor t and the equivalence Π α, t α ≃ t' α≃ t' α.
• Equiv.traversable: Equiv.traverse as a traversable functor.
• Equiv.isLawfulTraversable: Equiv.traverse as a lawful traversable functor.

ink

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

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

ink

def Equiv.functor {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : 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 {α β} => Equiv.map eqv, mapConst := fun {α β} => Equiv.map eqv ∘ Function.const β }

ink

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

ink

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)

ink

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' α

ink

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) : LawfulFunctor t'

ink

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

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

ink

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

ink

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

ink

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)

ink

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)

ink

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

ink

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

ink

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) : IsLawfulTraversable 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

• One or more equations did not get rendered due to their size.