Vec.ced

module Vec.

import Nat.
import Id.
import IFixIndM.
import VecF.
import List.

Vec ◂ ★ ➔ Nat ➔ ★ = λ A : ★. λ n : Nat. IFixIndM · Nat · (VecF · A) (imapV · A) n.
nilV ◂ ∀ A : ★. Vec · A zero
  = Λ A. iinIndM · Nat · (VecF · A) -(imapV · A) -zero
  (nilVF · A · (Vec · A)).
consV ◂ ∀ A : ★. ∀ n : Nat. A ➔ Vec · A n ➔ Vec · A (suc n)
  = Λ A. Λ n. λ a. λ xs. iinIndM · Nat · (VecF · A) -(imapV · A) -(suc n)
  (consVF · A · (Vec · A) -n a xs).

elimVec ◂ ∀ A : ★. ∀ P : Π n : Nat. Vec · A n ➔ ★.
  P zero (nilV · A) ➔
  (∀ n : Nat. Π a : A. Π xs : Vec · A n. P n xs ➔ P (suc n) (consV · A -n a xs)) ➔
  ∀ n : Nat. Π xs : Vec · A n. P n xs
  = Λ A. Λ P. λ pN. λ pC. iinductionM · Nat · (VecF · A) -(imapV · A) · P
  (Λ R. Λ c. λ ih. elimVecF · A · R
    · (λ n : Nat. λ s : VecF · A · R n. P n (iinIndM · Nat · (VecF · A) -(imapV · A) -n
        (elimId · (VecF · A · R n) · (VecF · A · (Vec · A) n)
          (imapV · A · R · (Vec · A) c -n) s)
      ))
    pN
    (Λ n . λ a. λ r. pC -n a (elimId~ · (R n) · (Vec · A n) -(c -n) r) (ih -n r))
  ).
foldVec ◂ ∀ A : ★. ∀ C : Nat ➔ ★.
  C zero ➔
  (∀ n : Nat. A ➔ Vec · A n ➔ C n ➔ C (suc n)) ➔
  ∀ n : Nat. Vec · A n ➔ C n
  = Λ A. Λ C. elimVec · A · (λ n : Nat. λ xs : Vec · A n. C n).

v2lPres ◂ ∀ A : ★. ∀ n : Nat. Π xs : Vec · A n. {n ≃ len xs}
  = Λ A. elimVec · A · (λ n : Nat. λ xs : Vec · A n. {n ≃ len xs})
  β
  (Λ n. λ x. λ xs. λ ih. ρ ih - β)
.