[Stated the right associativity lemma using casts.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080306014158
 + This made both the statement and the proof more complex.
] hunk ./MultiComposition.agda 17
+open import Relation.Binary.PropositionalEquality1
hunk ./MultiComposition.agda 52
--- Note the similarity between merge and split...
-
-merge : forall {a} ts₁ {ts₂} ->
-        Fun ts₁ (Fun ts₂ a) -> Fun (ts₁ ++₁ ts₂) a
-merge []₁        f = f
-merge (t ∷₁ ts₁) f = \x -> merge ts₁ (f x)
-
-split : forall {a} ts₁ {ts₂} ->
-        Fun (ts₁ ++₁ ts₂) a -> Fun ts₁ (Fun ts₂ a)
-split []₁        f = f
-split (t ∷₁ ts₁) f = \x -> split ts₁ (f x)
+-- The right associativity theorem is parameterised on some equality
+-- proofs (used to state the theorem) in order to increase
+-- flexibility.
hunk ./MultiComposition.agda 57
-              (f : a -> b) (g : Fun (t ∷₁ ts₂) a) (h : Fun ts₁ t) ->
-              (f ⟪ t ∷₁ ts₂ ⟫ g) ⟪ ts₁ ⟫ h ≡
-              split ts₁ (f ⟪ ts₁ ++₁ ts₂ ⟫ (merge ts₁ (g ⟪ ts₁ ⟫ h)))
-right-assoc []₁         ts₂ f g h = ≡-refl
-right-assoc (t₁ ∷₁ ts₁) ts₂ f g h =
-  ≡-ext \x -> right-assoc ts₁ ts₂ f g (h x)
+              (f : a -> b) (g : Fun (t ∷₁ ts₂) a) (h : Fun ts₁ t)
+
+              (eq₁ : Fun ts₁ (Fun ts₂ a) ≡₁ Fun (ts₁ ++₁ ts₂) a)
+              (eq₂ : Fun (ts₁ ++₁ ts₂) b ≡₁ Fun ts₁ (Fun ts₂ b)) ->
+
+              let c₁ = ≡₁-subst eq₁; c₂ = ≡₁-subst eq₂ in
+
+                 (f ⟪ t    ∷₁ ts₂ ⟫      g) ⟪ ts₁ ⟫ h    ≡
+              c₂ (f ⟪ ts₁ ++₁ ts₂ ⟫ (c₁ (g  ⟪ ts₁ ⟫ h)))
+
+right-assoc []₁         ts₂ f g h ≡₁-refl ≡₁-refl = ≡-refl
+right-assoc (t₁ ∷₁ ts₁) ts₂ f g h eq₁     eq₂     =
+  ≡-trans (≡-ext \x ->
+             right-assoc ts₁ ts₂ f g (h x)
+                         (Fun-lemma ts₁) (≡₁-sym (Fun-lemma ts₁)))
+          (helper (\g -> f ⟪ ts₁ ++₁ ts₂ ⟫ g) (\x' -> g ⟪ ts₁ ⟫ h x')
+                  (Fun-lemma ts₁) (≡₁-sym (Fun-lemma ts₁)) eq₁ eq₂)
+  where
+  helper : forall {a b b' c c'} (f : b' -> c) (g : a -> b)
+                  (eq₁' : b ≡₁ b') (eq₂' : c ≡₁ c')
+                  (eq₁ : (a -> b) ≡₁ (a -> b'))
+                  (eq₂ : (a -> c) ≡₁ (a -> c')) ->
+    (\x -> ≡₁-subst eq₂' (f (≡₁-subst eq₁' (g x)))) ≡
+    ≡₁-subst eq₂ (\x -> f (≡₁-subst eq₁ g x))
+  helper f g ≡₁-refl ≡₁-refl ≡₁-refl ≡₁-refl = ≡-refl