Proof that the left propagating ComonadApply instance for Store satisfies the laws

storeProofLeft.md

Relevant definitions

data Store s a = Store (s -> a) s
fmap g (Store f s) = Store (g.f) s
extract f s = f s
duplicate (Store f s) = Store (Store f) s

Store f1 s1 <@> Store f2 s2 = Store (\s -> f1 s (f2 s2)) s1

We will also use S as a synonym for the data constructor Store

Associativity law

(.) <$> Store f1 s1 <@> Store f2 s2 <@> Store f3 s3
= Store ((.) . f1) s1 <@> Store f2 s2 <@> Store f3 s3 
= Store (\s -> (.) (f1 s) (f2 s2)) s1 <@> Store f3 s3
= Store (\s -> (.) (f1 s) (f2 s2) (f3 s3)) s1
= Store (\s -> f1 s (f2 s2 (f3 s3))) s1

Store f1 s1 <@> (Store f2 s2 <@> Store f3 s3)
= Store f1 s1 <@> Store (\s -> f2 s (f3 s3)) s2
= Store (\s -> f1 s (f2 s2 (f3 s3))) s1

Extract law

extract (Store f1 s1) (extract (Store f2 s2))
= f1 s1 (f2 s2)

extract (Store f1 s1 <@> Store f2 s2)
= extract (Store (\s -> f1 s (f2 s2)) s1)
= f1 s1 (f2 s2)

Duplicate law

duplicate (S f1 s1 <@> S f2 s2)
= duplicate (S (\s -> f1 s (f2 s2)) s1)
= S (S (\s -> f1 s (f2 s2))) s1

(<@>) <$> duplicate (S f1 s1) <@> duplicate (S f2 s2)
= (<@>) <$> S (S f1) s1 <@> S (S f2) s2
= S ((<@>) . S f1) s1 <@> S (S f2) s2
= S (\t -> (<@>) (S f1 t) (S f2 s2)) s1
= S (\t -> S (\s -> f1 s (f2 s2)) t) s1
= S (S (\s -> f1 s (f2 s2))) s1