{-# OPTIONS --type-in-type
#-}
open import NeilPrelude
open import Equational
module Applicative (F : Set → Set)
(fmap : {A B : Set} → (A → B) → F A → F B)
(pure : {A : Set} → A → F A)
(_<*>_ : {A B : Set} → F (A → B) → F A → F B)
(fmapLaw : {A B : Set} → {g : A → B} → {fa : F A} → fmap g fa ≡ pure g <*> fa)
(identityLaw : {A : Set} → {fa : F A} → Extensionality → pure id <*> fa ≡ fa)
(compositionLaw : {A B C : Set} → {fa : F A} → {fbc : F (B → C)} → {fab : F (A → B)} → Extensionality
→ ((pure (_∘_) <*> fbc) <*> fab) <*> fa ≡ fbc <*> (fab <*> fa))
(homomorphismLaw : {A B : Set} → {f : A → B} → {a : A} → pure f <*> pure a ≡ pure (f a))
(interchangeLaw : {A B : Set} → {fab : F (A → B)} → {a : A} → Extensionality
→ fab <*> pure a ≡ pure (applyTo a) <*> fab)
where
functorLaw1 : {A : Set} → {fa : F A} → Extensionality → fmap id fa ≡ fa
functorLaw1 {_} {fa} ext = fmap id fa
≡⟨ fmapLaw ⟩
pure id <*> fa
≡⟨ identityLaw ext ⟩
fa
QED
functorLaw2 : {A B C : Set} → {f : A → B} → {g : B → C} → {fa : F A} → Extensionality
→ fmap (g ∘ f) fa ≡ fmap g (fmap f fa)
functorLaw2 {_} {_} {_} {f} {g} {fa} ext =
fmap (g ∘ f) fa
≡⟨ fmapLaw ⟩
pure (g ∘ f) <*> fa
≡⟨ cong (flip _<*>_ fa) (sym homomorphismLaw) ⟩
(pure (_∘_ g) <*> pure f) <*> fa
≡⟨ cong (flip _<*>_ fa ∘ flip _<*>_ (pure f)) (sym homomorphismLaw) ⟩
((pure _∘_ <*> pure g) <*> pure f) <*> fa
≡⟨ compositionLaw ext ⟩
pure g <*> (pure f <*> fa)
≡⟨ cong (_<*>_ (pure g)) (sym fmapLaw) ⟩
pure g <*> fmap f fa
≡⟨ sym fmapLaw ⟩
fmap g (fmap f fa)
QED
import Pointed
open Pointed F fmap pure functorLaw1 functorLaw2 public
fmap2 : {A B C : Set} → (A → B → C) → F A → F B → F C
fmap2 f a b = fmap f a <*> b
fmap3 : {A B C D : Set} → (A → B → C → D) → F A → F B → F C → F D
fmap3 f a b c = fmap2 f a b <*> c
fmap4 : {A B C D E : Set} → (A → B → C → D → E) → F A → F B → F C → F D → F E
fmap4 f a b c d = fmap3 f a b c <*> d