Updated the code in response to changes to the standard library.

Furthermore some laws related to _<$>_ were added, and some were
changed.

Author: nad

StructurallyRecursiveDescentParsing/DepthFirst.agda

@@ -17,7 +17,7 @@ open import Data.Vec using ([]; _∷_)
 open import Data.Vec.Bounded hiding ([]; _∷_)
 open import Effect.Applicative.Indexed
 open import Effect.Monad.Indexed
-open import Effect.Monad.State
+open import Effect.Monad.State.Indexed
 open import Function
 open import Codata.Musical.Notation
 import Level

TotalParserCombinators/Derivative/Definition.agda

@@ -13,11 +13,11 @@ open import Level
 
 open RawMonadPlus {f = zero} Data.List.Effectful.monadPlus
   using ()
-  renaming ( return to return′
-           ; ∅      to fail′
-           ; _∣_    to _∣′_
-           ; _⊛_    to _⊛′_
-           ; _>>=_  to _>>=′_
+  renaming ( pure  to return′
+           ; ∅     to fail′
+           ; _∣_   to _∣′_
+           ; _⊛_   to _⊛′_
+           ; _>>=_ to _>>=′_
            )
 
 open import TotalParserCombinators.Lib

TotalParserCombinators/InitialBag.agda

@@ -59,7 +59,7 @@ mutual
 
     complete′ : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
                 x ∈ p · s → s ≡ [] → x ∈ xs
-    complete′ return                                                    refl = to return↔            ⟨$⟩ refl
+    complete′ return                                                    refl = to pure↔              ⟨$⟩ refl
     complete′ (∣-left      x∈p₁)                                        refl = to ++↔                ⟨$⟩ inj₁ (complete x∈p₁)
     complete′ (∣-right xs₁ x∈p₂)                                        refl = to (++↔ {P = _≡_ _}
                                                                                        {xs = xs₁})   ⟨$⟩ inj₂ (complete x∈p₂)

TotalParserCombinators/Laws.agda

@@ -55,9 +55,15 @@ module Return⋆ = TotalParserCombinators.Laws.ReturnStar
 
 -- Laws related to _⊛_.
 
+import TotalParserCombinators.Laws.ApplicativeFunctor as AF
+  hiding (module <$>)
+module ApplicativeFunctor = AF
+
+-- Laws related to _<$>_.
+
 import TotalParserCombinators.Laws.ApplicativeFunctor
-module ApplicativeFunctor =
-  TotalParserCombinators.Laws.ApplicativeFunctor
+module <$> =
+  TotalParserCombinators.Laws.ApplicativeFunctor.<$>
 
 -- Laws related to _>>=_.
 
@@ -69,52 +75,6 @@ module Monad = TotalParserCombinators.Laws.Monad
 import TotalParserCombinators.Laws.KleeneAlgebra
 module KleeneAlgebra = TotalParserCombinators.Laws.KleeneAlgebra
 
-------------------------------------------------------------------------
--- Some laws for _<$>_
-
-module <$> where
-
-  open D
-
-  -- _<$>_ could have been defined using return and _⊛_.
-
-  return-⊛ : ∀ {Tok R₁ R₂ xs} {f : R₁ → R₂} (p : Parser Tok R₁ xs) →
-             f <$> p ≅P return f ⊛ p
-  return-⊛ {xs = xs} {f} p =
-    BagMonoid.reflexive (lemma xs) ∷ λ t → ♯ (
-      f <$> D t p         ≅⟨ return-⊛ (D t p) ⟩
-      return f ⊛ D t p    ≅⟨ sym $ D-return-⊛ f p ⟩
-      D t (return f ⊛ p)  ∎)
-    where
-    lemma : ∀ xs → List.map f xs ≡ ([ f ] ⊛′ xs)
-    lemma []       = P.refl
-    lemma (x ∷ xs) = P.cong (_∷_ (f x)) $ lemma xs
-
-  -- fail is a zero for _<$>_.
-
-  zero : ∀ {Tok R₁ R₂} {f : R₁ → R₂} →
-         f <$> fail {Tok = Tok} ≅P fail
-  zero {f = f} =
-    f <$> fail       ≅⟨ return-⊛ fail ⟩
-    return f ⊛ fail  ≅⟨ ApplicativeFunctor.right-zero (return f) ⟩
-    fail             ∎
-
-  -- A variant of ApplicativeFunctor.homomorphism.
-
-  homomorphism : ∀ {Tok R₁ R₂} (f : R₁ → R₂) {x} →
-                 f <$> return {Tok = Tok} x ≅P return (f x)
-  homomorphism f {x} =
-    f <$> return x       ≅⟨ return-⊛ {f = f} (return x) ⟩
-    return f ⊛ return x  ≅⟨ ApplicativeFunctor.homomorphism f x ⟩
-    return (f x)         ∎
-
-  -- Adjacent uses of _<$>_ can be fused.
-
-  <$>-<$> : ∀ {Tok R₁ R₂ R₃ xs}
-              {f : R₂ → R₃} {g : R₁ → R₂} {p : Parser Tok R₁ xs} →
-            f <$> (g <$> p) ≅P (f ∘ g) <$> p
-  <$>-<$> = BagMonoid.reflexive (P.sym (map-∘ _)) ∷ λ _ → ♯ <$>-<$>
-
 ------------------------------------------------------------------------
 -- A law for nonempty
 

TotalParserCombinators/Laws/ApplicativeFunctor.agda

@@ -1,20 +1,25 @@
 ------------------------------------------------------------------------
--- Laws related to _⊛_ and return
+-- Laws related to _⊛_, _<$>_ and return
 ------------------------------------------------------------------------
 
 module TotalParserCombinators.Laws.ApplicativeFunctor where
 
 open import Algebra
 open import Codata.Musical.Notation
-open import Data.List
+open import Data.List as List
 import Data.List.Effectful
+import Data.List.Properties as L
 import Data.List.Relation.Binary.BagAndSetEquality as BSEq
 open import Effect.Monad
 open import Function
-open import Level
-
-open RawMonad {f = zero} Data.List.Effectful.monad
-  using () renaming (_⊛_ to _⊛′_; _>>=_ to _>>=′_)
+import Level
+open import Relation.Binary.PropositionalEquality
+  using (module ≡-Reasoning)
+
+open RawMonad {f = Level.zero} Data.List.Effectful.monad
+  using ()
+  renaming (pure to return′;
+            _<$>_ to _<$>′_; _⊛_ to _⊛′_; _>>=_ to _>>=′_)
 private
   module BagMonoid {k} {A : Set} =
     CommutativeMonoid (BSEq.commutativeMonoid k A)
@@ -28,6 +33,98 @@ import TotalParserCombinators.Laws.Monad as Monad
 open import TotalParserCombinators.Lib
 open import TotalParserCombinators.Parser
 
+private variable
+  Tok R R₁ R₂ R₃ : Set
+  xs xs₁         : List R
+  p p₁ p₂        : Parser Tok R xs
+  x              : R
+  f g            : R₁ → R₂
+
+------------------------------------------------------------------------
+-- Some lemmas related to _<$>_
+
+module <$> where
+
+  -- Functor laws (expressed in a certain way).
+
+  identity : id <$> p ≅P p
+  identity {p = p} =
+    BagMonoid.reflexive (L.map-id _) ∷ λ t → ♯ (
+      id <$> D t p  ≅⟨ identity ⟩
+      D t p         ∎)
+
+  composition : (f ∘ g) <$> p ≅P f <$> (g <$> p)
+  composition {f = f} {g = g} {p = p} =
+    BagMonoid.reflexive (L.map-∘ _) ∷ λ t → ♯ (
+      (f ∘ g) <$> D t p    ≅⟨ composition ⟩
+      f <$> (g <$> D t p)  ∎)
+
+  -- The fail combinator is a right zero for _<$>_.
+
+  zero : f <$> fail ≅P fail {Tok = Tok}
+  zero {f = f} =
+    BagMonoid.refl ∷ λ _ → ♯ (
+      f <$> fail  ≅⟨ zero ⟩
+      fail        ∎)
+
+  -- A variant of the lemma homomorphism which is defined below.
+
+  homomorphism : f <$> return x ≅P return {Tok = Tok} (f x)
+  homomorphism {f = f} {x = x} =
+    BagMonoid.refl ∷ λ _ → ♯ (
+      f <$> fail  ≅⟨ zero ⟩
+      fail        ∎)
+
+  -- The combinator _<$>_ distributes from the left over _∣_.
+
+  left-distributive :
+    {p₁ : Parser Tok R₁ xs₁} →
+    f <$> (p₁ ∣ p₂) ≅P f <$> p₁ ∣ f <$> p₂
+  left-distributive {xs₁ = xs₁} {f = f} {p₂ = p₂} {p₁ = p₁} =
+    BagMonoid.reflexive (L.map-++ _ xs₁ _) ∷ λ t → ♯ (
+      f <$> (D t p₁ ∣ D t p₂)      ≅⟨ left-distributive ⟩
+      f <$> D t p₁ ∣ f <$> D t p₂  ∎)
+
+  -- The combinator _<$>_ can be expressed using _>>=_ and return.
+
+  in-terms-of->>= :
+    {p : Parser Tok R₁ xs} →
+    f <$> p ≅P p >>= (return ∘ f)
+  in-terms-of->>= {xs = xs} {f = f} {p = p} =
+    BagMonoid.reflexive lemma ∷ λ t → ♯ (
+      f <$> D t p                                           ≅⟨ sym (AdditiveMonoid.right-identity _) ⟩
+      f <$> D t p ∣ fail                                    ≅⟨ in-terms-of->>= ∣′ sym (Derivative.right-zero->>= _) ⟩
+      D t p >>= (return ∘ f) ∣ return⋆ xs >>= (λ _ → fail)  ∎)
+    where
+    open Data.List.Effectful.Applicative
+    open Data.List.Effectful.MonadProperties
+
+    lemma =
+      List.map f xs                               ≡-Reasoning.≡⟨ unfold-<$> _ _ ⟩
+      return′ f ⊛′ xs                             ≡-Reasoning.≡⟨ unfold-⊛ (return′ _) _ ⟩
+      (return′ f >>=′ λ f → xs >>=′ return′ ∘ f)  ≡-Reasoning.≡⟨ left-identity _ (λ f → xs >>=′ return′ ∘ f) ⟩
+      (xs >>=′ return′ ∘ f)                       ≡-Reasoning.∎
+
+  -- The combinator _<$>_ can be expressed using _⊛_ and return.
+
+  in-terms-of-⊛ : f <$> p ≅P return f ⊛ p
+  in-terms-of-⊛ {f = f} {p = p} =
+    BagMonoid.sym (BagMonoid.identityʳ _) ∷ λ t → ♯ (
+      f <$> D t p         ≅⟨ in-terms-of-⊛ ⟩
+      return f ⊛ D t p    ≅⟨ sym $ D-return-⊛ f p ⟩
+      D t (return f ⊛ p)  ∎)
+
+  -- A lemma related to _<$>_ and _>>=_.
+
+  >>=-∘ :
+    {p₂ : (x : R₂) → Parser Tok R₃ (g x)} →
+    p₁ >>= (p₂ ∘ f) ≅P f <$> p₁ >>= p₂
+  >>=-∘ {p₁ = p₁} {f = f} {p₂ = p₂} =
+    (p₁ >>= λ x → p₂ (f x))             ≅⟨ ([ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ → sym $ Monad.left-identity _ _) ⟩
+    (p₁ >>= λ x → return (f x) >>= p₂)  ≅⟨ Monad.associative _ _ _ ⟩
+    p₁ >>= (return ∘ f) >>= p₂          ≅⟨ ([ ○ - ○ - ○ - ○ ] sym in-terms-of->>= >>= λ _ → _ ∎) ⟩
+    f <$> p₁ >>= p₂                     ∎
+
 ------------------------------------------------------------------------
 -- _⊛_, return, _∣_ and fail form an applicative functor "with a zero
 -- and a plus"
@@ -36,16 +133,16 @@ open import TotalParserCombinators.Parser
 -- resembles an idempotent semiring (if we restrict ourselves to
 -- language equivalence).
 
--- First note that _⊛_ can be defined using _>>=_.
+-- First note that _⊛_ can be defined using _>>=_ and _<$>_.
 
 private
 
-  -- A variant of "flip map".
+  -- A flipped variant of "map".
 
   pam : ∀ {Tok R₁ R₂ xs} →
         Parser Tok R₁ xs → (f : R₁ → R₂) →
-        Parser Tok R₂ (xs >>=′ [_] ∘ f)
-  pam p f = p >>= (return ∘ f)
+        Parser Tok R₂ (f <$>′ xs)
+  pam p f = f <$> p
 
   infixl 10 _⊛″_
 
@@ -70,27 +167,12 @@ private
     return⋆ (flatten fs) ⊛ D t (♭? p₂)                    ≅⟨ ⊛-in-terms-of->>= (D t (♭? p₁)) (♭? p₂) ∣′
                                                              ⊛-in-terms-of->>= (return⋆ (flatten fs)) (D t (♭? p₂)) ⟩
     D t (♭? p₁) ⊛″ ♭? p₂ ∣
-    return⋆ (flatten fs) ⊛″ D t (♭? p₂)                   ≅⟨ (D t (♭? p₁) ⊛″ ♭? p₂ ∎) ∣′
-                                                             ([ ○ - ○ - ○ - ○ ] return⋆ (flatten fs) ∎ >>= λ f →
-                                                                                sym $ lemma t f) ⟩
+    return⋆ (flatten fs) ⊛″ D t (♭? p₂)                   ≅⟨ _ ∎ ⟩
+
     D t (♭? p₁) >>= pam (♭? p₂) ∣
     return⋆ (flatten fs) >>= (λ f → D t (pam (♭? p₂) f))  ≅⟨ sym $ D->>= (♭? p₁) (pam (♭? p₂)) ⟩
 
     D t (♭? p₁ >>= pam (♭? p₂))                           ∎)
-  where
-  lemma : ∀ t (f : R₁ → R₂) →
-          D t (♭? p₂ >>= λ x → return (f x)) ≅P
-          D t (♭? p₂) >>= λ x → return (f x)
-  lemma t f =
-    D t (pam (♭? p₂) f)                    ≅⟨ D->>= (♭? p₂) (return ∘ f) ⟩
-
-    pam (D t (♭? p₂)) f ∣
-    (return⋆ (flatten xs) >>= λ _ → fail)  ≅⟨ (pam (D t (♭? p₂)) f ∎) ∣′
-                                              Monad.right-zero (return⋆ (flatten xs)) ⟩
-    pam (D t (♭? p₂)) f ∣ fail             ≅⟨ AdditiveMonoid.right-identity (pam (D t (♭? p₂)) f) ⟩
-    pam (D t (♭? p₂)) f                    ∎
-
--- We can then reduce all the laws to corresponding laws for _>>=_.
 
 -- The zero laws have already been proved.
 
@@ -107,9 +189,8 @@ left-distributive : ∀ {Tok R₁ R₂ fs xs₁ xs₂}
                     p₁ ⊛ (p₂ ∣ p₃) ≅P p₁ ⊛ p₂ ∣ p₁ ⊛ p₃
 left-distributive p₁ p₂ p₃ =
   p₁ ⊛  (p₂ ∣ p₃)                     ≅⟨ ⊛-in-terms-of->>= p₁ (p₂ ∣ p₃) ⟩
-  p₁ ⊛″ (p₂ ∣ p₃)                     ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
-                                            Monad.right-distributive p₂ p₃ (return ∘ f)) ⟩
-  (p₁ >>= λ f → pam p₂ f ∣ pam p₃ f)  ≅⟨ Monad.left-distributive p₁ (pam p₂) (pam p₃) ⟩
+  p₁ ⊛″ (p₂ ∣ p₃)                     ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ _ → <$>.left-distributive) ⟩
+  (p₁ >>= λ f → f <$> p₂ ∣ f <$> p₃)  ≅⟨ Monad.left-distributive p₁ (pam p₂) (pam p₃) ⟩
   p₁ ⊛″ p₂ ∣ p₁ ⊛″ p₃                 ≅⟨ sym $ ⊛-in-terms-of->>= p₁ p₂ ∣′
                                                ⊛-in-terms-of->>= p₁ p₃ ⟩
   p₁ ⊛  p₂ ∣ p₁ ⊛  p₃                 ∎
