finish VecEnc

src/AOP/VecEnc.agda

@@ -43,8 +43,11 @@ cons : ∀{A n} → A → Vec A n → Vec A (suc n)
 cons x ls = ls , x
 
 {- Q3 : Give the eliminator. -}
-one-elim : ∀ {i} {P : One → Set i} (p : P one) → (o : One) → P o
-one-elim p one = p
+η× : ∀{A B} → (p : A × B) → (π1 p , π2 p) ≡ p
+η× (x , y) = refl
+
+η1 : (p : One) → one ≡ p
+η1 one = refl
 
 elim-vec :
   ∀{i A}{P : (n : ℕ) → Vec A n → Set i} → 
@@ -52,11 +55,18 @@ elim-vec :
   (∀{n} → (x : A) → (xs : Vec A n) → P n xs → P (suc n) (cons {A} {n} x xs)) → 
   ∀{n}(xs : Vec A n) → P n xs
 elim-vec {i} {A} {P} nn cc {n} xs = f xs where
-  f = iter {P = λ n → (a : Vec A n) → P n a}
-    (λ a → one-elim {P = λ x → P 0 x} nn a)
-    (λ m x a → let z = cc {n = m} {!   !} {!   !} {!   !} in {!   !}) n
+  case0 : (a : Vec A 0) → P 0 a
+  case0 a = subst (λ x → P 0 x) (η1 a) nn
+
+  casen : (m : ℕ) → ((a : Vec A m) → P m a) → (a : Vec A (suc m)) → P (suc m) a
+  casen m f a = subst (λ x → P (suc m) x) (η× a) (cc (π2 a) (π1 a) (f (π1 a)))
+
+  f = iter {P = λ n → (a : Vec A n) → P n a} case0 casen n
 
 {- Q4: Implement append using the eliminator. -}
 append : ∀{A m n} → Vec A m → Vec A n → Vec A (m + n)
-append {A} {m} {n} xs ys = elim-vec {P = λ x v → {! Vec   !}} {!   !} {!   !} {!   !}
-
+append {A} {m} {n} xs ys =
+  elim-vec {A = A} {P = λ m x → Vec A (m + n)}
+    ys
+    (λ {n = n₁} x f a → cons {A = A} {n = n₁ + n} x a)
+    {n = m} xs