def0 Vec : 0.ℕ → 0.★₀ → ★₀ =
  λ n A ⇒
  caseω n return ★₀ of {
    zero           ⇒ {nil};
    succ _, 0.Tail ⇒ A × Tail
  };

def0 List : 0.★₀ → ★₀ =
  λ A ⇒ (len : ℕ) × Vec len A;


defω nil : 0.(A : ★₀) → List A =
  λ A ⇒ (0, 'nil);

defω S : 1.ℕ → ℕ = λ n ⇒ succ n;

defω cons : 0.(A : ★₀) → 1.A → 1.(List A) → List A =
  λ A x xs ⇒
  case1 xs return List A of {
    (len, elems) ⇒ (succ len, x, elems)
  };

{-
-- needs coercions overall,
-- and real w-types to be linear
defω list-ind :
    0.(A : ★₀) →
    0.(P : ω.(List A) → ★₀) →
    1.(n : P (nil A)) →
    ω.(c : 1.(x : A) → 0.(xs : List A) → 1.(P xs) → P (cons A x xs)) →
    1.(lst : List A) → P lst =
  λ A P n c lst ⇒
    case1 lst return l ⇒ P l of {
      (len, elems) ⇒
        case1 len return len' ⇒ P (len', elems) of {
          zero ⇒ n;
          succ len', 1.ih ⇒
            case1 elems return P (succ len', elems) of {
              (first, rest) ⇒ c first rest ih
            }
        }
    };

defω foldr :
    0.(A : ★₀) → 0.(B : ★₀) →
    1.(n : B) → ω.(c : 1.A → 1.B → B) →
    1.(List A) → B =
  λ A B n c lst ⇒ list-ind A (λ _ ⇒ B) n (λ a as b ⇒ c a b) lst;

-- ...still does
defω foldr :
    0.(A : ★₀) → 0.(B : ★₀) →
    ω.(n : B) → ω.(c : 1.A → 1.B → B) →
    ω.(List A) → B =
  λ A B n c lst ⇒
    caseω lst return B of {
      (len, elems) ⇒
        caseω len return B of {
          zero ⇒ caseω elems return B of { 'nil ⇒ n };
          succ _, ω.ih ⇒
            caseω elems return B of {
              (first, rest) ⇒ c first ih
            }
        }
    };
-}

defω plus : 1.ℕ → 1.ℕ → ℕ =
  λ m n ⇒
  case1 m return ℕ of {
    zero         ⇒ n;
    succ _, 1.mn ⇒ succ mn
  };

-- case-ℕ's qout needs to be Σz + ωΣs

def0 plus-3-3 : plus 3 3 ≡ 6 : ℕ =
  δ 𝑖 ⇒ 6;

{-
defω sum : ω.(List ℕ) → ℕ = foldr ℕ ℕ 0 plus;

defω numbers : List ℕ =
  (5, (0, 1, 2, 3, 4, 'nil));

defω number-sum : sum numbers ≡ 10 : ℕ =
  δ _ ⇒ 10;
-}