qiitVec

-- 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 : El ℕ → U
             ; vnil : El (V Z)
             ; vcons : (n : El ℕ) → El a → El (V n) → El (V (S n)) )

-- the GENERIC FOLD: one dependent elimination for every carrier and
-- every result code
def vfold : (a : 𝕌) (b : 𝕌) (z : El b) (c : El a → El b → El b)
            (n : El ℕ) → El (V a n) → El b ≔
  λ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
def vlen : (a : 𝕌) (n : El ℕ) → El (V a n) → ℕ ≔
  λa. λn. λv. vfold _ _ Z (λx. λih. S ih) n v

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

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

def single : El (V _ (S Z)) ≔ vcons _ Z (S (S (S Z))) (vnil _)

def vsumSingle : vsum (S Z) single ≡ S (S (S Z)) ∈ _ ≔ ⋆
def vlenSingle : vlen ℕ (S Z) single ≡ S Z ∈ _ ≔ ⋆