Transferring traversable instances along isomorphisms #
This file allows to transfer traversable instances along isomorphisms.
Main declarations #
equiv.map: Turns functorially a functionα → βinto a functiont' α → t' βusing the functortand the equivalenceΠ α, t α ≃ t' α.equiv.functor:equiv.mapas a functor.equiv.traverse: Turns traversably a functionα → m βinto a functiont' α → m (t' β)using the traversable functortand the equivalenceΠ α, t α ≃ t' α.equiv.traversable:equiv.traverseas a traversable functor.equiv.is_lawful_traversable:equiv.traverseas a lawful traversable functor.
@[protected]
def
equiv.map
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[functor t]
{α β : 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).
@[protected]
def
equiv.functor
{t 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 := equiv.map eqv _inst_1, map_const := λ (α β : Type u), equiv.map eqv ∘ function.const β}
@[protected]
theorem
equiv.id_map
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[functor t]
[is_lawful_functor t]
{α : Type u}
(x : t' α) :
@[protected]
theorem
equiv.comp_map
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[functor t]
[is_lawful_functor t]
{α β γ : Type u}
(g : α → β)
(h : β → γ)
(x : t' α) :
@[protected]
theorem
equiv.is_lawful_functor
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[functor t]
[is_lawful_functor t] :
@[protected]
theorem
equiv.is_lawful_functor'
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[functor t]
[is_lawful_functor t]
[F : functor t']
(h₀ : ∀ {α β : Type u} (f : α → β), functor.map f = equiv.map eqv f)
(h₁ : ∀ {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv ∘ function.const α) f) :
@[protected]
def
equiv.traverse
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
{m : Type u → Type u}
[applicative m]
{α β : 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.
@[protected]
def
equiv.traversable
{t 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 = {to_functor := equiv.functor eqv traversable.to_functor, traverse := equiv.traverse eqv _inst_1}
@[protected]
theorem
equiv.id_traverse
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable t]
{α : Type u}
(x : t' α) :
equiv.traverse eqv id.mk x = x
@[protected]
theorem
equiv.traverse_eq_map_id
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable t]
{α β : Type u}
(f : α → β)
(x : t' α) :
@[protected]
theorem
equiv.comp_traverse
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
{α β γ : 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)
@[protected]
theorem
equiv.naturality
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable t]
{F G : Type u → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
(η : applicative_transformation F G)
{α β : Type u}
(f : α → F β)
(x : t' α) :
⇑η (equiv.traverse eqv f x) = equiv.traverse eqv (⇑η ∘ f) x
@[protected]
def
equiv.is_lawful_traversable
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable 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
- equiv.is_lawful_traversable eqv = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}
@[protected]
def
equiv.is_lawful_traversable'
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable t]
[traversable t']
(h₀ : ∀ {α β : Type u} (f : α → β), functor.map f = equiv.map eqv f)
(h₁ : ∀ {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv ∘ function.const α) f)
(h₂ : ∀ {F : Type u → Type u} [_inst_7 : applicative F] [_inst_8 : is_lawful_applicative 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
- equiv.is_lawful_traversable' eqv h₀ h₁ h₂ = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}