applicative
instances #
This file provides Applicative
instances for concrete functors:
id
Functor.comp
Functor.const
Functor.add_const
theorem
Applicative.pure_seq_eq_map'
{F : Type u → Type v}
[Applicative F]
[LawfulApplicative F]
{α : Type u}
{β : Type u}
(f : α → β)
:
theorem
Applicative.ext
{F : Type u → Type u_1}
{A1 : Applicative F}
{A2 : Applicative F}
[LawfulApplicative F]
[LawfulApplicative F]
:
theorem
Functor.Comp.map_pure
{F : Type u → Type w}
{G : Type v → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative F]
[LawfulApplicative G]
{α : Type v}
{β : Type v}
(f : α → β)
(x : α)
:
theorem
Functor.Comp.seq_pure
{F : Type u → Type w}
{G : Type v → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative F]
[LawfulApplicative G]
{α : Type v}
{β : Type v}
(f : Functor.Comp F G (α → β))
(x : α)
:
theorem
Functor.Comp.seq_assoc
{F : Type u → Type w}
{G : Type v → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative F]
[LawfulApplicative G]
{α : Type v}
{β : Type v}
{γ : 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]
[LawfulApplicative F]
[LawfulApplicative G]
{α : Type v}
{β : Type v}
(f : α → β)
(x : Functor.Comp F G α)
:
instance
Functor.Comp.instLawfulApplicativeComp
{F : Type u → Type w}
{G : Type v → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative F]
[LawfulApplicative G]
:
Equations
- ⋯ = ⋯
theorem
Functor.Comp.applicative_id_comp
{F : Type u_1 → Type u_2}
[AF : Applicative F]
[LawfulApplicative F]
:
Functor.Comp.instApplicativeComp = AF
theorem
Functor.Comp.applicative_comp_id
{F : Type u_1 → Type u_2}
[AF : Applicative F]
[LawfulApplicative F]
:
Functor.Comp.instApplicativeComp = AF
instance
Functor.Comp.instCommApplicative
{f : Type u → Type w}
{g : Type v → Type u}
[Applicative f]
[Applicative g]
[CommApplicative f]
[CommApplicative g]
:
CommApplicative (Functor.Comp f g)
Equations
- ⋯ = ⋯
theorem
Comp.seq_mk
{α : Type w}
{β : 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 ((fun (x1 : g (α → β)) (x2 : g α) => x1 <*> x2) <$> h <*> x)
Equations
- instApplicativeConstOfOneOfMul = Applicative.mk
Equations
- ⋯ = ⋯
Equations
- instApplicativeAddConstOfZeroOfAdd = Applicative.mk
Equations
- ⋯ = ⋯