[Simplified the right associativity statement by using difference lists.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080306134221] hunk ./MultiComposition.agda 8
-         -- Assume extensionality; it is used in proofs below.
+         -- Assume extensionality; it is used in a proof below.
hunk ./MultiComposition.agda 10
-                    (forall x -> f x ≡ g x) -> f ≡ g)
-         (≡₁-ext : forall {a : Set} {f g : a -> Set} ->
-                     (forall x -> f x ≡₁ g x) ->
-                     ((x : a) -> f x) ≡₁ ((x : a) -> g x))
-         where
+                  (forall x -> f x ≡ g x) -> f ≡ g)
+       where
hunk ./MultiComposition.agda 14
-open import Relation.Binary.PropositionalEquality1
-open import Data.List1
+open ≡-Reasoning
+open import Data.Function
hunk ./MultiComposition.agda 18
--- Turning a list of types into a function type
+-- Type lists
hunk ./MultiComposition.agda 20
--- Fun (a ∷₁ b ∷₁ c ∷₁ []₁) d ≡₁ a -> b -> c -> d.
+-- Difference lists.
hunk ./MultiComposition.agda 22
-Fun : [ Set ]₁ -> Set -> Set
-Fun []₁       b = b
-Fun (a ∷₁ as) b = a -> Fun as b
+record TypeList : Set1 where
+  field
+    Fun   : Set -> Set
+    map   : forall {a b} -> (a -> b) -> Fun a -> Fun b
hunk ./MultiComposition.agda 27
-Fun-lemma : forall {a} ts₁ {ts₂} ->
-            Fun ts₁ (Fun ts₂ a) ≡₁ Fun (ts₁ ++₁ ts₂) a
-Fun-lemma []₁        = ≡₁-refl
-Fun-lemma (t ∷₁ ts₁) = ≡₁-ext \_ -> Fun-lemma ts₁
+    -- Since extensionality is needed anyway we might as well state
+    -- functoriality in point-free form:
+
+    map-∘ : forall {a b c} (f : b -> c) (g : a -> b) ->
+            map (f ∘ g) ≡ map f ∘ map g
+
+open TypeList
+
+ε : TypeList
+ε = record
+  { Fun   = \c -> c
+  ; map   = \f as -> f as
+  ; map-∘ = \f g -> ≡-refl
+  }
+
+infixr 5 _◅_
+
+_◅_ : Set -> TypeList -> TypeList
+a ◅ bs = record
+  { Fun   = \c -> a -> Fun bs c
+  ; map   = \f k x -> map bs f (k x)
+  ; map-∘ = \f g -> ≡-ext \k -> ≡-ext \x ->
+      ≡-cong (\h -> h (k x)) (map-∘ bs f g)
+  }
+
+infixr 5 _◅▻_
+
+_◅▻_ : TypeList -> TypeList -> TypeList
+as ◅▻ bs = record
+  { Fun   = \c -> Fun as (Fun bs c)
+  ; map   = \f k -> map as (map bs f) k
+  ; map-∘ = \f g -> begin
+      map as (map bs (f ∘ g))
+        ≡⟨ ≡-cong (map as) (map-∘ bs f g) ⟩
+      map as (map bs f ∘ map bs g)
+        ≡⟨ map-∘ as (map bs f) (map bs g) ⟩
+      map as (map bs f) ∘ map as (map bs g)
+        ∎
+  }
hunk ./MultiComposition.agda 75
-        (a -> b) -> (ts : [ Set ]₁) -> Fun ts a -> Fun ts b
-f ⟪ []₁     ⟫ g = f g
-f ⟪ a ∷₁ as ⟫ g = \x -> f ⟪ as ⟫ g x
-
-_⟪_⟫-cong_ : forall {a b} {f₁ f₂ : a -> b} ->
-             f₁ ≡ f₂ ->
-             (ts : [ Set ]₁) {g₁ g₂ : Fun ts a} -> g₁ ≡ g₂ ->
-             f₁ ⟪ ts ⟫ g₁ ≡ f₂ ⟪ ts ⟫ g₂
-eqf ⟪ ts ⟫-cong eqg = ≡-cong₂ (\f g -> f ⟪ ts ⟫ g) eqf eqg
-
--- The right associativity theorem is parameterised on some equality
--- proofs (used to state the theorem) in order to increase
--- flexibility.
+        (a -> b) -> (ts : TypeList) -> Fun ts a -> Fun ts b
+f ⟪ ts ⟫ g = map ts f g
hunk ./MultiComposition.agda 79
-              (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
+              (f : a -> b) (g : Fun (t ◅ ts₂) a) (h : Fun ts₁ t) ->
+              (f ⟪ t   ◅  ts₂ ⟫  g) ⟪ ts₁ ⟫ h  ≡
+               f ⟪ ts₁ ◅▻ ts₂ ⟫ (g  ⟪ ts₁ ⟫ h)
+right-assoc ts₁ ts₂ f g h =
+  ≡-cong (\F -> F h) (map-∘ ts₁ (map ts₂ f) g)