[Converted Wand to the new _⟪_⟫_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080306162646] hunk ./Wand.agda 12
-         (≡₁-ext : forall {a : Set} {f g : a -> Set} ->
-                     (forall x -> f x ≡₁ g x) ->
-                     ((x : a) -> f x) ≡₁ ((x : a) -> g x))
hunk ./Wand.agda 17
-open MC ≡-ext ≡₁-ext
+open MC ≡-ext
+open TypeList using (_→_)
hunk ./Wand.agda 21
-open import Data.List
-open import Data.List1
hunk ./Wand.agda 101
-      E e₁ ⟪ K ∷₁ []₁ ⟫ (\κ v₁ -> E e₂ (\v₂ -> κ (v₁ + v₂)))
+      E e₁ ⟪ K ◅ ε ⟫ (\κ v₁ -> E e₂ (\v₂ -> κ (v₁ + v₂)))
hunk ./Wand.agda 103
-      E e₁ ⟪ K ∷₁ []₁ ⟫ (E e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
-        ≡⟨ proof (E'P e₁) ⟪ K ∷₁ []₁ ⟫-cong
-             (proof (E'P e₂) ⟪ K ∷₁ V ∷₁ []₁ ⟫-cong ≡-refl) ⟩
-      E' e₁ ⟪ K ∷₁ []₁ ⟫ (E' e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
+      E e₁ ⟪ K ◅ ε ⟫ (E e₂ ⟪ K ◅ V ◅ ε ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
+        ≡⟨ proof (E'P e₁) ⟪ K ◅ ε ⟫-cong
+             (proof (E'P e₂) ⟪ K ◅ V ◅ ε ⟫-cong ≡-refl) ⟩
+      E' e₁ ⟪ K ◅ ε ⟫ (E' e₂ ⟪ K ◅ V ◅ ε ⟫ (\κ v₁ v₂ -> κ (v₁ + v₂)))
hunk ./Wand.agda 108
-      E' e₁ ⟪ K ∷₁ []₁ ⟫ (E' e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ add)
+      E' e₁ ⟪ K ◅ ε ⟫ (E' e₂ ⟪ K ◅ V ◅ ε ⟫ add)
hunk ./Wand.agda 125
-      E e ⟪ []₁ ⟫ (\v σ -> v)
-        ≡⟨ proof (E'P e) ⟪ []₁ ⟫-cong ≡-refl ⟩
-      E' e ⟪ []₁ ⟫ halt
+      E e ⟪ ε ⟫ (\v σ -> v)
+        ≡⟨ proof (E'P e) ⟪ ε ⟫-cong ≡-refl ⟩
+      E' e ⟪ ε ⟫ halt
hunk ./Wand.agda 138
-            Exp' (a -> b) -> Exp' (Fun ts a) -> Exp' (Fun ts b)
+            Exp' (a -> b) -> Exp' (ts → a) -> Exp' (ts → b)
hunk ./Wand.agda 156
-    B (K ∷₁ []₁) (comp e₁) (B (K ∷₁ V ∷₁ []₁) (comp e₂) add)
+    B (K ◅ ε) (comp e₁) (B (K ◅ V ◅ ε) (comp e₂) add)
hunk ./Wand.agda 197
-      {witness = B (K ∷₁ []₁) (comp' e₁) (B (K ∷₁ V ∷₁ []₁) (comp' e₂) add)}
+      {witness = B (K ◅ ε) (comp' e₁) (B (K ◅ V ◅ ε) (comp' e₂) add)}
hunk ./Wand.agda 199
-        Step₁.E' e₁ ⟪ K ∷₁ []₁ ⟫ (Step₁.E' e₂ ⟪ K ∷₁ V ∷₁ []₁ ⟫ Step₁.add)
+        Step₁.E' e₁ ⟪ K ◅ ε ⟫ (Step₁.E' e₂ ⟪ K ◅ V ◅ ε ⟫ Step₁.add)
hunk ./Wand.agda 204
-        ⟦ B (K ∷₁ []₁) (comp' e₁) (B (K ∷₁ V ∷₁ []₁) (comp' e₂) add) ⟧
+        ⟦ B (K ◅ ε) (comp' e₁) (B (K ◅ V ◅ ε) (comp' e₂) add) ⟧
hunk ./Wand.agda 226
-    B     : forall {a b} ts {f : a -> b} {g : Fun ts a} ->
+    B     : forall {a b} ts {f : a -> b} {g : ts → a} ->
hunk ./Wand.agda 242
-    B (K ∷₁ []₁) (comp e₁) (B (K ∷₁ V ∷₁ []₁) (comp e₂) add)
+    B (K ◅ ε) (comp e₁) (B (K ◅ V ◅ ε) (comp e₂) add)
hunk ./Wand.agda 265
-  fig2b = B []₁ l halt
+  fig2b = B ε l halt
hunk ./Wand.agda 268
-    llr = B (K ∷₁ V ∷₁ []₁) (fetch Y) add
+    llr = B (K ◅ V ◅ ε) (fetch Y) add
hunk ./Wand.agda 271
-    ll = B (K ∷₁ []₁) (fetch X) llr
+    ll = B (K ◅ ε) (fetch X) llr
hunk ./Wand.agda 274
-    lr = B (K ∷₁ V ∷₁ []₁) (fetch Z) add
+    lr = B (K ◅ V ◅ ε) (fetch Z) add
hunk ./Wand.agda 277
-    l = B (K ∷₁ []₁) ll lr
+    l = B (K ◅ ε) ll lr
hunk ./Wand.agda 282
-  fig2c = B []₁ (fetch X) step₂
+  fig2c = B ε (fetch X) step₂
hunk ./Wand.agda 288
-    step₅ = B []₁ add step₆
+    step₅ = B ε add step₆
hunk ./Wand.agda 291
-    step₄ = B (V ∷₁ []₁) (fetch Z) step₅
+    step₄ = B (V ◅ ε) (fetch Z) step₅
hunk ./Wand.agda 294
-    step₃ = B []₁ add step₄
+    step₃ = B ε add step₄
hunk ./Wand.agda 297
-    step₂ = B (V ∷₁ []₁) (fetch Y) step₃
+    step₂ = B (V ◅ ε) (fetch Y) step₃
hunk ./Wand.agda 303
-  infixr 5 _^_→_
-
-  -- This type constructor is used by Wand to represent a stack:
-
-  _^_→_ : Set -> ℕ -> Set -> Set
-  A ^ n → B = Fun (replicate₁ n A) B
-
hunk ./Wand.agda 305
-  shift₀ :  forall {A B} n
-         -> A ^ suc n → B
-         -> A ^ n     → (A -> B)
-  shift₀ zero    f = f
-  shift₀ (suc n) f = \x -> shift₀ n (f x)
+  shift₀ : forall {A B} n ->
+           A ^ suc n      →  B  ≡₁
+           A ^ n     → (A -> B)
+  shift₀         zero    = ≡₁-refl
+  shift₀ {A = A} (suc n) = ≡₁-cong (\t -> A -> t) (shift₀ n)
hunk ./Wand.agda 311
-  shift :  forall {A B} m n
-        -> A ^ suc m +     n → B
-        -> A ^ m     + suc n → B
-  shift zero    n f = f
-  shift (suc m) n f = \x -> shift m n (f x)
+  shift₀' : forall {A B} {C : Set} n ->
+            (C -> A ^ suc n      →  B)  ≡₁
+            (C -> A ^ n     → (A -> B))
+  shift₀' {C = C} n = ≡₁-cong (\t -> C -> t) (shift₀ n)
hunk ./Wand.agda 316
-  swap : forall {A B} m n
-       -> A ^ m → A ^ n → B
-       -> A ^ n + m     → B
-  swap m       zero    f = f
-  swap zero    (suc n) f = \x -> swap zero n (f x)
-  swap (suc m) (suc n) f = \x -> shift n m (swap m (suc n) (f x))
+  merge : forall {A B} m n ->
+          A ^  m → A ^ n  → B ≡₁
+          A ^ (m +     n) → B
+  merge         zero    n = ≡₁-refl
+  merge {A = A} (suc m) n = ≡₁-cong (\t -> A -> t) (merge m n)
hunk ./Wand.agda 322
-  swap-lemma : forall {A B} m n ->
-               A ^ m → A ^ n → B ≡₁
-               A ^ n + m     → B
-  swap-lemma m       zero    = ≡₁-refl
-  swap-lemma zero    (suc n) = ≡₁-ext \x -> swap-lemma zero n
-  swap-lemma (suc m) (suc n) = ≡₁-ext \x -> ≡₁-trans (swap-lemma m (suc n)) {! !}
-    -- shift n m (swap-lemma m (suc n) (f x))
+  swap : forall {A B} m n ->
+         A ^ (m + n) → B ≡₁
+         A ^ (n + m) → B
+  swap {A} {B} m n = ≡₀₁-cong (\i -> A ^ i → B) (+-comm m n)
+    where open IsCommutativeSemiring _ ℕ-isCommutativeSemiring
hunk ./Wand.agda 332
-  B′ n f g = f ⟪ K ∷₁ replicate₁ n V ⟫ \κ -> shift₀ n (g κ)
+  B′ n f g = f ⟪ K ◅ V ^ n ⟫ cast g
+    where cast = ≡₁-subst (shift₀' n)
hunk ./Wand.agda 336
-       (K -> V ^ m → C) -> (V ^ suc n → C) -> (V ^ m + n → C)
-  B″ m n f g = swap n m (f ⟪ replicate₁ n V ⟫ shift₀ n g)
+       (K -> V ^ m → C) -> (V ^ suc n → C) -> (V ^ (m + n) → C)
+  B″ m n f g = cast₂ (f ⟪ V ^ n ⟫ cast₁ g)
+    where
+    cast₁ = ≡₁-subst (shift₀ n)
+    cast₂ = ≡₁-subst (≡₁-trans (merge n m) (swap n m))
hunk ./Wand.agda 345
-  rot-lemma zero    zero    f g h = ≡-refl
-  rot-lemma zero    (suc n) f g h = ≡-ext \x -> rot-lemma zero n f g (h x)
-  rot-lemma (suc m) zero    f g h = ≡-ext \x -> {! (g h x)  !}
-  rot-lemma (suc m) (suc n) f g h = {!≡-ext \x -> rot-lemma m (suc n) f (\κ -> g κ x) h  !}