[Proved various laws for const⋆.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101217213659
 Ignore-this: ce180baedd47bf7d9e463a93c8bbe311
] hunk ./ReverseComposition.agda 422
+  -- _⊙_ distributes from the left over _⊙∥_.
+
+  ⊙-⊙∥ : ∀ {As Bs} {C D E : Set ℓ}
+         (f : As ⇨ C) (g : C ∷ Bs ⇨ D) (h : D ∷ C ∷ Bs ⇨ E) →
+         f ⊙ (g ⊙∥ h) ≈ (f ⊙ g) ⊙∥ Λ (λ x → f ⊙ h · x)
+  ⊙-⊙∥ {[]}     x g h = refl _
+  ⊙-⊙∥ {A ∷ As} f g h = Λ-cong λ x → ⊙-⊙∥ (f · x) g h
+
hunk ./ReverseComposition.agda 446
+  const⋆-const⋆ : ∀ As Bs {Cs} {D : Set ℓ} (f : Cs ⇨ D) →
+                  const⋆ As (const⋆ Bs f) ≈ const⋆ (As ++ Bs) f
+  const⋆-const⋆ []       Bs f = refl (const⋆ Bs f)
+  const⋆-const⋆ (A ∷ As) Bs f = Λ-cong (λ _ → const⋆-const⋆ As Bs f)
+
hunk ./ReverseComposition.agda 632
+  const⋆-cong : ∀ As {Bs} {C : Set ℓ} {f₁ f₂ : Bs ⇨ C} →
+                f₁ ≈ f₂ → const⋆ As f₁ ≈ const⋆ As f₂
+  const⋆-cong As f₁≈f₂ =
+    refl (return∥ {As = As} (lift tt)) >>=-cong′ λ _ → f₁≈f₂
+    where open MonadLaws
+
hunk ./ReverseComposition.agda 664
+  -- const⋆ distributes over various operations.
+
+  const⋆-map : ∀ As {Bs} {C D : Set ℓ} (f : C → D) (g : Bs ⇨ C) →
+               const⋆ As (map f g) ≈ map f (const⋆ As g)
+  const⋆-map As f g =
+    const⋆ As (map f g)                              ≡⟨ P.refl ⟩
+    return∥ {As = As} (lift tt) ⊙ map f (Λ λ _ → g)  ≈⟨ sym $ map-⊙ f (return∥ {As = As} (lift tt)) (Λ λ _ → g) ⟩
+    map f (return∥ {As = As} (lift tt) ⊙ Λ λ _ → g)  ≡⟨ P.refl ⟩
+    map f (const⋆ As g)                              ∎
+
+  const⋆->>=∥ : ∀ As {Bs} {C D : Set ℓ} (f : Bs ⇨ C) (g : C → Bs ⇨ D) →
+               const⋆ As (f >>=∥ g) ≈ const⋆ As f >>=∥ const⋆ As ∘ g
+  const⋆->>=∥ As f g =
+    const⋆ As (f >>=∥ g)                                 ≡⟨ P.refl ⟩
+    return∥ {As = As} (lift tt) >>= const (f >>=∥ g)     ≈⟨ ⊙-⊙∥ (return∥ {As = As} (lift tt)) (Λ λ _ → f) (Λ λ x → Λ λ _ → g x) ⟩
+    (return∥ {As = As} (lift tt) >>= const f >>=∥ λ x →
+     return∥ {As = As} (lift tt) >>= const (g x))        ≡⟨ P.refl ⟩
+    const⋆ As f >>=∥ const⋆ As ∘ g                       ∎
+
+  const⋆-⊛∥ : ∀ As {Bs} {C D : Set ℓ} (f : Bs ⇨ (C → D)) (g : Bs ⇨ C) →
+              const⋆ As (f ⊛∥ g) ≈ const⋆ As f ⊛∥ const⋆ As g
+  const⋆-⊛∥ As f g =
+    const⋆ As (f ⊛∥ g)                            ≡⟨ P.refl ⟩
+    const⋆ As (f >>=∥ λ f → map f g)              ≈⟨ const⋆->>=∥ As f (λ f → map f g) ⟩
+    const⋆ As f >>=∥ (λ f → const⋆ As (map f g))  ≈⟨ (refl (const⋆ As f) >>=∥-cong′ λ f → const⋆-map As f g) ⟩
+    const⋆ As f >>=∥ (λ f → map f (const⋆ As g))  ≡⟨ P.refl ⟩
+    const⋆ As f ⊛∥ const⋆ As g                    ∎
+    where open MonadLaws∥
+