Qiit.vec

-- An INDEXED sort over a PARAMETER: length-indexed vectors of any
-- carrier (external index arity over the ambient [a : 𝕌]), with
-- dependent elimination at an indexed motive — and the functions at
-- the same generality.

data [a : 𝕌]
  V : ℕ → U
  vnil : El (V Z)
  vcons : (n : ℕ) → a → El (V n) → El (V (S n))

-- the GENERIC FOLD: one dependent elimination for every carrier and
-- every result code
vfold : (a : 𝕌) {b : 𝕌} (z : b) (c : a → b → b) (n : ℕ) → V a n → b
  using (Qiit.vec.V.eq, Qiit.vec.V.unfold)
vfold = λa b z c n v. VElim a (λm w. b) z (λm x xs ih. c x ih) n v

-- generic length and an instance-level sum, both folds
vlen : (a : 𝕌) (n : ℕ) → V a n → ℕ
vlen = λa n v. vfold _ Z (λx ih. S ih) _ v

plusV : ℕ → ℕ → ℕ
plusV = λx y. ℕ-elim y (n ih. S ih) x

vsum : (n : ℕ) → V ℕ n → ℕ
vsum = λn v. vfold _ Z (λx ih. plusV x ih) _ v

single : V ℕ (S Z) using (Qiit.vec.V.eq, Qiit.vec.V.unfold)
single = vcons ℕ Z 3 (vnil ℕ)

vsumSingle : vsum _ single ≡ 3
  using (Qiit.vec.VElim.eq,
    Qiit.vec.plusV.eq,
    Qiit.vec.single.eq,
    Qiit.vec.vcons.eq,
    Qiit.vec.vfold.eq,
    Qiit.vec.vnil.eq,
    Qiit.vec.vsum.eq)
vsumSingle = ⋆

vlenSingle : vlen _ _ single ≡ S Z
  using (Qiit.vec.VElim.eq,
    Qiit.vec.single.eq,
    Qiit.vec.vcons.eq,
    Qiit.vec.vfold.eq,
    Qiit.vec.vlen.eq,
    Qiit.vec.vnil.eq)
vlenSingle = ⋆