def
equiv.functor
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[functor t] :
functor t'
Equations
- equiv.functor eqv = {map := equiv.map eqv _inst_1, map_const := λ (α β : Type u), equiv.map eqv ∘ function.const β}
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' α) :
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' α) :
theorem
equiv.is_lawful_functor
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[functor t]
[is_lawful_functor t] :
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'] :
(∀ {α β : Type u} (f : α → β), functor.map f = equiv.map eqv f) → (∀ {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv ∘ function.const α) f) → is_lawful_functor t'
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} :
(α → m β) → t' α → m (t' β)
Equations
- equiv.traverse eqv f x = ⇑(eqv β) <$> traversable.traverse f (⇑((eqv α).symm) x)
def
equiv.traversable
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t] :
traversable t'
Equations
- equiv.traversable eqv = {to_functor := equiv.functor eqv traversable.to_functor, traverse := equiv.traverse eqv _inst_1}
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
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' α) :
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)
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
def
equiv.is_lawful_traversable
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable t] :
Equations
- equiv.is_lawful_traversable eqv = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}
def
equiv.is_lawful_traversable'
{t t' : Type u → Type u}
(eqv : Π (α : Type u), t α ≃ t' α)
[traversable t]
[is_lawful_traversable t]
[traversable t'] :
(∀ {α β : Type u} (f : α → β), functor.map f = equiv.map eqv f) → (∀ {α β : Type u} (f : β), functor.map_const f = (equiv.map eqv ∘ function.const α) f) → (∀ {F : Type u → Type u} [_inst_7 : applicative F] [_inst_8 : is_lawful_applicative F] {α β : Type u} (f : α → F β), traversable.traverse f = equiv.traverse eqv f) → is_lawful_traversable t'
Equations
- equiv.is_lawful_traversable' eqv h₀ h₁ h₂ = {to_is_lawful_functor := _, id_traverse := _, comp_traverse := _, traverse_eq_map_id := _, naturality := _}