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' α) [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
Instances For
    def Equiv.functor {t : Type u → Type u} {t' : Type u → Type u} (eqv : (α : Type u) → t α t' α) [Functor 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' α) [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] :
      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) :
      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
      Instances For
        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] :

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

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

          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.