@@ -134,15 +215,15 @@ identity : ∀ {Tok R xs} (p : Parser Tok R xs) → return id ⊛ p ≅P p
 identity p =
   return id ⊛  p  ≅⟨ ⊛-in-terms-of->>= (return id) p ⟩
   return id ⊛″ p  ≅⟨ Monad.left-identity id (pam p) ⟩
-  p >>= return    ≅⟨ Monad.right-identity p ⟩
+  id <$> p        ≅⟨ <$>.identity ⟩
   p               ∎
 
 homomorphism : ∀ {Tok R₁ R₂} (f : R₁ → R₂) (x : R₁) →
                return f ⊛ return x ≅P return {Tok = Tok} (f x)
 homomorphism f x =
   return f ⊛  return x  ≅⟨ ⊛-in-terms-of->>= (return f) (return x) ⟩
   return f ⊛″ return x  ≅⟨ Monad.left-identity f (pam (return x)) ⟩
-  pam (return x) f      ≅⟨ Monad.left-identity x (return ∘ f) ⟩
+  f <$> return x        ≅⟨ <$>.homomorphism ⟩
   return (f x)          ∎
 
 private
@@ -160,48 +241,41 @@ private
     p₃ ⊛  p₄  ≅⟨ ⊛-in-terms-of->>= p₃ p₄ ⟩
     p₃ ⊛″ p₄  ∎
 
