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 functort
and the equivalenceΠ α, t α ≃ t' α
.equiv.functor
:equiv.map
as a functor.equiv.traverse
: Turns traversably a functionα → m β
into a functiont' α → m (t' β)
using the traversable functort
and the equivalenceΠ α, t α ≃ t' α
.equiv.traversable
:equiv.traverse
as a traversable functor.equiv.is_lawful_traversable
:equiv.traverse
as a lawful traversable functor.
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
).
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 β}
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 β) <$> traversable.traverse f (⇑((eqv α).symm) x)
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}
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 := _}
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 := _}