theorem
applicative.map_seq_map
{F : Type u → Type v}
[applicative F]
[is_lawful_applicative F]
{α β γ σ : Type u}
(f : α → β → γ)
(g : σ → β)
(x : F α)
(y : F σ) :
theorem
applicative.pure_seq_eq_map'
{F : Type u → Type v}
[applicative F]
[is_lawful_applicative F]
{α β : Type u}
(f : α → β) :
has_seq.seq (has_pure.pure f) = functor.map f
theorem
applicative.ext
{F : Type u → Type u_1}
{A1 A2 : applicative F}
[is_lawful_applicative F]
[is_lawful_applicative F] :
(∀ {α : Type u} (x : α), has_pure.pure x = has_pure.pure x) → (∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x) → A1 = A2
@[instance]
Equations
theorem
functor.comp.map_pure
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
{α β : Type v}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
theorem
functor.comp.seq_pure
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
{α β : Type v}
(f : functor.comp F G (α → β))
(x : α) :
f <*> has_pure.pure x = (λ (g : α → β), g x) <$> f
theorem
functor.comp.seq_assoc
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
{α β γ : Type v}
(x : functor.comp F G α)
(f : functor.comp F G (α → β))
(g : functor.comp F G (β → γ)) :
theorem
functor.comp.pure_seq_eq_map
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G]
{α β : Type v}
(f : α → β)
(x : functor.comp F G α) :
has_pure.pure f <*> x = f <$> x
@[instance]
def
functor.comp.is_lawful_applicative
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
[is_lawful_applicative F]
[is_lawful_applicative G] :
Equations
theorem
functor.comp.applicative_id_comp
{F : Type u_1 → Type u_2}
[AF : applicative F]
[LF : is_lawful_applicative F] :
theorem
functor.comp.applicative_comp_id
{F : Type u_1 → Type u_2}
[AF : applicative F]
[LF : is_lawful_applicative F] :
@[instance]
def
functor.comp.is_comm_applicative
{f : Type u → Type w}
{g : Type v → Type u}
[applicative f]
[applicative g]
[is_comm_applicative f]
[is_comm_applicative g] :
Equations
theorem
comp.seq_mk
{α β : Type w}
{f : Type u → Type v}
{g : Type w → Type u}
[applicative f]
[applicative g]
(h : f (g (α → β)))
(x : f (g α)) :
functor.comp.mk h <*> functor.comp.mk x = functor.comp.mk (has_seq.seq <$> h <*> x)