[Tried using uncurried functions, but this was awkward.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>*-20080302230339] hunk ./MultiComposition.agda 75
-right-assoc (t₁ ∷ ts₁) f g h = {! !}
+right-assoc (t₁ ∷ ts₁) f g h = ≡-ext \x -> right-assoc ts₁ f g (h x)
hunk ./MultiComposition.agda 68
-f ⟪ ts₁ ⟫' g = uncurry ts₁ (curry f ⟪ ts₁ ⟫ g)
+f ⟪ ts₁ ⟫' g = merge ts₁ (f ⟪ ts₁ ⟫ g)
+
+-- This function is more obviously related to _⟪_⟫_, but the use of
+-- substitutivity makes it harder to prove things about it.
+-- Furthermore _⟪_⟫'_ above has the same computational behaviour as
+-- _⟪_⟫_.
+--
+-- _⟪_⟫'_ : forall {a b ts₂} ->
+--          (a -> Fun ts₂ b) -> (ts₁ : TypeList) ->
+--          Fun ts₁ a -> Fun (ts₁ ++ ts₂) b
+-- f ⟪ ts₁ ⟫' g = ≡₁-subst (lemma ts₁) (f ⟪ ts₁ ⟫ g)
hunk ./MultiComposition.agda 65
+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)
+
hunk ./MultiComposition.agda 57
-f ⟪ ts ⟫ g = \p -> f (g p)
+f ⟪ []     ⟫ g = f g
+f ⟪ a ∷ as ⟫ g = \x -> f ⟪ as ⟫ g x
hunk ./MultiComposition.agda 40
-curry : forall {a ts b} -> Fun (a ∷ ts) b -> (a -> Fun ts b)
-curry f = \x p -> f (x , p)
-
-uncurry : forall ts₁ {ts₂ b} ->
-          Fun ts₁ (Fun ts₂ b) -> Fun (ts₁ ++ ts₂) b
-uncurry []        f = \p -> f tt p
-uncurry (t ∷ ts₁) f = \p -> uncurry ts₁ (curry f (proj₁ p)) (proj₂ p)
+lemma : forall {a} ts₁ {ts₂} ->
+        Fun ts₁ (Fun ts₂ a) ≡₁ Fun (ts₁ ++ ts₂) a
+lemma []        = ≡₁-refl
+lemma (t ∷ ts₁) = ≡₁-ext \_ -> lemma ts₁
hunk ./MultiComposition.agda 34
-Fun ts b = Prod ts -> b
+Fun []       b = b
+Fun (a ∷ as) b = a -> Fun as b
hunk ./MultiComposition.agda 29
-Prod : TypeList -> Set
-Prod []       = ⊤
-Prod (a ∷ as) = a × Prod as
-
hunk ./MultiComposition.agda 17
-open import Data.Unit
-open import Data.Product.Record hiding (curry; uncurry)