applicative instances

This file provides Applicative instances for concrete functors:

• id
• Functor.comp
• Functor.const
• Functor.add_const

theorem Applicative.map_seq_map {F : Type u → Type v} [Applicative F] [LawfulApplicative F] {α β γ σ : Type u} (f : α → β → γ) (g : σ → β) (x : F α) (y : F σ) : f <$> x <*> g <$> y = ((fun (x : β → γ) => x ∘ g) ∘ f) <$> x <*> y

theorem Applicative.pure_seq_eq_map' {F : Type u → Type v} [Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → β) : (fun (x : F α) => pure f <*> x) = fun (x : F α) => f <$> x

theorem Applicative.ext {F : Type u → Type u_1} {A1 A2 : Applicative F} [LawfulApplicative F] [LawfulApplicative F] : (∀ {α : Type u} (x : α), pure x = pure x) → (∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x) → A1 = A2

theorem instCommApplicativeId : CommApplicative Id

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} (f : α → β) (x : α) : f <$> pure x = pure (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} (f : Functor.Comp F G (α → β)) (x : α) : f <*> pure x = (fun (g : α → β) => g x) <$> f

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} (x : Functor.Comp F G α) (f : Functor.Comp F G (α → β)) (g : Functor.Comp F G (β → γ)) : g <*> (f <*> x) = Function.comp <$> g <*> f <*> x

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} (f : α → β) (x : Functor.Comp F G α) : pure f <*> x = f <$> x

theorem Functor.Comp.instLawfulApplicativeComp {F : Type u → Type w} {G : Type v → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] : LawfulApplicative (Functor.Comp F G)

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

theorem 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)

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 ((fun (x1 : g (α → β)) (x2 : g α) => x1 <*> x2) <$> h <*> x)

instance instApplicativeConstOfOneOfMul {α : Type u_1} [One α] [Mul α] : Applicative (Functor.Const α)

Equations

• instApplicativeConstOfOneOfMul = Applicative.mk

theorem instLawfulApplicativeConst {α : Type u_1} [Monoid α] : LawfulApplicative (Functor.Const α)

instance instApplicativeAddConstOfZeroOfAdd {α : Type u_1} [Zero α] [Add α] : Applicative (Functor.AddConst α)

Equations

• instApplicativeAddConstOfZeroOfAdd = Applicative.mk

theorem instLawfulApplicativeAddConst {α : Type u_1} [AddMonoid α] : LawfulApplicative (Functor.AddConst α)