-  pam-lemma : ∀ {Tok R₁ R₂ R₃ xs} {g : R₂ → List R₃}
-              (p₁ : Parser Tok R₁ xs) (f : R₁ → R₂)
-              (p₂ : (x : R₂) → Parser Tok R₃ (g x)) →
-              pam p₁ f >>= p₂ ≅P p₁ >>= λ x → p₂ (f x)
-  pam-lemma p₁ f p₂ =
-    pam p₁ f >>= p₂                     ≅⟨ sym $ Monad.associative p₁ (return ∘ f) p₂ ⟩
-    (p₁ >>= λ x → return (f x) >>= p₂)  ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ x →
-                                              Monad.left-identity (f x) p₂) ⟩
-    (p₁ >>= λ x → p₂ (f x))             ∎
-
 composition :
   ∀ {Tok R₁ R₂ R₃ fs gs xs}
   (p₁ : Parser Tok (R₂ → R₃) fs)
   (p₂ : Parser Tok (R₁ → R₂) gs)
   (p₃ : Parser Tok R₁        xs) →
   return _∘′_ ⊛ p₁ ⊛ p₂ ⊛ p₃ ≅P p₁ ⊛ (p₂ ⊛ p₃)
 composition p₁ p₂ p₃ =
-  return _∘′_ ⊛  p₁ ⊛  p₂ ⊛  p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁ ⊛ p₂) p₃ ⟩
-  return _∘′_ ⊛  p₁ ⊛  p₂ ⊛″ p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁) p₂ ⊛-cong (p₃ ∎) ⟩
-  return _∘′_ ⊛  p₁ ⊛″ p₂ ⊛″ p₃                   ≅⟨ ⊛-in-terms-of->>= (return _∘′_) p₁ ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
-  return _∘′_ ⊛″ p₁ ⊛″ p₂ ⊛″ p₃                   ≅⟨ Monad.left-identity _∘′_ (pam p₁) ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
-  pam p₁ _∘′_ ⊛″ p₂ ⊛″ p₃                         ≅⟨ pam-lemma p₁ _∘′_ (pam p₂) ⊛-cong (p₃ ∎) ⟩
-  ((p₁ >>= λ f → pam p₂ (_∘′_ f)) ⊛″ p₃)          ≅⟨ sym $ Monad.associative p₁ (λ f → pam p₂ (_∘′_ f)) (pam p₃) ⟩
-  (p₁ >>= λ f → pam p₂ (_∘′_ f) >>= pam p₃)       ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
-                                                      pam-lemma p₂ (_∘′_ f) (pam p₃)) ⟩
-  (p₁ >>= λ f → p₂ >>= λ g → pam p₃ (f ∘′ g))     ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
-                                                      [ ○ - ○ - ○ - ○ ] p₂ ∎ >>= λ g →
-                                                      sym $ pam-lemma p₃ g (return ∘ f)) ⟩
-  (p₁ >>= λ f → p₂ >>= λ g → pam (pam p₃ g) f)    ≅⟨ ([ ○ - ○ - ○ - ○ ] p₁ ∎ >>= λ f →
-                                                      Monad.associative p₂ (pam p₃) (return ∘ f)) ⟩
-  p₁ ⊛″ (p₂ ⊛″ p₃)                                ≅⟨ sym $ (p₁ ∎) ⊛-cong ⊛-in-terms-of->>= p₂ p₃ ⟩
-  p₁ ⊛″ (p₂ ⊛  p₃)                                ≅⟨ sym $ ⊛-in-terms-of->>= p₁ (p₂ ⊛ p₃) ⟩
-  p₁ ⊛  (p₂ ⊛  p₃)                                ∎
+  return _∘′_ ⊛  p₁ ⊛  p₂ ⊛  p₃                          ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁ ⊛ p₂) p₃ ⟩
+  return _∘′_ ⊛  p₁ ⊛  p₂ ⊛″ p₃                          ≅⟨ ⊛-in-terms-of->>= (return _∘′_ ⊛ p₁) p₂ ⊛-cong (p₃ ∎) ⟩
+  return _∘′_ ⊛  p₁ ⊛″ p₂ ⊛″ p₃                          ≅⟨ ⊛-in-terms-of->>= (return _∘′_) p₁ ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
+  return _∘′_ ⊛″ p₁ ⊛″ p₂ ⊛″ p₃                          ≅⟨ Monad.left-identity _∘′_ (pam p₁) ⊛-cong (p₂ ∎) ⊛-cong (p₃ ∎) ⟩
+  _∘′_ <$> p₁ ⊛″ p₂ ⊛″ p₃                                ≅⟨ _ ∎ ⟩
+  (_∘′_ <$> p₁ >>= _<$> p₂) >>= _<$> p₃                  ≅⟨ ([ ○ - ○ - ○ - ○ ] sym <$>.>>=-∘ >>= λ _ → _ ∎) ⟩
+  (p₁ >>= λ f → (f ∘′_) <$> p₂) >>= _<$> p₃              ≅⟨ sym $ Monad.associative _ _ _ ⟩
+  (p₁ >>= λ f → (f ∘′_) <$> p₂ >>= _<$> p₃)              ≅⟨ ([ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ → sym <$>.>>=-∘) ⟩
+  (p₁ >>= λ f → p₂ >>= λ g → (f ∘′ g) <$> p₃)            ≅⟨ ([ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ →
+                                                             [ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ →
+                                                             <$>.composition) ⟩
+  (p₁ >>= λ f → p₂ >>= λ g → f <$> (g <$> p₃))           ≅⟨ ([ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ →
+                                                             [ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ →
+                                                             <$>.in-terms-of->>=) ⟩
+  (p₁ >>= λ f → p₂ >>= λ g → g <$> p₃ >>= (return ∘ f))  ≅⟨ ([ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ → Monad.associative _ _ _) ⟩
+  (p₁ >>= λ f → p₂ >>= _<$> p₃ >>= (return ∘ f))         ≅⟨ ([ ○ - ○ - ○ - ○ ] _ ∎ >>= λ _ → sym <$>.in-terms-of->>=) ⟩
+  (p₁ >>= λ f → f <$> (p₂ >>= _<$> p₃))                  ≅⟨ _ ∎ ⟩
+  p₁ ⊛″ (p₂ ⊛″ p₃)                                       ≅⟨ sym $ (p₁ ∎) ⊛-cong ⊛-in-terms-of->>= p₂ p₃ ⟩
+  p₁ ⊛″ (p₂ ⊛  p₃)                                       ≅⟨ sym $ ⊛-in-terms-of->>= p₁ (p₂ ⊛ p₃) ⟩
+  p₁ ⊛  (p₂ ⊛  p₃)                                       ∎
 
 interchange : ∀ {Tok R₁ R₂ fs}
               (p : Parser Tok (R₁ → R₂) fs) (x : R₁) →
               p ⊛ return x ≅P return (λ f → f x) ⊛ p
 interchange p x =
   p ⊛  return x               ≅⟨ ⊛-in-terms-of->>= p (return x) ⟩
-  p ⊛″ return x               ≅⟨ ([ ○ - ○ - ○ - ○ ] p ∎ >>= λ f →
-                                    Monad.left-identity x (return ∘ f)) ⟩
-  (p >>= λ f → return (f x))  ≅⟨ pam p (λ f → f x) ∎ ⟩
-  pam p (λ f → f x)           ≅⟨ sym $ Monad.left-identity (λ f → f x) (pam p) ⟩
+  p ⊛″ return x               ≅⟨ ([ ○ - ○ - ○ - ○ ] p ∎ >>= λ _ → <$>.homomorphism) ⟩
+  (p >>= λ f → return (f x))  ≅⟨ sym <$>.in-terms-of->>= ⟩
+  (λ f → f x) <$> p           ≅⟨ sym $ Monad.left-identity (λ f → f x) (pam p) ⟩
   return (λ f → f x) ⊛″ p     ≅⟨ sym $ ⊛-in-terms-of->>= (return (λ f → f x)) p ⟩
   return (λ f → f x) ⊛  p     ∎