Equiv.isLawfulTraversable'
theorem Equiv.isLawfulTraversable' :
∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [inst_1 : LawfulTraversable t]
[inst_2 : Traversable t'],
(∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f) →
(∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f) →
(∀ {F : Type u → Type u} [inst_3 : Applicative F] [inst_4 : LawfulApplicative F] {α β : Type u} (f : α → F β),
traverse f = Equiv.traverse eqv f) →
LawfulTraversable t'
The theorem `Equiv.isLawfulTraversable'` states that for any two type constructors `t` and `t'` with the property that there exists an equivalence between `t α` and `t' α` for all types `α`, if `t` is a lawful traversable functor, then `t'` can also be considered a lawful traversable functor provided that the `map`, `mapConst`, and `traverse` operations for `t'` are equivalent to those for `t` when carried over using the equivalences. More specifically, `map`, `mapConst`, and `traverse` operations for `t'` must be equal to `Equiv.map eqv`, `(Equiv.map eqv ∘ Function.const α)`, and `Equiv.traverse eqv` respectively, where `eqv` is the function giving the type equivalences.
More concisely: If `t` is a lawful traversable functor and there exists an equivalence between `t α` and `t' α` for all types `α`, then `t'` is a lawful traversable functor given equivalent `map`, `mapConst`, and `traverse` operations.
|
Equiv.isLawfulTraversable
theorem Equiv.isLawfulTraversable :
∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [inst_1 : LawfulTraversable t],
LawfulTraversable t'
This theorem states that if `t` is a lawful traversable functor, then its equivalence `t'`, given the traversable functor structure by `Equiv.traversable`, is also a lawful traversable functor. The equivalence is parameterized over types `α` and it transforms `t α` into `t' α`. The original type `t` needs to not only be traversable, but also lawful traversable for this to hold.
More concisely: If `t` is a lawful traversable functor, then the equivalence `Equiv.traversable t : Traversable (α →α) => Traversable α => Traversable α` obtained from `t` is also a lawful traversable functor.
|