diff --git a/stdlib/bool.quox b/stdlib/bool.quox
new file mode 100644
index 0000000..855f064
--- /dev/null
+++ b/stdlib/bool.quox
@@ -0,0 +1,49 @@
+load "misc.quox"
+
+namespace bool {
+
+def0 Bool : ★ = {true, false}
+
+def if-dep : 0.(P : Bool → ★) → (b : Bool) → ω.(P 'true) → ω.(P 'false) → P b =
+  λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f }
+
+def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A =
+  λ A ⇒ if-dep (λ _ ⇒ A)
+
+def0 if-same : (A : ★) → (b : Bool) → (x : A) → if A b x x ≡ x : A =
+  λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x)
+
+def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B =
+  λ A B ⇒ if-dep (λ b ⇒ if¹ ★ b A B)
+
+def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False
+
+def dup! : (b : Bool) → Dup Bool b =
+  λ b ⇒
+  case b return b' ⇒ Dup Bool b' of {
+    'true  ⇒ (['true],  [δ _ ⇒ ['true]]);
+    'false ⇒ (['false], [δ _ ⇒ ['false]])
+  }
+
+def dup : Bool → [ω.Bool] =
+  λ b ⇒
+    case dup! b return [ω.Bool] of {
+      (b!, p0) ⇒ drop0 (b! ≡ [b] : [ω.Bool]) [ω.Bool] p0 b!
+    }
+
+def true-not-false : Not ('true ≡ 'false : Bool) =
+  λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true
+
+
+-- [todo] infix
+def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false
+def or  : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b
+def not : Bool → Bool = λ b ⇒ if Bool b 'false 'true
+
+
+def0 not-not : (b : Bool) → not (not b) ≡ b : Bool =
+  λ b ⇒ if-dep (λ b ⇒ not (not b) ≡ b : Bool) b (δ _ ⇒ 'true) (δ _ ⇒ 'false)
+
+}
+
+def0 Bool = bool.Bool
diff --git a/stdlib/either.quox b/stdlib/either.quox
new file mode 100644
index 0000000..fa67ea2
--- /dev/null
+++ b/stdlib/either.quox
@@ -0,0 +1,116 @@
+load "misc.quox"
+load "bool.quox"
+
+namespace either {
+
+def0 Tag : ★ = {left, right}
+
+def0 Payload : ★ → ★ → Tag → ★ =
+  λ A B tag ⇒ case tag return ★ of { 'left ⇒ A; 'right ⇒ B }
+
+def0 Either : ★ → ★ → ★ =
+  λ A B ⇒ (tag : Tag) × Payload A B tag
+
+def Left : 0.(A B : ★) → A → Either A B =
+  λ A B x ⇒ ('left, x)
+
+def Right : 0.(A B : ★) → B → Either A B =
+  λ A B x ⇒ ('right, x)
+
+def elim :
+    0.(A B : ★) → 0.(P : 0.(Either A B) → ★) →
+    ω.((x : A) → P (Left  A B x)) →
+    ω.((x : B) → P (Right A B x)) →
+    (x : Either A B) → P x =
+  λ A B P f g e ⇒
+    case e return e' ⇒ P e' of { (t, a) ⇒
+      case t return t' ⇒ (a : Payload A B t') → P (t', a)
+      of { 'left ⇒ f; 'right ⇒ g } a
+    }
+
+def elimω :
+    0.(A B : ★) → 0.(P : 0.(Either A B) → ★) →
+    ω.(ω.(x : A) → P (Left  A B x)) →
+    ω.(ω.(x : B) → P (Right A B x)) →
+    ω.(x : Either A B) → P x =
+  λ A B P f g e ⇒
+    case fst e return t' ⇒ ω.(a : Payload A B t') → P (t', a)
+    of { 'left ⇒ f; 'right ⇒ g } (snd e)
+
+def fold :
+    0.(A B C : ★) → ω.(A → C) → ω.(B → C) → Either A B → C =
+  λ A B C ⇒ elim A B (λ _ ⇒ C)
+
+def foldω :
+    0.(A B C : ★) → ω.(ω.A → C) → ω.(ω.B → C) → ω.(Either A B) → C =
+  λ A B C ⇒ elimω A B (λ _ ⇒ C)
+
+
+}
+
+def0 Either = either.Either
+def  Left   = either.Left
+def  Right  = either.Right
+
+
+namespace dec {
+
+def0 Dec : ★ → ★ = λ A ⇒ Either [0.A] [0.Not A]
+
+def Yes : 0.(A : ★) → 0.A       → Dec A = λ A y ⇒ Left  [0.A] [0.Not A] [y]
+def No  : 0.(A : ★) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]
+
+def yes-refl : 0.(A : ★) → 0.(x : A) → Dec (x ≡ x : A) =
+  λ A x ⇒ Yes (x ≡ x : A) (δ 𝑖 ⇒ x)
+
+def0 DecEq : ★ → ★ =
+  λ A ⇒ ω.(x y : A) → Dec (x ≡ y : A)
+
+def elim :
+    0.(A : ★) → 0.(P : 0.(Dec A) → ★) →
+    ω.(0.(y : A)     → P (Yes A y)) →
+    ω.(0.(n : Not A) → P (No  A n)) →
+    (x : Dec A) → P x =
+  λ A P f g ⇒
+    either.elim [0.A] [0.Not A] P
+      (λ y ⇒ case y return y' ⇒ P (Left  [0.A] [0.Not A] y') of {[y'] ⇒ f y'})
+      (λ n ⇒ case n return n' ⇒ P (Right [0.A] [0.Not A] n') of {[n'] ⇒ g n'})
+
+def bool : 0.(A : ★) → Dec A → Bool =
+  λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false)
+
+def drop' : 0.(A : ★) → Dec A → True =
+  λ A ⇒ elim A (λ _ ⇒ True) (λ _ ⇒ 'true) (λ _ ⇒ 'true)
+
+def drop : 0.(A B : ★) → Dec A → B → B =
+  λ A B x y ⇒ true.drop B (drop' A x) y
+
+}
+
+def0 Dec   = dec.Dec
+def0 DecEq = dec.DecEq
+def  Yes   = dec.Yes
+def  No    = dec.No
+
+
+namespace dect {
+
+def0 DecT : ★ → ★ = λ A ⇒ Either A [0.Not A]
+
+def YesT : 0.(A : ★) → 1.A       → DecT A = λ A y ⇒ Left  A [0.Not A] y
+def NoT  : 0.(A : ★) → 0.(Not A) → DecT A = λ A n ⇒ Right A [0.Not A] [n]
+
+def elim :
+    0.(A : ★) → 0.(P : 0.(DecT A) → ★) →
+    ω.(1.(y : A)     → P (YesT A y)) →
+    ω.(0.(n : Not A) → P (NoT  A n)) →
+    (x : DecT A) → P x =
+  λ A P f g ⇒
+    either.elim A [0.Not A] P
+      f
+      (λ n ⇒ case n return n' ⇒ P (Right A [0.Not A] n') of {[n'] ⇒ g n'})
+}
+
+def0 DecT = dect.DecT
+def  YesT = dect.YesT
+def  NoT  = dect.NoT
diff --git a/stdlib/fin.quox b/stdlib/fin.quox
new file mode 100644
index 0000000..2491c90
--- /dev/null
+++ b/stdlib/fin.quox
@@ -0,0 +1,259 @@
+load "nat.quox"
+load "either.quox"
+load "maybe.quox"
+load "sub.quox"
+
+
+namespace nat.lt {
+
+def0 LT : ℕ → ℕ → ★ =
+  elim-pair¹ (λ _ _ ⇒ ★)
+    False             -- 0      ≮ 0
+    (λ   n p ⇒ True)  -- 0      < succ n
+    (λ m   p ⇒ False) -- succ m ≮ 0
+    (λ m n p ⇒ p)     -- succ m < succ n ⇔ m < n
+
+
+def0 irr : sub.Irr2 ℕ ℕ LT =
+  elim-pair (λ m n ⇒ (p q : LT m n) → p ≡ q : LT m n)
+    false.irr (λ _ _ ⇒ true.irr) (λ _ _ ⇒ false.irr) (λ _ _ p ⇒ p)
+
+
+-- [todo] quantities (which will need to inline and adapt elim-pair)
+def elimω : 0.(P : (m n : ℕ) → LT m n → ★) →
+            ω.(0.(n : ℕ) → P 0 (succ n) 'true) →
+            ω.(0.(m n : ℕ) → 0.(lt : LT m n) →
+               ω.(P m n lt) → P (succ m) (succ n) lt) →
+            ω.(m n : ℕ) → 0.(lt : LT m n) → P m n lt =
+  λ P p0s pss ⇒
+    elim-pairω (λ m n ⇒ 0.(lt : LT m n) → P m n lt)
+      (λ       ff ⇒ void (P 0 0 ff) ff)
+      (λ   n p tt ⇒ p0s n)
+      (λ m   p ff ⇒ void (P (succ m) 0 ff) ff)
+      (λ m n p tt ⇒ pss m n tt (p tt))
+
+def0 true-ty : (m n : ℕ) → LT m n → LT m n ≡ True : ★ =
+  elim-pair¹ (λ m n ⇒ LT m n → LT m n ≡ True : ★)
+    (λ       ff ⇒ void¹ (False ≡ True : ★) ff)
+    (λ   n p tt ⇒ δ _ ⇒ True)
+    (λ m   p ff ⇒ void¹ (False ≡ True : ★) ff)
+    (λ n m p tf ⇒ p tf)
+
+def0 true-val :
+    (m n : ℕ) → (lt : LT m n) → Eq (𝑖 ⇒ true-ty m n lt @𝑖) lt 'true =
+  let IsTrue : (m n : ℕ) → LT m n → ★ =
+    λ m n lt ⇒ Eq (𝑖 ⇒ true-ty m n lt @𝑖) lt 'true in
+  elim-pair (λ m n ⇒ (lt : LT m n) → IsTrue m n lt)
+    (λ       ff ⇒ void (IsTrue 0 0 ff) ff)
+    (λ   n p tt ⇒ δ _ ⇒ 'true)
+    (λ m   p ff ⇒ void (IsTrue (succ m) 0 ff) ff)
+    (λ n m p tf ⇒ p tf)
+
+def revive : 0.(m n : ℕ) → 0.(LT m n) → LT m n =
+  λ m n lt ⇒ coe (𝑘 ⇒ true-ty m n lt @𝑘) @1 @0 'true
+
+
+def drop : 0.(A : ★) → 0.(m n : ℕ) → LT m n → A → A =
+  λ A m n lt x ⇒ true.drop A (coe (𝑖 ⇒ true-ty m n lt @𝑖) lt) x
+
+def0 succ-both : (m n : ℕ) → LT m n → LT (succ m) (succ n) =
+  λ m n p ⇒ p
+
+def0 succ-right : (m n : ℕ) → LT m n → LT m (succ n) =
+  λ m n lt ⇒
+    elimω (λ m n _ ⇒ LT m (succ n))
+      (λ _        ⇒ 'true)
+      (λ _ _ _ ih ⇒ ih)
+      m n lt
+
+def0 right-is-succ : (m n : ℕ) → LT m n → IsSucc n =
+  λ m n lt ⇒
+    elimω (λ _ n _ ⇒ IsSucc n) (λ _ ⇒ 'true) (λ _ _ _ _ ⇒ 'true) m n lt
+
+def right-has-succ : 0.(m : ℕ) → (n : ℕ) → 0.(LT m n) → HasSucc n =
+  λ m n lt ⇒
+    case n return n' ⇒ 0.(LT m n') → HasSucc n' of {
+      0      ⇒ λ lt ⇒ void (HasSucc 0) (right-is-succ m 0 lt);
+      succ n ⇒ λ _  ⇒ (n, [δ _ ⇒ succ n])
+    } lt
+
+def0 right-not-zero : (m : ℕ) → Not (LT m 0) =
+  λ m ⇒ case m return m' ⇒ Not (LT m' 0) of { 0 ⇒ λ v ⇒ v; succ _ ⇒ λ v ⇒ v }
+
+def0 plus-right : (m n₀ n₁ : ℕ) → LT m n₀ → LT m (plus n₀ n₁) =
+  λ m n₀ n₁ lt ⇒
+    elimω (λ m n _ ⇒ LT m (plus n n₁)) (λ _ ⇒ 'true) (λ _ _ _ ih ⇒ ih) m n₀ lt
+
+#[compile-scheme "(lambda% (m n) (if (< m n) dec.Yes dec.No))"]
+def lt? : ω.(m n : ℕ) → Dec (LT m n) =
+  elim-pairω (λ m n ⇒ Dec (LT m n))
+    (No (LT 0 0) (λ v ⇒ v))
+    (λ n p ⇒ Yes (LT 0 (succ n)) 'true)
+    (λ m p ⇒ No  (LT (succ m) 0) (λ v ⇒ v))
+    (λ m n p ⇒
+      dec.elim (LT m n) (λ _ ⇒ Dec (LT (succ m) (succ n)))
+        (λ yes ⇒ Yes (LT (succ m) (succ n)) yes)
+        (λ no  ⇒ No  (LT (succ m) (succ n)) no) p)
+
+
+def0 irrefl : (m n : ℕ) → LT m n → Not (m ≡ n : ℕ) =
+  λ m n lt ⇒
+    elimω (λ m n _ ⇒ Not (m ≡ n : ℕ))
+      (λ n eq ⇒ zero-not-succ n eq)
+      (λ m n _ ih eq ⇒ ih (succ-inj m n eq))
+      m n lt
+
+def0 asym : (m n : ℕ) → LT m n → Not (LT n m) =
+  λ m n lt ⇒
+    elimω (λ m n _ ⇒ Not (LT n m)) (λ _ ff ⇒ ff) (λ _ _ _ ih ff ⇒ ih ff) m n lt
+
+def0 trans : (n₀ n₁ n₂ : ℕ) → LT n₀ n₁ → LT n₁ n₂ → LT n₀ n₂ =
+  λ n₀ n₁ n₂ lt₀₁ lt₁₂ ⇒
+  elimω (λ n₀ n₁ lt₀₁ ⇒ (n₂ : ℕ) → (lt₁₂ : LT n₁ n₂) → LT n₀ n₂)
+    (λ n₁ n₂ ⇒
+      case n₂ return n₂' ⇒ LT (succ n₁) n₂' → LT 0 n₂' of {
+        0      ⇒ λ v ⇒ v;
+        succ _ ⇒ λ _ ⇒ 'true
+      })
+    (λ n₀ n₁ lt₀₁ ih n₂ ⇒
+      case n₂ return n₂' ⇒ LT (succ n₁) n₂' → LT (succ n₀) n₂' of {
+        0       ⇒ λ v    ⇒ v;
+        succ n₂ ⇒ λ lt₁₂ ⇒ ih n₂ lt₁₂
+      })
+    n₀ n₁ lt₀₁ n₂ lt₁₂
+
+}
+
+namespace nat {
+def0 LT  = lt.LT
+def  lt? = lt.lt?
+}
+
+
+namespace fin {
+
+def0 Bounded : ℕ → ℕ → ★ = λ n i ⇒ nat.LT i n
+
+def0 Fin : ℕ → ★ = λ n ⇒ Sub ℕ (Bounded n)
+
+def fin : 0.(n : ℕ) → (i : ℕ) → 0.(Bounded n i) → Fin n =
+  λ n ⇒ sub.sub ℕ (Bounded n)
+
+def val : 0.(n : ℕ) → Fin n → ℕ =
+  λ n ⇒ sub.val ℕ (Bounded n)
+
+def0 val-eq : (n : ℕ) → (i j : Fin n) → val n i ≡ val n j : ℕ → i ≡ j : Fin n =
+  λ n ⇒ sub.sub-eq ℕ (Bounded n) (λ i ⇒ nat.lt.irr i n)
+
+def0 proof : (n : ℕ) → (i : Fin n) → nat.LT (val n i) n =
+  λ n ⇒ sub.proof ℕ (Bounded n)
+
+
+def0 no-fin0 : Not (Fin 0) =
+  λ f0 ⇒ case f0 return False of { (i, lt) ⇒
+    nat.lt.right-not-zero i (get0 (nat.LT i 0) lt)
+  }
+
+
+def fin? : ω.(n i : ℕ) → Maybe (Fin n) =
+  λ n ⇒ sub.sub? ℕ (Bounded n) (λ i ⇒ nat.lt? i n)
+
+def F0 : 0.(n : ℕ) → Fin (succ n) =
+  λ n ⇒ fin (succ n) 0 'true
+def FS : 0.(n : ℕ) → Fin n → Fin (succ n) =
+  λ n i ⇒ fin (succ n) (succ (val n i)) (proof n i)
+
+def weak : 0.(m n : ℕ) → 0.(nat.LT m n) → Fin m → Fin n =
+  λ m n mn i' ⇒
+    let i = val m i'; 0.im = proof m i' in
+    fin n i (nat.lt.trans i m n im mn)
+
+
+def bound-has-succ : (n : ℕ) → 0.(Fin n) → nat.HasSucc n =
+  λ n i ⇒ nat.lt.right-has-succ (fst i) n (get0 (nat.LT (fst i) n) (snd i))
+
+def elim' :
+    0.(P : (n i : ℕ) → nat.LT i n → ★) →
+    1.(pz : 0.(n : ℕ) → P (succ n) 0 'true) →
+    ω.(ps : 0.(n i : ℕ) → 0.(lt : nat.LT i n) →
+            P n i lt → P (succ n) (succ i) lt) →
+    0.(n : ℕ) → (i : ℕ) → 0.(lt : nat.LT i n) → P n i lt =
+  λ P pz ps n i lt ⇒
+    case i return i' ⇒ 0.(n : ℕ) → 0.(lt : nat.LT i' n) → P n i' lt of {
+      0 ⇒ λ n lt ⇒
+        let0 npp = nat.lt.right-has-succ 0 n lt;
+             p   = nat.has-succ.val n npp;
+             np  = nat.has-succ.proof n npp in
+        coe (𝑘 ⇒ P (np @𝑘) 0 (coe (𝑙 ⇒ nat.LT 0 (np @𝑙)) @0 @𝑘 lt)) @1 @0
+            (pz p);
+      succ i, ih ⇒ λ n lt ⇒
+        let 0.npp = nat.lt.right-has-succ (succ i) n lt;
+            0.p   = nat.has-succ.val n npp;
+            0.np  = nat.has-succ.proof n npp;
+            0.lt' : nat.LT i p = coe (𝑘 ⇒ nat.LT (succ i) (np @𝑘)) lt;
+            0.lteq : Eq (𝑘 ⇒ nat.LT (succ i) (np @𝑘)) lt lt' =
+              δ 𝑘 ⇒ coe (𝑙 ⇒ nat.LT (succ i) (np @𝑙)) @0 @𝑘 lt;
+            1.almost : P (succ p) (succ i) lt' = ps p i lt' (ih p lt') in
+        coe (𝑘 ⇒ P (np @𝑘) (succ i) (lteq @𝑘)) @1 @0 almost;
+    } n lt
+
+def elim : 0.(P : (n : ℕ) → Fin n → ★) →
+           (pz : 0.(n : ℕ) → P (succ n) (F0 n)) →
+           (ps : 0.(n : ℕ) → 0.(i : Fin n) →
+                 P n i → P (succ n) (FS n i)) →
+           0.(n : ℕ) → (i : Fin n) → P n i =
+  λ P pz ps n ilt ⇒
+    case ilt return ilt' ⇒ P n ilt' of { (i, lt) ⇒
+      let0 lt = get0 (nat.LT i n) lt in
+      drop0 (nat.LT i n) (P n (i, [lt])) lt
+      (elim' (λ n i lt ⇒ P n (i, [lt])) pz (λ n i lt ⇒ ps n (i, [lt])) n i lt)
+    }
+
+{-
+def elim : 0.(P : (n : ℕ) → Fin n → ★) →
+           (pz : 0.(n : ℕ) → P (succ n) (F0 n)) →
+           (ps : 0.(n : ℕ) → 0.(i : Fin n) →
+                 P n i → P (succ n) (FS n i)) →
+           0.(n : ℕ) → (i : Fin n) → P n i =
+  λ P pz ps n ilt ⇒
+    let i = val n ilt; 0.lt : nat.LT i n = proof n ilt;
+        0.pp = nat.lt.right-has-succ i n lt;
+        0.p  = nat.has-succ.val n pp; 0.np = nat.has-succ.proof n pp;
+        0.RES : ℕ → ℕ → ★ =
+          λ i n ⇒ (lt : nat.LT i n) × P n (i, [lt]);
+        res : RES i (succ p) =
+          case i
+          return i' ⇒ 0.(p : ℕ) → 0.(nat.LT i' (succ p)) → RES i' (succ p)
+          of {
+            0 ⇒ λ p _ ⇒ ('true, pz p);
+            succ i, IH ⇒ λ p lt ⇒
+              let 0.qq = nat.lt.right-has-succ i p lt;
+                  0.q  = nat.has-succ.val p qq; 0.pq = nat.has-succ.proof p qq;
+                  0.lt : nat.LT i (succ q) = coe (𝑘 ⇒ nat.LT i (pq @𝑘)) lt;
+              in
+              case IH q lt return RES (succ i) (succ p) of { (lt', ih') ⇒
+                let lt : nat.LT (succ i) (succ p) =
+                      coe (𝑘 ⇒ nat.LT i (pq @𝑘)) @1 @0 lt';
+                    ih : P p (i, [lt]) =
+                      coe (𝑘 ⇒ P (pq @𝑘) (i, [coe (𝑙 ⇒ nat.LT i (pq @𝑙)) @1 @𝑘 lt']))
+                          @1 @0 ih';
+                    res : P (succ p) (succ i, [lt]) =
+                      ps p (i, [lt]) ih;
+                in
+                (lt, res)
+              }
+          } p (coe (𝑘 ⇒ nat.LT i (np @𝑘)) lt);
+    in
+    case coe (𝑘 ⇒ RES i (np @𝑘)) @1 @0 res
+    return P n ilt
+    of { (lt', res) ⇒
+      nat.lt.drop (P n ilt) i n lt' res
+    }
+-}
+
+}
+
+
+def0 Fin = fin.Fin
+def  F0  = fin.F0
+def  FS  = fin.FS
diff --git a/stdlib/int.quox b/stdlib/int.quox
new file mode 100644
index 0000000..3ca1478
--- /dev/null
+++ b/stdlib/int.quox
@@ -0,0 +1,149 @@
+load "nat.quox"
+
+namespace int {
+
+def0 Sign : ★ = {pos, neg-succ}
+def0 ℤ : ★ = Sign × ℕ
+
+def from-ℕ : ℕ → ℤ = λ n ⇒ ('pos, n)
+
+def neg-ℕ : ℕ → ℤ =
+  λ n ⇒ case n return ℤ of { 0 ⇒ ('pos, 0); succ n ⇒ ('neg-succ, n) }
+
+def zeroℤ : ℤ = ('pos, 0)
+
+
+def match : 0.(A : ★) → ω.(pos neg : ℕ → A) → ℤ → A =
+  λ A pos neg x ⇒
+    case x return A of { (s, x) ⇒
+      case s return A of { 'pos ⇒ pos x; 'neg-succ ⇒ neg x }
+    }
+
+def negate : ℤ → ℤ =
+  match ℤ neg-ℕ (λ x ⇒ from-ℕ (succ x))
+
+def minus-ℕ-ℕ : ℕ → ℕ → ℤ =
+  λ m n ⇒
+    letω f : ω.ℕ → ω.ℕ → ℤ = λ m n ⇒
+      bool.if ℤ (nat.ge m n) (from-ℕ (nat.minus m n))
+                             (neg-ℕ (nat.minus n m)) in
+    getω ℤ (app2ω ℕ ℕ ℤ f (nat.dup m) (nat.dup n))
+
+def plus-ℕ : ℤ → ℕ → ℤ =
+  match (ℕ → ℤ) (λ x n ⇒ from-ℕ (nat.plus x n))
+                (λ x n ⇒ minus-ℕ-ℕ n (succ x))
+
+def minus-ℕ : ℤ → ℕ → ℤ =
+  match (ℕ → ℤ) minus-ℕ-ℕ (λ x n ⇒ ('neg-succ, nat.plus x n))
+
+
+def plus : ℤ → ℤ → ℤ =
+  match (ℤ → ℤ) (λ x y ⇒ plus-ℕ y x) (λ x y ⇒ minus-ℕ y (succ x))
+
+def minus : ℤ → ℤ → ℤ = λ x y ⇒ plus x (negate y)
+
+
+def dup-sign : Sign → [ω. Sign] =
+  λ s ⇒ case s return [ω. Sign] of {
+    'pos      ⇒ ['pos];
+    'neg-succ ⇒ ['neg-succ]
+  }
+
+def0 dup-sign-ok : (s : Sign) → dup-sign s ≡ [s] : [ω. Sign] =
+  λ s ⇒ case s return s' ⇒ dup-sign s' ≡ [s'] : [ω. Sign] of {
+    'pos      ⇒ δ 𝑖 ⇒ ['pos];
+    'neg-succ ⇒ δ 𝑖 ⇒ ['neg-succ]
+  }
+
+def dup : ℤ → [ω.ℤ] =
+  λ x ⇒ case x return [ω.ℤ] of { (s, n) ⇒
+    app2ω Sign ℕ ℤ (λ s n ⇒ (s, n)) (dup-sign s) (nat.dup n)
+  }
+
+def0 dup-ok : (x : ℤ) → dup x ≡ [x] : [ω.ℤ] =
+  λ x ⇒
+  case x return x' ⇒ dup x' ≡ [x'] : [ω.ℤ] of { (s, n) ⇒ δ 𝑖 ⇒
+    app2ω Sign ℕ ℤ (λ s n ⇒ (s, n)) (dup-sign-ok s @𝑖) (nat.dup-ok n @𝑖)
+  }
+
+
+def times-ℕ : ℤ → ℕ → ℤ =
+  match (ℕ → ℤ)
+    (λ m  n ⇒ from-ℕ (nat.times m n))
+    (λ m' n ⇒ neg-ℕ (nat.times (succ m') n))
+
+def times : ℤ → ℤ → ℤ =
+  match (ℤ → ℤ) (λ p x ⇒ times-ℕ x p) (λ n x ⇒ negate (times-ℕ x (succ n)))
+
+
+def abs : ℤ → ℕ = match ℕ (λ p ⇒ p) (λ n ⇒ succ n)
+
+
+def pair-eq? : 0.(A B : ★) → ω.(DecEq A) → ω.(DecEq B) → DecEq (A × B) =
+  λ A B eqA? eqB? x y ⇒
+    let0 Ret : ★ = x ≡ y : (A × B) in
+    letω a0 = fst x; a1 = fst y;
+         b0 = snd x; b1 = snd y in
+    dec.elim (a0 ≡ a1 : A) (λ _ ⇒ Dec Ret)
+      (λ ya ⇒
+        dec.elim (b0 ≡ b1 : B) (λ _ ⇒ Dec Ret)
+          (λ yb ⇒ Yes Ret (δ 𝑖 ⇒ (ya @𝑖, yb @𝑖)))
+          (λ nb ⇒ No  Ret (λ eq ⇒ nb (δ 𝑖 ⇒ snd (eq @𝑖))))
+          (eqB? b0 b1))
+      (λ na ⇒ No Ret (λ eq ⇒ na (δ 𝑖 ⇒ fst (eq @𝑖))))
+      (eqA? a0 a1)
+
+
+def sign-eq? : DecEq Sign =
+  λ x y ⇒
+    let0 disc : Sign → ★ =
+      λ s ⇒ case s return ★ of { 'pos ⇒ True; 'neg-succ ⇒ False } in
+  case x return x' ⇒ Dec (x' ≡ y : Sign) of {
+    'pos ⇒
+      case y return y' ⇒ Dec ('pos ≡ y' : Sign) of {
+        'pos ⇒ dec.yes-refl Sign 'pos;
+        'neg-succ ⇒
+          No ('pos ≡ 'neg-succ : Sign)
+             (λ eq ⇒ coe (𝑖 ⇒ disc (eq @𝑖)) 'true)
+      };
+    'neg-succ ⇒
+      case y return y' ⇒ Dec ('neg-succ ≡ y' : Sign) of {
+        'neg-succ ⇒ dec.yes-refl Sign 'neg-succ;
+        'pos ⇒
+          No ('neg-succ ≡ 'pos : Sign)
+             (λ eq ⇒ coe (𝑖 ⇒ disc (eq @𝑖)) @1 @0 'true)
+      }
+  }
+
+#[compile-scheme "(lambda% (x y) (if (equal? x y) Yes No))"]
+def eq? : DecEq ℤ = pair-eq? Sign ℕ sign-eq? nat.eq?
+
+def eq : ω.ℤ → ω.ℤ → Bool =
+  λ x y ⇒ dec.bool (x ≡ y : ℤ) (eq? x y)
+
+}
+
+def0 ℤ = int.ℤ
+
+
+namespace scheme-int {
+  postulate0 Int : ★
+
+  #[compile-scheme "(lambda (x) x)"]
+  postulate from-ℕ : ℕ → Int
+
+  #[compile-scheme "(lambda% (x y) (+ x y))"]
+  postulate plus : Int → Int → Int
+
+  #[compile-scheme "(lambda% (x y) (- x y))"]
+  postulate minus : Int → Int → Int
+
+  #[compile-scheme "(lambda% (x y) (* x y))"]
+  postulate times : Int → Int → Int
+
+  #[compile-scheme "(lambda% (x y) (if (= x y) 'true 'false))"]
+  postulate eq : Int → Int → Bool
+
+  #[compile-scheme "abs"]
+  postulate abs : Int → ℕ
+}
diff --git a/stdlib/io.quox b/stdlib/io.quox
new file mode 100644
index 0000000..36ebe69
--- /dev/null
+++ b/stdlib/io.quox
@@ -0,0 +1,100 @@
+load "misc.quox"
+load "maybe.quox"
+load "list.quox"
+
+namespace io {
+
+def0 IORes : ★ → ★ = λ A ⇒ A × IOState
+
+def0 IO : ★ → ★ = λ A ⇒ IOState → IORes A
+
+def pure : 0.(A : ★) → A → IO A = λ A x s ⇒ (x, s)
+
+def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B =
+  λ A B m k s0 ⇒
+  case m s0 return IORes B of { (x, s1) ⇒ k x s1 }
+
+def bindω : 0.(A B : ★) → IO [ω.A] → (ω.A → IO B) → IO B =
+  λ A B m k s0 ⇒
+  case m s0 return IORes B of { (x, s1) ⇒
+    case x return IORes B of { [x] ⇒ k x s1 }
+  }
+
+def map : 0.(A B : ★) → (A → B) → IO A → IO B =
+  λ A B f m ⇒ bind A B m (λ x ⇒ pure B (f x))
+
+def mapω : 0.(A B : ★) → (ω.A → B) → IO [ω.A] → IO B =
+  λ A B f m ⇒ bindω A B m (λ x ⇒ pure B (f x))
+
+def seq : 0.(B : ★) → IO True → IO B → IO B =
+  λ B x y ⇒ bind True B x (λ u ⇒ case u return IO B of { 'true ⇒ y })
+
+def seq' : IO True → IO True → IO True = seq True
+
+def pass : IO True = pure True 'true
+
+#[compile-scheme "(lambda (str) (builtin-io (display str) 'true))"]
+postulate print : String → IO True
+
+#[compile-scheme "(lambda (str) (builtin-io (write str) (newline) 'true))"]
+postulate dump : 0.(A : ★) → A → IO True
+
+def newline = print "\n"
+
+def println : String → IO True =
+  λ str ⇒ seq' (print str) newline
+
+#[compile-scheme "(builtin-io (get-line (current-input-port)))"]
+postulate readln : IO String
+
+
+-- [todo] errors lmao
+
+{-
+postulate0 File : ★
+
+#[compile-scheme "(lambda (path) (builtin-io (open-input-file path)))"]
+postulate open-read : String → IO File
+
+#[compile-scheme "(lambda (file) (builtin-io (close-port file) 'true))"]
+postulate close : File → IO True
+
+#[compile-scheme
+ "(lambda% (file if-eof if-line)
+    (builtin-io
+      (let ([result (get-line file)])
+        (if (eof-object? result)
+            (cons if-eof file)
+            (cons (if-line result) file)))))"]
+postulate prim-read-line :
+  File →
+  ω.(if-eof  : Maybe [ω.String]) →
+  ω.(if-line : ω.String → Maybe [ω.String]) →
+  IO (Maybe [ω.String] × File)
+
+def read-line : File → IO (Maybe [ω.String] × File) =
+  λ f ⇒ prim-read-line f (Nothing [ω.String]) (λ x ⇒ Just [ω.String] [x])
+-}
+
+
+#[compile-scheme
+ "(lambda (path) (builtin-io (call-with-input-file path get-string-all)))"]
+postulate read-fileω : ω.(path : String) → IO [ω.String]
+
+def read-file : ω.(path : String) → IO String =
+  λ path ⇒
+    map [ω.String] String (getω String) (read-fileω path)
+
+
+#[compile-scheme
+  "(lambda (path) (builtin-io
+    (call-with-input-file path
+      (lambda (file)
+        (do [(line (get-line file) (get-line file))
+             (acc  '()             (cons line acc))]
+          [(eof-object? line) (reverse acc)])))))"]
+postulate read-file-lines : ω.(path : String) → IO (List String)
+
+}
+
+def0 IO = io.IO
diff --git a/stdlib/irrel.quox b/stdlib/irrel.quox
new file mode 100644
index 0000000..87537a4
--- /dev/null
+++ b/stdlib/irrel.quox
@@ -0,0 +1,43 @@
+load "misc.quox"
+
+def0 Irr1 : (A : ★) → (A → ★) → ★ =
+  λ A P ⇒ (x : A) → (p q : P x) → p ≡ q : P x
+
+def0 Sub : (A : ★) → (P : A → ★) → ★ =
+  λ A P ⇒ (x : A) × [0. P x]
+
+def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ =
+  λ A P s ⇒ Dup A (fst s)
+    -- (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]]
+
+def subdup-to-dup :
+    0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
+    0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
+  λ A P pirr s sd ⇒
+    case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
+    case ss0 return Dup (Sub A P) s of { [ss0] ⇒
+      case sω
+      return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s
+      of { [s!] ⇒ λ ss' ⇒
+        let ω.p  : [0.P (fst s)] = revive0 (P (fst s)) (snd s);
+            0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss' in
+        ([(s!, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @0 p)],
+         [δ 𝑗 ⇒ [(ss @𝑗, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @𝑗 p)]])
+      } ss0
+    }}
+
+def subdup : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
+             ((x : A) → Dup A x) →
+             (s : Sub A P) → SubDup A P s =
+  λ A P pirr dup s ⇒
+    case s return s' ⇒ SubDup A P s' of { (x, p) ⇒
+      drop0 (P x) (Dup A x) p (dup x)
+    }
+
+def dup : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
+          ((x : A) → Dup A x) →
+          (s : Sub A P) → Dup (Sub A P) s =
+  λ A P pirr dup s ⇒ subdup-to-dup A P pirr s (subdup A P pirr dup s)
+
+def forget : 0.(A : ★) → 0.(P : A → ★) → Sub A P → A =
+  λ A P s ⇒ case s return A of { (x, p) ⇒ drop0 (P x) A p x }
diff --git a/stdlib/list.quox b/stdlib/list.quox
new file mode 100644
index 0000000..2bab51e
--- /dev/null
+++ b/stdlib/list.quox
@@ -0,0 +1,590 @@
+load "misc.quox"
+load "nat.quox"
+load "maybe.quox"
+load "bool.quox"
+load "qty.quox"
+
+namespace vec {
+
+def0 Vec : ℕ → ★ → ★ =
+  λ n A ⇒
+  caseω n return ★ of {
+    zero           ⇒ {nil};
+    succ _, 0.Tail ⇒ A × Tail
+  }
+
+def drop-nil-dep : 0.(A : ★) → 0.(P : Vec 0 A → ★) →
+                   (xs : Vec 0 A) → P 'nil → P xs =
+  λ A P xs p ⇒ case xs return xs' ⇒ P xs' of { 'nil ⇒ p }
+
+def drop-nil : 0.(A B : ★) → Vec 0 A → B → B =
+  λ A B ⇒ drop-nil-dep A (λ _ ⇒ B)
+
+def match-dep :
+    0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
+    ω.(P 0 'nil) →
+    ω.((n : ℕ) → (x : A) → (xs : Vec n A) → P (succ n) (x, xs)) →
+    (n : ℕ) → (xs : Vec n A) → P n xs =
+  λ A P pn pc n ⇒
+    case n return n' ⇒ (xs : Vec n' A) → P n' xs of {
+      0 ⇒ λ nil ⇒ drop-nil-dep A (P 0) nil pn;
+      succ len ⇒ λ cons ⇒
+        case cons return cons' ⇒ P (succ len) cons' of {
+          (first, rest) ⇒ pc len first rest
+        }
+    }
+
+def match-depω :
+    0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
+    ω.(P 0 'nil) →
+    ω.(ω.(n : ℕ) → ω.(x : A) → ω.(xs : Vec n A) → P (succ n) (x, xs)) →
+    ω.(n : ℕ) → ω.(xs : Vec n A) → P n xs =
+  λ A P pn pc n ⇒
+    caseω n return n' ⇒ ω.(xs : Vec n' A) → P n' xs of {
+      0 ⇒ λ nil ⇒ drop-nil-dep A (P 0) nil pn;
+      succ len ⇒ λ cons ⇒
+        caseω cons return cons' ⇒ P (succ len) cons' of {
+          (first, rest) ⇒ pc len first rest
+        }
+    }
+def match-dep# = match-depω
+
+def elim : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
+           P 0 'nil →
+           ω.((x : A) → 0.(n : ℕ) → 0.(xs : Vec n A) →
+              P n xs → P (succ n) (x, xs)) →
+           (n : ℕ) → (xs : Vec n A) → P n xs =
+  λ A P pn pc n ⇒
+    case n return n' ⇒ (xs' : Vec n' A) → P n' xs' of {
+      zero ⇒ λ nil ⇒
+        case nil return nil' ⇒ P 0 nil' of { 'nil ⇒ pn };
+      succ n, IH ⇒ λ cons ⇒
+        case cons return cons' ⇒ P (succ n) cons' of {
+          (first, rest) ⇒ pc first n rest (IH rest)
+        }
+    }
+
+def elim2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★) →
+            P 0 'nil 'nil →
+            ω.((x : A) → (y : B) → 0.(n : ℕ) →
+               0.(xs : Vec n A) → 0.(ys : Vec n B) →
+               P n xs ys → P (succ n) (x, xs) (y, ys)) →
+            (n : ℕ) → (xs : Vec n A) → (ys : Vec n B) → P n xs ys =
+  λ A B P pn pc n ⇒
+    case n return n' ⇒ (xs : Vec n' A) → (ys : Vec n' B) → P n' xs ys of {
+      zero ⇒ λ nila nilb ⇒
+        drop-nil-dep A (λ n ⇒ P 0 n nilb) nila
+          (drop-nil-dep B (λ n ⇒ P 0 'nil n) nilb pn);
+      succ n, IH ⇒ λ consa consb ⇒
+        case consa return consa' ⇒ P (succ n) consa' consb of { (a, as) ⇒
+          case consb return consb' ⇒ P (succ n) (a, as) consb' of { (b, bs) ⇒
+            pc a b n as bs (IH as bs)
+          }
+        }
+    }
+
+def elim2-uneven :
+    0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →
+    -- both nil
+    ω.(P 0 0 'nil 'nil) →
+    -- first nil
+    ω.((y : B) → 0.(n : ℕ) → 0.(ys : Vec n B) →
+       P 0 n 'nil ys → P 0 (succ n) 'nil (y, ys)) →
+    -- second nil
+    ω.((x : A) → 0.(m : ℕ) → 0.(xs : Vec m A) →
+       P m 0 xs 'nil → P (succ m) 0 (x, xs) 'nil) →
+    -- both cons
+    ω.((x : A) → (y : B) → 0.(m n : ℕ) →
+       0.(xs : Vec m A) → 0.(ys : Vec n B) →
+       P m n xs ys → P (succ m) (succ n) (x, xs) (y, ys)) →
+    (m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) → P m n xs ys =
+  λ A B P pnn pnc pcn pcc ⇒
+    nat.elim-pair (λ m n ⇒ (xs : Vec m A) → (ys : Vec n B) → P m n xs ys)
+      (λ xnil ynil ⇒
+        let0 Ret = P 0 0 'nil 'nil in
+        drop-nil A Ret xnil (drop-nil B Ret ynil pnn))
+      (λ n IH xnil yys ⇒
+        case yys return yys' ⇒ P 0 (succ n) 'nil yys' of { (y, ys) ⇒
+          pnc y n ys (IH xnil ys)
+        })
+      (λ m IH xxs ynil ⇒
+        case xxs return xxs' ⇒ P (succ m) 0 xxs' 'nil of { (x, xs) ⇒
+          pcn x m xs (IH xs ynil)
+        })
+      (λ m n IH xxs yys ⇒
+        case xxs return xxs' ⇒ P (succ m) (succ n) xxs'    yys  of { (x, xs) ⇒
+        case yys return yys' ⇒ P (succ m) (succ n) (x, xs) yys' of { (y, ys) ⇒
+          pcc x y m n xs ys (IH xs ys)
+        }})
+
+-- haha gross
+def elimω : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
+            ω.(P 0 'nil) →
+            ω.(ω.(x : A) → ω.(n : ℕ) → ω.(xs : Vec n A) →
+               ω.(P n xs) → P (succ n) (x, xs)) →
+            ω.(n : ℕ) → ω.(xs : Vec n A) → P n xs =
+  λ A P pn pc n ⇒
+    caseω n return n' ⇒ ω.(xs' : Vec n' A) → P n' xs' of {
+      zero         ⇒ λ _ ⇒ pn;
+      succ n, ω.IH ⇒ λ xxs ⇒
+        letω x = fst xxs; xs = snd xxs in pc x n xs (IH xs)
+    }
+
+def elimω2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★) →
+             ω.(P 0 'nil 'nil) →
+             ω.(ω.(x : A) → ω.(y : B) → ω.(n : ℕ) →
+                ω.(xs : Vec n A) → ω.(ys : Vec n B) →
+                ω.(P n xs ys) → P (succ n) (x, xs) (y, ys)) →
+             ω.(n : ℕ) → ω.(xs : Vec n A) → ω.(ys : Vec n B) → P n xs ys =
+  λ A B P pn pc n ⇒
+    caseω n return n' ⇒ ω.(xs : Vec n' A) → ω.(ys : Vec n' B) → P n' xs ys of {
+      zero         ⇒ λ _ _ ⇒ pn;
+      succ n, ω.IH ⇒ λ xxs yys ⇒
+        letω x = fst xxs; xs = snd xxs; y = fst yys; ys = snd yys in
+        pc x y n xs ys (IH xs ys)
+    }
+
+postulate elimP :
+    ω.(π : NzQty) → ω.(ρₙ ρₗ : Qty) →
+    0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
+    FunNz π (P 0 'nil)
+    (Fun 'any
+        (FUN-NZ π A (λ x ⇒ FUN ρₙ ℕ (λ n ⇒ FUN ρₗ (Vec n A) (λ xs ⇒
+            FunNz π (P n xs) (P (succ n) (x, xs))))))
+    (FUN-NZ π ℕ (λ n ⇒ FUN-NZ π (Vec n A) (λ xs ⇒ P n xs))))
+{-
+  =
+  λ π ρₙ ρₗ A P ⇒ uhhhhhhhhhhhhhhhhhhh
+-}
+
+def elimω2-uneven :
+    0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →
+    -- both nil
+    ω.(P 0 0 'nil 'nil) →
+    -- first nil
+    ω.(ω.(y : B) → ω.(n : ℕ) → ω.(ys : Vec n B) →
+       ω.(P 0 n 'nil ys) → P 0 (succ n) 'nil (y, ys)) →
+    -- second nil
+    ω.(ω.(x : A) → ω.(m : ℕ) → ω.(xs : Vec m A) →
+       ω.(P m 0 xs 'nil) → P (succ m) 0 (x, xs) 'nil) →
+    -- both cons
+    ω.(ω.(x : A) → ω.(y : B) → ω.(m n : ℕ) →
+       ω.(xs : Vec m A) → ω.(ys : Vec n B) →
+       ω.(P m n xs ys) → P (succ m) (succ n) (x, xs) (y, ys)) →
+    ω.(m n : ℕ) → ω.(xs : Vec m A) → ω.(ys : Vec n B) → P m n xs ys =
+  λ A B P pnn pnc pcn pcc ⇒
+    nat.elim-pairω (λ m n ⇒ ω.(xs : Vec m A) → ω.(ys : Vec n B) → P m n xs ys)
+      (λ _ _ ⇒ pnn)
+      (λ n IH xnil yys ⇒
+        letω y = fst yys; ys = snd yys in pnc y n ys (IH xnil ys))
+      (λ m IH xxs ynil ⇒
+        letω x = fst xxs; xs = snd xxs in pcn x m xs (IH xs ynil))
+      (λ m n IH xxs yys ⇒
+        letω x = fst xxs; xs = snd xxs; y = fst yys; ys = snd yys in
+        pcc x y m n xs ys (IH xs ys))
+
+def zip-with : 0.(A B C : ★) → ω.(A → B → C) →
+               (n : ℕ) → Vec n A → Vec n B → Vec n C =
+  λ A B C f ⇒
+    elim2 A B (λ n _ _ ⇒ Vec n C) 'nil (λ a b _ _ _ abs ⇒ (f a b, abs))
+
+def zip-withω : 0.(A B C : ★) → ω.(ω.A → ω.B → C) →
+                ω.(n : ℕ) → ω.(Vec n A) → ω.(Vec n B) → Vec n C =
+  λ A B C f ⇒
+    elimω2 A B (λ n _ _ ⇒ Vec n C) 'nil (λ a b _ _ _ abs ⇒ (f a b, abs))
+
+
+namespace zip-with {
+  def0 Failure : (A B : ★) → (m n : ℕ) → Vec m A → Vec n B → ★ =
+    λ A B m n xs ys ⇒
+    Sing (Vec m A) xs × Sing (Vec n B) ys × [0. Not (m ≡ n : ℕ)]
+
+  def0 Success : (C : ★) → (m n : ℕ) → ★ =
+    λ C m n ⇒ Vec n C × [0. m ≡ n : ℕ]
+
+  def0 Result : (A B C : ★) → (m n : ℕ) → Vec m A → Vec n B → ★ =
+    λ A B C m n xs ys ⇒
+    Either (Failure A B m n xs ys) (Success C m n)
+
+  def zip-with-hetω : 0.(A B C : ★) → ω.(A → B → C) →
+                      ω.(m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) →
+                      Result A B C m n xs ys =
+    λ A B C f m n xs ys ⇒
+      let0 TNo  : Vec m A → Vec n B → ★ = Failure A B m n;
+           TYes : ★ = Success C m n;
+           TRes : Vec m A → Vec n B → ★ = λ xs ys ⇒ Either (TNo xs ys) TYes in
+      dec.elim (m ≡ n : ℕ)
+        (λ _ ⇒ (xs : Vec m A) → (ys : Vec n B) → TRes xs ys)
+        (λ eq xs ys ⇒
+          let zs : Vec n C =
+            zip-with A B C f n (coe (𝑖 ⇒ Vec (eq @𝑖) A) xs) ys in
+          Right (TNo xs ys) TYes (zs, [eq]))
+        (λ neq xs ys ⇒ Left (TNo xs ys) TYes
+          (sing (Vec m A) xs, sing (Vec n B) ys, [neq]))
+        (nat.eq? m n) xs ys
+
+  def zip-with-het : 0.(A B C : ★) → ω.(A → B → C) →
+                     (m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) →
+                     Result A B C m n xs ys =
+    λ A B C f m n ⇒
+      let0 Ret : ℕ → ℕ → ★ =
+             λ m n ⇒ (xs : Vec m A) → (ys : Vec n B) → Result A B C m n xs ys in
+      dup.elim ℕ m (λ m' ⇒ Ret m' n)
+        (λ m ⇒ dup.elim ℕ n (λ n' ⇒ Ret m n')
+          (λ n ⇒ zip-with-hetω A B C f m n) (nat.dup! n))
+        (nat.dup! m)
+}
+def0 ZipWith = zip-with.Result
+def zip-with-het = zip-with.zip-with-het
+def zip-with-hetω = zip-with.zip-with-hetω
+
+#[compile-scheme "(lambda% (n xs) xs)"]
+def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A =
+  λ A n ⇒
+    case n return n' ⇒ Vec n' A → Vec¹ n' A of {
+      zero ⇒ λ xs ⇒
+        case xs return Vec¹ 0 A of { 'nil ⇒ 'nil };
+      succ n', f' ⇒ λ xs ⇒
+        case xs return Vec¹ (succ n') A of {
+          (first, rest) ⇒ (first, f' rest)
+        }
+    }
+
+def append : 0.(A : ★) → (m : ℕ) → 0.(n : ℕ) →
+             Vec m A → Vec n A → Vec (nat.plus m n) A =
+  λ A m n xs ys ⇒
+    elim A (λ m _ ⇒ Vec (nat.plus m n) A) ys (λ x _ _ xsys ⇒ (x, xsys)) m xs
+
+}
+
+def0 Vec = vec.Vec
+
+
+namespace list {
+
+def0 List : ★ → ★ =
+  λ A ⇒ (len : ℕ) × Vec len A
+
+def Nil : 0.(A : ★) → List A =
+  λ A ⇒ (0, 'nil)
+
+def Cons : 0.(A : ★) → A → List A → List A =
+  λ A x xs ⇒ case xs return List A of { (len, elems) ⇒ (succ len, x, elems) }
+
+def single : 0.(A : ★) → A → List A =
+  λ A x ⇒ Cons A x (Nil A)
+
+def elim : 0.(A : ★) → 0.(P : List A → ★) →
+           P (Nil A) →
+           ω.((x : A) → 0.(xs : List A) → P xs → P (Cons A x xs)) →
+           (xs : List A) → P xs =
+  λ A P pn pc xs ⇒
+    case xs return xs' ⇒ P xs' of { (len, elems) ⇒
+      vec.elim A (λ n xs ⇒ P (n, xs))
+        pn (λ x n xs IH ⇒ pc x (n, xs) IH)
+        len elems
+    }
+
+def elimω : 0.(A : ★) → 0.(P : List A → ★) →
+            ω.(P (Nil A)) →
+            ω.(ω.(x : A) → ω.(xs : List A) → ω.(P xs) → P (Cons A x xs)) →
+            ω.(xs : List A) → P xs =
+  λ A P pn pc xs ⇒
+    caseω xs return xs' ⇒ P xs' of { (len, elems) ⇒
+      vec.elimω A (λ n xs ⇒ P (n, xs))
+        pn (λ x n xs IH ⇒ pc x (n, xs) IH)
+        len elems
+    }
+
+def elim2 : 0.(A B : ★) → 0.(P : List A → List B → ★) →
+            ω.(P (Nil A) (Nil B)) →
+            ω.((y : B) → 0.(ys : List B) →
+               P (Nil A) ys → P (Nil A) (Cons B y ys)) →
+            ω.((x : A) → 0.(xs : List A) →
+               P xs (Nil B) → P (Cons A x xs) (Nil B)) →
+            ω.((x : A) → 0.(xs : List A) → (y : B) → 0.(ys : List B) →
+               P xs ys → P (Cons A x xs) (Cons B y ys)) →
+            (xs : List A) → (ys : List B) → P xs ys =
+  λ A B P pnn pnc pcn pcc xs ys ⇒
+    case xs return xs' ⇒ P xs'     ys  of { (m, xs) ⇒
+    case ys return ys' ⇒ P (m, xs) ys' of { (n, ys) ⇒
+      vec.elim2-uneven A B (λ m n xs ys ⇒ P (m, xs) (n, ys))
+        pnn
+        (λ y n ys IH ⇒ pnc y (n, ys) IH)
+        (λ x m xs IH ⇒ pcn x (m, xs) IH)
+        (λ x y m n xs ys IH ⇒ pcc x (m, xs) y (n, ys) IH)
+        m n xs ys
+    }}
+
+def elimω2 : 0.(A B : ★) → 0.(P : List A → List B → ★) →
+             ω.(P (Nil A) (Nil B)) →
+             ω.(ω.(y : B) → ω.(ys : List B) →
+                ω.(P (Nil A) ys) → P (Nil A) (Cons B y ys)) →
+             ω.(ω.(x : A) → ω.(xs : List A) →
+                ω.(P xs (Nil B)) → P (Cons A x xs) (Nil B)) →
+             ω.(ω.(x : A) → ω.(xs : List A) → ω.(y : B) → ω.(ys : List B) →
+                ω.(P xs ys) → P (Cons A x xs) (Cons B y ys)) →
+             ω.(xs : List A) → ω.(ys : List B) → P xs ys =
+  λ A B P pnn pnc pcn pcc xs ys ⇒
+    caseω xs return xs' ⇒ P xs'     ys  of { (m, xs) ⇒
+    caseω ys return ys' ⇒ P (m, xs) ys' of { (n, ys) ⇒
+      vec.elimω2-uneven A B (λ m n xs ys ⇒ P (m, xs) (n, ys))
+        pnn
+        (λ y n ys IH ⇒ pnc y (n, ys) IH)
+        (λ x m xs IH ⇒ pcn x (m, xs) IH)
+        (λ x y m n xs ys IH ⇒ pcc x (m, xs) y (n, ys) IH)
+        m n xs ys
+    }}
+
+def as-vec : 0.(A : ★) → 0.(P : List A → ★) → (xs : List A) →
+             (ω.(n : ℕ) → (xs : Vec n A) → P (n, xs)) → P xs =
+  λ A P xs f ⇒
+    case xs return xs' ⇒ P xs' of { (n, xs) ⇒
+      dup.elim ℕ n (λ n' ⇒ (xs : Vec n' A) → P (n', xs)) f (nat.dup! n) xs
+    }
+
+def match-dep :
+    0.(A : ★) → 0.(P : List A → ★) →
+    ω.(P (Nil A)) → ω.((x : A) → (xs : List A) → P (Cons A x xs)) →
+    (xs : List A) → P xs =
+  λ A P pn pc xs ⇒
+    case xs return xs' ⇒ P xs' of {
+      (len, elems) ⇒
+        vec.match-dep A (λ n xs ⇒ P (n, xs)) pn (λ n x xs ⇒ pc x (n, xs))
+          len elems
+    }
+
+def match-depω :
+    0.(A : ★) → 0.(P : List A → ★) →
+    ω.(P (Nil A)) →
+    ω.(ω.(x : A) → ω.(xs : List A) → P (Cons A x xs)) →
+    ω.(xs : List A) → P xs =
+  λ A P pn pc xs ⇒
+    vec.match-depω A (λ n xs ⇒ P (n, xs)) pn (λ n x xs ⇒ pc x (n, xs))
+                   (fst xs) (snd xs)
+def match-dep# = match-depω
+
+def match : 0.(A B : ★) → ω.B → ω.(A → List A → B) → List A → B =
+  λ A B ⇒ match-dep A (λ _ ⇒ B)
+
+def matchω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.(List A) → B) → ω.(List A) → B =
+  λ A B ⇒ match-depω A (λ _ ⇒ B)
+def match# = matchω
+
+
+def up : 0.(A : ★) → List A → List¹ A =
+  λ A xs ⇒
+  case xs return List¹ A of { (len, elems) ⇒
+    dup.elim'¹ ℕ len (λ _ ⇒ List¹ A)
+      (λ len eq ⇒ (len, vec.up A len (coe (𝑖 ⇒ Vec (eq @𝑖) A) @1 @0 elems)))
+      (nat.dup! len)
+  }
+
+def foldr : 0.(A B : ★) → B → ω.(A → B → B) → List A → B =
+  λ A B z f xs ⇒ elim A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs
+
+def foldl : 0.(A B : ★) → B → ω.(B → A → B) → List A → B =
+  λ A B z f xs ⇒
+    foldr A (B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z
+
+def map : 0.(A B : ★) → ω.(A → B) → List A → List B =
+  λ A B f ⇒ foldr A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys)
+
+
+-- ugh
+def foldrω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.B → B) → ω.(List A) → B =
+  λ A B z f xs ⇒ elimω A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs
+
+def foldlω : 0.(A B : ★) → ω.B → ω.(ω.B → ω.A → B) → ω.(List A) → B =
+  λ A B z f xs ⇒
+    foldrω A (ω.B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z
+
+def mapω : 0.(A B : ★) → ω.(ω.A → B) → ω.(List A) → List B =
+  λ A B f ⇒ foldrω A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys)
+
+
+def0 All : (A : ★) → (P : A → ★) → List A → ★ =
+  λ A P xs ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps) (up A xs)
+
+def append : 0.(A : ★) → List A → List A → List A =
+  λ A xs ys ⇒ foldr A (List A) ys (Cons A) xs
+
+def reverse : 0.(A : ★) → List A → List A =
+  λ A ⇒ foldl A (List A) (Nil A) (λ xs x ⇒ Cons A x xs)
+
+
+def find : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → Maybe A =
+  λ A p ⇒
+    foldlω A (Maybe A) (Nothing A) (λ m x ⇒ maybe.or A m (maybe.check A p x))
+
+def cons-first : 0.(A : ★) → ω.A → List (List A) → List (List A) =
+  λ A x ⇒
+    match (List A) (List (List A))
+      (single (List A) (single A x))
+      (λ xs xss ⇒ Cons (List A) (Cons A x xs) xss)
+
+def split : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List (List A) =
+  λ A p ⇒
+    foldrω A (List (List A))
+      (Nil (List A))
+      (λ x xss ⇒ bool.if (List (List A)) (p x)
+          (Cons (List A) (Nil A) xss)
+          (cons-first A x xss))
+
+def break : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List A × List A =
+  λ A p xs ⇒
+  let0 Lst = List A; Lst2 = (Lst × Lst) ∷ ★; State = Either Lst Lst2 in
+  letω LeftS = Left Lst Lst2; RightS = Right Lst Lst2 in
+  letω res =
+    foldlω A State
+      (LeftS (Nil A))
+      (λ acc x ⇒
+        either.foldω Lst Lst2 State
+          (λ xs ⇒ bool.if State (p x)
+            (RightS (xs, list.single A x))
+            (LeftS  (Cons A x xs)))
+          (λ xsys ⇒
+            RightS (fst xsys, Cons A x (snd xsys))) acc)
+      xs ∷ State in
+  letω res =
+    either.fold Lst Lst2 Lst2 (λ xs ⇒ (Nil A, xs)) (λ xsys ⇒ xsys) res in
+  (reverse A (fst res), reverse A (snd res))
+
+def uncons : 0.(A : ★) → List A → Maybe (A × List A) =
+  λ A ⇒
+    match A (Maybe (A × List A))
+      (Nothing (A × List A))
+      (λ x xs ⇒ Just (A × List A) (x, xs))
+
+def head : 0.(A : ★) → ω.(List A) → Maybe A =
+  λ A ⇒ matchω A (Maybe A) (Nothing A) (λ x _ ⇒ Just A x)
+
+def tail : 0.(A : ★) → ω.(List A) → Maybe (List A) =
+  λ A ⇒ matchω A (Maybe (List A)) (Nothing (List A)) (λ _ xs ⇒ Just (List A) xs)
+
+def tail-or-nil : 0.(A : ★) → ω.(List A) → List A =
+  λ A ⇒ matchω A (List A) (Nil A) (λ _ xs ⇒ xs)
+
+-- slip (xs, [])      = (xs, [])
+-- slip (xs, y :: ys) = (y :: xs, ys)
+def slip : 0.(A : ★) → List A × List A → List A × List A =
+  λ A xsys ⇒
+    case xsys return List A × List A of { (xs, ys) ⇒
+      match A (List A → List A × List A)
+        (λ      xs ⇒ (xs, Nil A))
+        (λ y ys xs ⇒ (Cons A y xs, ys))
+        ys xs
+    }
+
+def split-at' : 0.(A : ★) → ℕ → List A → List A × List A =
+  λ A n xs ⇒
+    (case n return List A × List A → List A × List A of {
+      0         ⇒ λ xsys ⇒ xsys;
+      succ _, f ⇒ λ xsys ⇒ f (slip A xsys)
+    }) (Nil A, xs)
+
+def split-at : 0.(A : ★) → ℕ → List A → List A × List A =
+  λ A n xs ⇒
+    case split-at' A n xs return List A × List A of {
+      (xs', ys) ⇒ (reverse A xs', ys)
+    }
+
+def filter : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List A =
+  λ A p ⇒
+    foldrω A (List A)
+      (Nil A)
+      (λ x xs ⇒ bool.if (List A) (p x) (Cons A x xs) xs)
+
+def length : 0.(A : ★) → ω.(List A) → ℕ =
+  λ A xs ⇒ fst xs
+
+
+namespace zip-with {
+  def0 VFailure = vec.zip-with.Failure
+  def0 VSuccess = vec.zip-with.Success
+
+  def0 Failure : (A B : ★) → List A → List B → ★ =
+    λ A B xs ys ⇒ VFailure A B (fst xs) (fst ys) (snd xs) (snd ys)
+
+  def0 Result : (A B C : ★) → List A → List B → ★ =
+    λ A B C xs ys ⇒ Either (Failure A B xs ys) (List C)
+
+  def zip-with : 0.(A B C : ★) → ω.(A → B → C) →
+                 (xs : List A) → (ys : List B) →
+                 Result A B C xs ys =
+    λ A B C f xs ys ⇒
+    let0 Ret = Result A B C in
+    as-vec A (λ xs' ⇒ Ret xs'     ys)  xs (λ m xs ⇒
+    as-vec B (λ ys' ⇒ Ret (m, xs) ys') ys (λ n ys ⇒
+    let0 Err = Failure A B (m, xs) (n, ys) in
+    either.fold Err (VSuccess C m n) (Ret (m, xs) (n, ys))
+      (λ no ⇒ Left Err (List C) no)
+      (λ yes ⇒ case yes return Ret (m, xs) (n, ys) of { (vec, prf) ⇒
+        Right Err (List C) (drop0 (m ≡ n : ℕ) (List C) prf (n, vec))
+      })
+      (vec.zip-with-hetω A B C f m n xs ys)))
+}
+def0 ZipWith = zip-with.Result
+def zip-with = zip-with.zip-with
+
+def zip-withω : 0.(A B C : ★) → ω.(ω.A → ω.B → C) →
+                ω.(xs : List A) → ω.(ys : List B) →
+                Either [0. Not (fst xs ≡ fst ys : ℕ)] (List C) =
+  λ A B C f xs ys ⇒
+    letω m = fst xs; xs = snd xs;
+         n = fst ys; ys = snd ys in
+    let0 Err : ★ = [0. Not (m ≡ n : ℕ)] in
+    dec.elim (m ≡ n : ℕ) (λ _ ⇒ Either Err (List C))
+      (λ mn ⇒
+        letω xs = coe (𝑖 ⇒ Vec (mn @𝑖) A) xs in
+        Right Err (List C) (n, vec.zip-withω A B C f n xs ys))
+      (λ nmn ⇒ Left Err (List C) [nmn])
+      (nat.eq? m n)
+def zip-with# = zip-withω
+
+
+def zip-with-uneven :
+    0.(A B C : ★) → ω.(ω.A → ω.B → C) → ω.(List A) → ω.(List B) → List C =
+  λ A B C f xs ys ⇒
+    caseω nat.min (fst xs) (fst ys)
+    return ω.(List A) → ω.(List B) → List C of {
+      0             ⇒ λ _ _ ⇒ Nil C;
+      succ _, ω.fih ⇒ λ xs ys ⇒
+        maybe.foldω (A × List A) (List C) (Nil C)
+          (λ xxs ⇒ maybe.foldω (B × List B) (List C) (Nil C)
+            (λ yys ⇒ Cons C (f (fst xxs) (fst yys)) (fih (snd xxs) (snd yys)))
+            (list.uncons B ys))
+          (list.uncons A xs)
+    } xs ys
+
+
+def sum     : List ℕ → ℕ = foldl ℕ ℕ 0 nat.plus
+def product : List ℕ → ℕ = foldl ℕ ℕ 1 nat.times
+
+
+namespace mergesort {
+  def deal : 0.(A : ★) → List A → List A × List A =
+    λ A ⇒
+    let0 One = List A; Pair : ★ = One × One in
+    foldl A Pair (Nil A, Nil A)
+      (pair.uncurry' One One (A → Pair) (λ ys zs x ⇒ (Cons A x zs, ys)))
+
+}
+
+
+postulate0 SchemeList : ★ → ★
+
+#[compile-scheme
+  "(lambda (list) (cons (length list) (fold-right cons 'nil list)))"]
+postulate from-scheme : 0.(A : ★) → SchemeList A → List A
+
+#[compile-scheme
+ "(lambda (lst)
+    (do [(lst (cdr lst) (cdr lst))
+         (acc '()       (cons (car lst) acc))]
+      [(equal? lst 'nil) (reverse acc)]))"]
+postulate to-scheme : 0.(A : ★) → List A → SchemeList A
+
+}
+
+def0 List = list.List
diff --git a/stdlib/maybe.quox b/stdlib/maybe.quox
new file mode 100644
index 0000000..83e96c4
--- /dev/null
+++ b/stdlib/maybe.quox
@@ -0,0 +1,146 @@
+load "misc.quox"
+load "pair.quox"
+load "either.quox"
+
+namespace maybe {
+
+def0 Tag : ★ = {nothing, just}
+
+def0 Payload : Tag → ★ → ★ =
+  λ tag A ⇒ case tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
+
+def0 Maybe : ★ → ★ =
+  λ A ⇒ (t : Tag) × Payload t A
+
+def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
+  λ _ x ⇒ caseω x return Tag of { (tag, _) ⇒ tag }
+
+def Nothing : 0.(A : ★) → Maybe A =
+  λ _ ⇒ ('nothing, 'true)
+
+def Just : 0.(A : ★) → A → Maybe A =
+  λ _ x ⇒ ('just, x)
+
+def0 IsJustTag : Tag → ★ =
+  λ t ⇒ case t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
+
+def0 IsJust : (A : ★) → Maybe A → ★ =
+  λ A x ⇒ IsJustTag (tag A x)
+
+def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
+  λ A x ⇒
+  caseω tag A x return t ⇒ Dec (IsJustTag t) of {
+    'just    ⇒ Yes True  'true;
+    'nothing ⇒ No  False (λ x ⇒ x)
+  }
+
+def0 nothing-unique :
+    (A : ★) → (x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
+  λ A x ⇒
+  case x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
+    'true ⇒ δ _ ⇒ ('nothing, 'true)
+  }
+
+def elim' :
+    0.(A : ★) →
+    0.(P : (t : Tag) → Payload t A → ★) →
+    ω.(P 'nothing 'true) →
+    ω.((x : A) → P 'just x) →
+    (t : Tag) → (x : Payload t A) → P t x =
+  λ A P nothing just tag ⇒
+  case tag return t ⇒ (x : Payload t A) → P t x of {
+    'nothing ⇒ λ x ⇒ case x return x' ⇒ P 'nothing x' of { 'true ⇒ nothing };
+    'just    ⇒ just
+  }
+
+def elim :
+    0.(A : ★) →
+    0.(P : Maybe A → ★) →
+    ω.(P (Nothing A)) →
+    ω.((x : A) → P (Just A x)) →
+    (x : Maybe A) → P x =
+  λ A P n j x ⇒
+    case x return x' ⇒ P x' of {
+      (tag, payload) ⇒ elim' A (λ x t ⇒ P (x, t)) n j tag payload
+    }
+
+def elimω' :
+    0.(A : ★) →
+    0.(P : (t : Tag) → Payload t A → ★) →
+    ω.(P 'nothing 'true) →
+    ω.(ω.(x : A) → P 'just x) →
+    ω.(t : Tag) → ω.(x : Payload t A) → P t x =
+  λ A P nothing just tag ⇒
+  case tag return t ⇒ ω.(x : Payload t A) → P t x of {
+    'nothing ⇒ λ x ⇒ case x return x' ⇒ P 'nothing x' of { 'true ⇒ nothing };
+    'just    ⇒ just
+  }
+
+def elimω :
+    0.(A : ★) →
+    0.(P : Maybe A → ★) →
+    ω.(P (Nothing A)) →
+    ω.(ω.(x : A) → P (Just A x)) →
+    ω.(x : Maybe A) → P x =
+  λ A P n j x ⇒
+    caseω x return x' ⇒ P x' of {
+      (tag, payload) ⇒ elimω' A (λ x t ⇒ P (x, t)) n j tag payload
+    }
+
+{-
+-- direct elim implementation
+def elim :
+    0.(A : ★) →
+    0.(P : Maybe A → ★) →
+    ω.(P (Nothing A)) →
+    ω.((x : A) → P (Just A x)) →
+    (x : Maybe A) → P x =
+  λ A P n j x ⇒
+  case x return x' ⇒ P x' of { (tag, payload) ⇒
+    (case tag
+     return t ⇒
+       0.(eq : tag ≡ t : Tag) → P (t, coe (𝑖 ⇒ Payload (eq @𝑖) A) payload)
+     of {
+       'nothing ⇒
+          λ eq ⇒
+          case coe (𝑖 ⇒ Payload (eq @𝑖) A) payload
+          return p ⇒ P ('nothing, p)
+          of { 'true ⇒ n };
+       'just ⇒ λ eq ⇒ j (coe (𝑖 ⇒ Payload (eq @𝑖) A) payload)
+     }) (δ 𝑖 ⇒ tag)
+  }
+-}
+
+def fold : 0.(A B : ★) → ω.B → ω.(A → B) → Maybe A → B =
+  λ A B ⇒ elim A (λ _ ⇒ B)
+
+def foldω : 0.(A B : ★) → ω.B → ω.(ω.A → B) → ω.(Maybe A) → B =
+  λ A B ⇒ elimω A (λ _ ⇒ B)
+
+def join : 0.(A : ★) → (Maybe (Maybe A)) → Maybe A =
+  λ A ⇒ fold (Maybe A) (Maybe A) (Nothing A) (λ x ⇒ x)
+
+def pair : 0.(A B : ★) → ω.(Maybe A) → ω.(Maybe B) → Maybe (A × B) =
+  λ A B x y ⇒
+    foldω A (Maybe (A × B)) (Nothing (A × B))
+      (λ x' ⇒ fold B (Maybe (A × B)) (Nothing (A × B))
+        (λ y' ⇒ Just (A × B) (x', y')) y) x
+
+def map : 0.(A B : ★) → ω.(A → B) → Maybe A → Maybe B =
+  λ A B f ⇒ fold A (Maybe B) (Nothing B) (λ x ⇒ Just B (f x))
+
+def mapω : 0.(A B : ★) → ω.(ω.A → B) → ω.(Maybe A) → Maybe B =
+  λ A B f ⇒ foldω A (Maybe B) (Nothing B) (λ x ⇒ Just B (f x))
+
+
+def check : 0.(A : ★) → (ω.A → Bool) → ω.A → Maybe A =
+  λ A p x ⇒ bool.if (Maybe A) (p x) (Just A x) (Nothing A)
+
+def or : 0.(A : ★) → Maybe A → ω.(Maybe A) → Maybe A =
+  λ A l r ⇒ fold A (Maybe A) r (Just A) l
+
+}
+
+def0 Maybe   = maybe.Maybe
+def  Just    = maybe.Just
+def  Nothing = maybe.Nothing
diff --git a/stdlib/misc.quox b/stdlib/misc.quox
new file mode 100644
index 0000000..945c9af
--- /dev/null
+++ b/stdlib/misc.quox
@@ -0,0 +1,261 @@
+namespace true {
+  def0 True : ★ = {true}
+
+  def drop : 0.(A : ★) → True → A → A =
+    λ A t x ⇒ case t return A of { 'true ⇒ x }
+
+  def0 eta : (s : True) → s ≡ 'true : True =
+    λ s ⇒ case s return s' ⇒ s' ≡ 'true : True of { 'true ⇒ δ 𝑖 ⇒ 'true }
+
+  def0 irr : (s t : True) → s ≡ t : True =
+    λ s t ⇒
+      coe (𝑖 ⇒ eta s @𝑖 ≡ t : True) @1 @0
+        (coe (𝑖 ⇒ 'true ≡ eta t @𝑖 : True) @1 @0 (δ _ ⇒ 'true))
+
+  def revive : 0.True → True = λ _ ⇒ 'true
+}
+def0 True = true.True
+
+namespace false {
+  def0 False : ★ = {}
+
+  def void : 0.(A : ★) → 0.False → A =
+    λ A v ⇒ case0 v return A of { }
+
+  def0 irr : (u v : False) → u ≡ v : False =
+    λ u v ⇒ void (u ≡ v : False) u
+
+  def revive : 0.False → False = void False
+}
+def0 False = false.False
+def void = false.void
+
+
+def0 Not : ★ → ★ = λ A ⇒ ω.A → False
+
+def0 Iff : ★ → ★ → ★ = λ A B ⇒ (A → B) × (B → A)
+
+def0 All : (A : ★) → (A → ★) → ★ =
+  λ A P ⇒ (x : A) → P x
+
+def cong :
+    0.(A : ★) → 0.(P : A → ★) → 1.(p : All A P) →
+    0.(x y : A) → 1.(xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
+  λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
+
+def cong' :
+    0.(A B : ★) → 1.(f : A → B) →
+    0.(x y : A) → 1.(xy : x ≡ y : A) → f x ≡ f y : B =
+  λ A B ⇒ cong A (λ _ ⇒ B)
+
+def coherence :
+    0.(A B : ★) → 0.(AB : A ≡ B : ★) → 1.(x : A) →
+    Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) =
+  λ A B AB x ⇒
+    δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x
+
+
+def0 EqF : (A : ★) → (P : A → ★) → (p : All A P) → (q : All A P) → A → ★ =
+  λ A P p q x ⇒ p x ≡ q x : P x
+
+def funext :
+    0.(A : ★) → 0.(P : A → ★) → 0.(p q : All A P) →
+    1.(All A (EqF A P p q)) → p ≡ q : All A P =
+  λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖
+
+def refl : 0.(A : ★) → 1.(x : A) → x ≡ x : A = λ A x ⇒ δ _ ⇒ x
+
+def sym : 0.(A : ★) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
+  λ A x y eq ⇒ coe (𝑗 ⇒ eq @𝑗 ≡ x : A) (δ _ ⇒ eq @0)
+    -- btw this uses eq @0 instead of just x because of the quantities
+
+def sym-c : 0.(A : ★) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
+  λ A x y eq ⇒ δ 𝑖 ⇒
+    comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }
+
+{-
+def sym-het : 0.(A B : ★) → 0.(AB : A ≡ B : ★) →
+              0.(x : A) → 0.(y : B) →
+              1.(Eq (𝑖 ⇒ AB @𝑖) x y) →
+              Eq (𝑖 ⇒ sym¹ ★ A B AB @𝑖) y x =
+  λ A B AB x y xy ⇒
+    let0 BA  = sym¹ ★ A B AB;
+         y'  : A = coe (𝑖 ⇒ BA @𝑖) y;
+         yy' : Eq (𝑖 ⇒ BA @𝑖) y y' =
+           δ 𝑗 ⇒ coe (𝑖 ⇒ BA @𝑖) @0 @𝑗 y;
+    in
+    0
+-}
+
+{-
+  δ 𝑖 ⇒
+    comp (𝑗 ⇒ sym¹ ★ A B AB @𝑗) @0 @𝑖 y @𝑖 {
+      0 𝑗 ⇒ xy @𝑗;
+      1 𝑗 ⇒ xy @𝑗
+    }
+-}
+
+def trans10 : 0.(A : ★) → 0.(x y z : A) →
+              1.(x ≡ y : A) → 0.(y ≡ z : A) → x ≡ z : A =
+  λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ x ≡ eq2 @𝑗 : A) eq1
+
+def trans01 : 0.(A : ★) → 0.(x y z : A) →
+              0.(x ≡ y : A) → 1.(y ≡ z : A) → x ≡ z : A =
+  λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ eq1 @𝑗 ≡ z : A) @1 @0 eq2
+
+def trans : 0.(A : ★) → 0.(x y z : A) →
+            ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
+  λ A x y z eq1 eq2 ⇒ trans01 A x y z eq1 eq2
+
+{-
+def trans-het : 0.(A B C : ★) → 0.(AB : A ≡ B : ★) → 0.(BC : B ≡ C : ★) →
+                0.(x : A) → 0.(y : B) → 0.(z : C) →
+                ω.(Eq (𝑖 ⇒ AB @𝑖) x y) →
+                ω.(Eq (𝑖 ⇒ BC @𝑖) y z) →
+                Eq (𝑖 ⇒ trans¹ ★ A B C AB BC @𝑖) x z
+=
+  λ A B C AB BC x y z xy yz ⇒
+    let 0.AC = trans¹ ★ A B C AB BC;
+        0.y' : A = coe (𝑗 ⇒ AB @𝑗) @1 @0 y;
+    in
+    δ 𝑖 ⇒
+    trans (AC @𝑖) (coe (𝑗 ⇒ AC @𝑗) @0 @𝑖 x)
+                  (coe (𝑗 ⇒ AC @𝑗) @0 @𝑖 y')
+                  (coe (𝑗 ⇒ AC @𝑗) @1 @𝑖 z)
+                  0
+                  0
+                  @𝑖
+
+def0 trans-trans-het :
+    (A : ★) → (x y z : A) →
+    (xy : x ≡ y : A) → (yz : y ≡ z : A) →
+    Eq (_ ⇒ x ≡ z : A)
+       (trans A x y z xy yz)
+       (trans-het A A A (δ _ ⇒ A) (δ _ ⇒ A) x y z xy yz) =
+  λ A x y z xy yz ⇒ δ _ ⇒ trans A x y z xy yz
+-}
+
+def appω : 0.(A B : ★) → ω.(f : ω.A → B) → [ω.A] → [ω.B] =
+  λ A B f x ⇒ case x return [ω.B] of { [x'] ⇒ [f x'] }
+def app# = appω
+
+def app2ω : 0.(A B C : ★) → ω.(f : ω.A → ω.B → C) → [ω.A] → [ω.B] → [ω.C] =
+  λ A B C f x y ⇒
+  case x return [ω.C] of { [x'] ⇒
+    case y return [ω.C] of { [y'] ⇒ [f x' y'] }
+  }
+def app2# = app2ω
+
+def getω : 0.(A : ★) → [ω.A] → A =
+  λ A x ⇒ case x return A of { [x] ⇒ x }
+def get# = getω
+
+def0 get0 : (A : ★) → [0.A] → A =
+  λ A x ⇒ case x return A of { [x] ⇒ x }
+
+def0 get0-box : (A : ★) → (b : [0.A]) →
+                [get0 A b] ≡ b : [0.A] =
+  λ A b ⇒ case b return b' ⇒ [get0 A b'] ≡ b' : [0.A] of { [x] ⇒ δ _ ⇒ [x] }
+
+def drop0 : 0.(A B : ★) → [0.A] → B → B =
+  λ A B x y ⇒ case x return B of { [_] ⇒ y }
+
+def0 drop0-eq : (A B : ★) → (x : [0.A]) → (y : B) → drop0 A B x y ≡ y : B =
+  λ A B x y ⇒
+  case x return x' ⇒ drop0 A B x' y ≡ y : B of { [_] ⇒ δ 𝑖 ⇒ y }
+
+def0 HEq : (A B : ★) → A → B → ★¹ =
+  λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y
+
+def0 boxω-inj : (A : ★) → (x y : A) → [x] ≡ [y] : [ω.A] → x ≡ y : A =
+  λ A x y xy ⇒ δ 𝑖 ⇒ getω A (xy @𝑖)
+-- [todo] change lexical syntax to allow "box#-inj"
+
+def revive0 : 0.(A : ★) → 0.[0.A] → [0.A] =
+  λ A s ⇒ [get0 A s]
+
+
+namespace sing {
+
+def0 Sing : (A : ★) → A → ★ =
+  λ A x ⇒ (val : A) × [0. val ≡ x : A]
+
+def sing : 0.(A : ★) → (x : A) → Sing A x =
+  λ A x ⇒ (x, [δ _ ⇒ x])
+
+def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
+  λ A x sg ⇒
+  case sg return A of { (x', eq) ⇒ drop0 (x' ≡ x : A) A eq x' }
+
+def0 val-fst : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ fst sg : A =
+  λ A x sg ⇒ drop0-eq (fst sg ≡ x : A) A (snd sg) (fst sg)
+
+def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
+  λ A x sg ⇒
+  trans A (val A x sg) (fst sg) x
+    (val-fst A x sg) (get0 (fst sg ≡ x : A) (snd sg))
+
+def app : 0.(A B : ★) → 0.(x : A) →
+          (f : A → B) → Sing A x → Sing B (f x) =
+  λ A B x f sg ⇒
+    let 1.x' = val A x sg;
+        0.xx = proof A x sg in
+    (f x', [δ 𝑖 ⇒ f (xx @𝑖)])
+
+}
+
+def0 Sing = sing.Sing
+def  sing = sing.sing
+
+
+namespace dup {
+
+def0 Dup : (A : ★) → A → ★ =
+  λ A x ⇒ Sing [ω.A] [x]
+
+def from-parts :
+    0.(A : ★) →
+    (dup : A → [ω.A]) →
+    0.(prf : (x : A) → dup x ≡ [x] : [ω.A]) →
+    (x : A) → Dup A x =
+  λ A dup prf x ⇒ (dup x, [prf x])
+
+def to-drop : 0.(A : ★) → (A → [ω.A]) → 0.(B : ★) → A → B → B =
+  λ A dup B x y ⇒ case dup x return B of { [_] ⇒ y }
+
+def erased : 0.(A : ★) → (x : [0.A]) → Dup [0.A] x =
+  λ A x ⇒ case x return x' ⇒ Dup [0.A] x' of { [x] ⇒ sing [ω.[0.A]] [[x]] }
+
+def valω : 0.(A : ★) → 0.(x : A) → Dup A x → [ω.A] =
+  λ A x ⇒ sing.val [ω.A] [x]
+def val# = valω
+
+def val : 0.(A : ★) → 0.(x : A) → Dup A x → A =
+  λ A x x! ⇒ getω A (valω A x x!)
+
+def0 proofω : (A : ★) → (x : A) → (x! : Dup A x) → valω A x x! ≡ [x] : [ω.A] =
+  λ A x x! ⇒ sing.proof [ω.A] [x] x!
+def0 proof# : (A : ★) → (x : A) → (x! : Dup A x) → val# A x x! ≡ [x] : [ω.A] =
+  proofω
+
+def0 proof : (A : ★) → (x : A) → (x! : Dup A x) → val A x x! ≡ x : A =
+  λ A x x! ⇒ δ 𝑖 ⇒ getω A (proofω A x x! @𝑖)
+
+def elim' : 0.(A : ★) → 0.(x : A) → 0.(P : A → ★) →
+            (ω.(x' : A) → 0.(x' ≡ x : A) → P x) → Dup A x → P x =
+  λ A x P f x! ⇒
+    let xω : [ω.A] = sing.val [ω.A] [x] x! in
+    case xω return xω' ⇒ 0.(xω' ≡ xω : [ω.A]) → P x of { [x'] ⇒ λ eq1 ⇒
+      let0 eq2 = sing.proof [ω.A] [x] x!;
+           eq  = boxω-inj A x' x (trans [ω.A] [x'] xω [x] eq1 eq2) in
+      f x' eq
+    } (δ _ ⇒ xω)
+
+def elim : 0.(A : ★) → 0.(x : A) → 0.(P : A → ★) →
+           (ω.(x' : A) → P x') → Dup A x → P x =
+  λ A x P f ⇒ elim' A x P (λ x' xx ⇒ coe (𝑖 ⇒ P (xx @𝑖)) (f x'))
+
+
+}
+
+def0 Dup = dup.Dup
diff --git a/stdlib/nat.quox b/stdlib/nat.quox
new file mode 100644
index 0000000..d2e620f
--- /dev/null
+++ b/stdlib/nat.quox
@@ -0,0 +1,297 @@
+load "misc.quox"
+load "bool.quox"
+load "either.quox"
+load "sub.quox"
+
+namespace nat {
+
+def elim-0-1 :
+    0.(P : ℕ → ★) →
+    ω.(P 0) → ω.(P 1) →
+    ω.(0.(n : ℕ) → P n → P (succ n)) →
+    (n : ℕ) → P n =
+  λ P p0 p1 ps n ⇒
+  case n return n' ⇒ P n' of {
+    zero    ⇒ p0;
+    succ n' ⇒
+      case n' return n'' ⇒ P (succ n'') of {
+        zero         ⇒ p1;
+        succ n'', IH ⇒ ps (succ n'') IH
+      }
+  }
+
+def elim-pair :
+    0.(P : ℕ → ℕ → ★) →
+    ω.(P 0 0) →
+    ω.(0.(n : ℕ)   → P 0 n → P 0 (succ n)) →
+    ω.(0.(m : ℕ)   → P m 0 → P (succ m) 0) →
+    ω.(0.(m n : ℕ) → P m n → P (succ m) (succ n)) →
+    (m n : ℕ) → P m n =
+  λ P zz zs sz ss m ⇒
+    case m return m' ⇒ (n : ℕ) → P m' n of {
+      0 ⇒ λ n ⇒ case n return n' ⇒ P 0 n' of {
+        0            ⇒ zz;
+        succ n', ihn ⇒ zs n' ihn
+      };
+      succ m', ihm ⇒ λ n ⇒ case n return n' ⇒ P (succ m') n' of {
+        0       ⇒ sz m' (ihm 0);
+        succ n' ⇒ ss m' n' (ihm n')
+      }
+    }
+
+def elim-pairω :
+    0.(P : ℕ → ℕ → ★) →
+    ω.(P 0 0) →
+    ω.(ω.(n : ℕ)   → ω.(P 0 n) → P 0 (succ n)) →
+    ω.(ω.(m : ℕ)   → ω.(P m 0) → P (succ m) 0) →
+    ω.(ω.(m n : ℕ) → ω.(P m n) → P (succ m) (succ n)) →
+    ω.(m n : ℕ) → P m n =
+  λ P zz zs sz ss m ⇒
+    caseω m return m' ⇒ ω.(n : ℕ) → P m' n of {
+      0 ⇒ λ n ⇒ caseω n return n' ⇒ P 0 n' of {
+        0              ⇒ zz;
+        succ n', ω.ihn ⇒ zs n' ihn
+      };
+      succ m', ω.ihm ⇒ λ n ⇒ caseω n return n' ⇒ P (succ m') n' of {
+        0       ⇒ sz m' (ihm 0);
+        succ n' ⇒ ss m' n' (ihm n')
+      }
+    }
+
+
+def succ-boxω : [ω.ℕ] → [ω.ℕ] =
+  λ n ⇒ case n return [ω.ℕ] of { [n] ⇒ [succ n] }
+
+#[compile-scheme "(lambda (n) n)"]
+def dup : ℕ → [ω.ℕ] =
+  λ n ⇒ case n return [ω.ℕ] of {
+    0          ⇒ [0];
+    succ _, n! ⇒ succ-boxω n!
+  }
+
+def0 dup-ok : (n : ℕ) → dup n ≡ [n] : [ω.ℕ] =
+  λ n ⇒
+  case n return n' ⇒ dup n' ≡ [n'] : [ω.ℕ] of {
+    0          ⇒ δ 𝑖 ⇒ [0];
+    succ _, ih ⇒ δ 𝑖 ⇒ succ-boxω (ih @𝑖)
+  }
+
+def dup! : (n : ℕ) → Dup ℕ n =
+  dup.from-parts ℕ dup dup-ok
+
+
+def drop : 0.(A : ★) → ℕ → A → A =
+  dup.to-drop ℕ dup
+
+
+def natopω' : 0.(A : ★) → ω.(ω.ℕ → ω.ℕ → A) → ℕ → ℕ → A =
+  λ A f m n ⇒
+    getω A (app2ω ℕ ℕ A f (dup m) (dup n))
+
+def natopω = natopω' ℕ
+
+#[compile-scheme "(lambda% (m n) (+ m n))"]
+def plus : ℕ → ℕ → ℕ =
+  λ m n ⇒
+  case m return ℕ of {
+    zero      ⇒ n;
+    succ _, p ⇒ succ p
+  }
+
+#[compile-scheme "(lambda% (m n) (* m n))"]
+def timesω : ω.ℕ → ω.ℕ → ℕ =
+  λ m n ⇒
+  case m return ℕ of {
+    zero      ⇒ zero;
+    succ _, t ⇒ plus n t
+  }
+
+def times = natopω timesω
+
+def pred : ℕ → ℕ = λ n ⇒ case n return ℕ of { zero ⇒ zero; succ n ⇒ n }
+
+def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
+  λ n ⇒ δ 𝑖 ⇒ n
+
+def succ-inj : 0.(m n : ℕ) → succ m ≡ succ n : ℕ → m ≡ n : ℕ =
+  λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖)
+
+#[compile-scheme "(lambda% (m n) (max 0 (- m n)))"]
+def minus : ℕ → ℕ → ℕ =
+  λ m n ⇒
+  (case n return ℕ → ℕ of {
+    zero      ⇒ λ m ⇒ m;
+    succ _, f ⇒ λ m ⇒ f (pred m)
+  }) m
+
+
+def minω : ω.ℕ → ω.ℕ → ℕ =
+  elim-pairω (λ _ _ ⇒ ℕ) 0 (λ _ _ ⇒ 0) (λ _ _ ⇒ 0) (λ _ _ x ⇒ succ x)
+
+def min = natopω minω
+
+
+def0 IsSucc : ℕ → ★ =
+  λ n ⇒ case n return ★ of { zero ⇒ False; succ _ ⇒ True }
+
+def is-succ? : ω.(n : ℕ) → Dec (IsSucc n) =
+  λ n ⇒
+  caseω n return n' ⇒ Dec (IsSucc n') of {
+    zero   ⇒ No  (IsSucc zero)      (λ v ⇒ v);
+    succ n ⇒ Yes (IsSucc (succ n)) 'true
+  }
+
+def zero-not-succ : 0.(m : ℕ) → Not (zero ≡ succ m : ℕ) =
+  λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) @1 @0 'true
+
+def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) =
+  λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) 'true
+
+def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) =
+  λ m ⇒
+  case m return m' ⇒ Not (m' ≡ succ m' : ℕ) of {
+    zero         ⇒ zero-not-succ 0;
+    succ n, ω.ih ⇒ λ eq ⇒ ih (succ-inj n (succ n) eq)
+  }
+
+
+def0 IsSuccOf : ℕ → ℕ → ★ =
+  λ n p ⇒ n ≡ succ p : ℕ
+
+def0 PredOf : ℕ → ★ =
+  λ n ⇒ Sub ℕ (IsSuccOf n)
+
+def0 no-pred0 : Not (PredOf 0) =
+  λ p ⇒
+  case p return False of { (p, lt) ⇒
+    zero-not-succ p (get0 (0 ≡ succ p : ℕ) lt)
+  }
+
+def pred? : (n : ℕ) → DecT (PredOf n) =
+  λ n ⇒
+  case n return n' ⇒ DecT (PredOf n') of {
+    zero   ⇒ NoT  (PredOf zero)     no-pred0;
+    succ n ⇒ YesT (PredOf (succ n)) (n, [δ _ ⇒ succ n])
+  }
+
+namespace pred-of {
+
+def revive : (n : ℕ) → 0.(PredOf n) → PredOf n =
+  λ n hs ⇒
+    let0 p = fst hs in
+    case n return n' ⇒ 0.(n' ≡ succ p : ℕ) → PredOf n' of {
+      zero    ⇒ λ eq ⇒ void (PredOf zero) (zero-not-succ p eq);
+      succ p' ⇒ λ _  ⇒ (p', [δ _ ⇒ succ p'])
+    } (get0 (n ≡ succ p : ℕ) (snd hs))
+
+def val : 0.(n : ℕ) → PredOf n → ℕ =
+  λ n ⇒ sub.val ℕ (IsSuccOf n)
+
+def0 proof : (n : ℕ) → (p : PredOf n) → n ≡ succ (fst p) : ℕ =
+  λ n ⇒ sub.proof ℕ (IsSuccOf n)
+
+}
+
+
+def divmodω : ω.ℕ → ω.ℕ → ℕ × ℕ =
+  -- https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Init.Nat.html#divmod
+  letω divmod' : ℕ → ω.ℕ → ℕ → ℕ → ℕ × ℕ =
+    λ x ⇒
+    case x return ω.ℕ → ℕ → ℕ → ℕ × ℕ of {
+      0          ⇒ λ y q u ⇒ (q, u);
+      succ _, f' ⇒ λ y q u ⇒
+        case u return ℕ × ℕ of {
+          0       ⇒ f' y (succ q) y;
+          succ u' ⇒ f' y q u'
+        }
+    } in
+  λ x y ⇒
+  caseω y return ℕ × ℕ of {
+    0       ⇒ (0, 0);
+    succ y' ⇒
+      case divmod' x y' 0 y' return ℕ × ℕ of { (d, m) ⇒ (d, minus y' m) }
+  }
+
+def divmod = natopω' (ℕ × ℕ) divmodω
+
+def divω : ω.ℕ → ω.ℕ → ℕ = λ x y ⇒ fst (divmodω x y)
+def div = natopω divω
+
+def modω : ω.ℕ → ω.ℕ → ℕ = λ x y ⇒ snd (divmodω x y)
+def mod = natopω modω
+
+
+#[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"]
+def eq? : DecEq ℕ =
+  λ m n ⇒
+  elim-pair (λ m n ⇒ Dec (m ≡ n : ℕ))
+    (Yes (0 ≡ 0 : ℕ) (δ 𝑖 ⇒ 0))
+    (λ n p ⇒
+      dec.drop (0 ≡ n : ℕ) (Dec (0 ≡ succ n : ℕ)) p
+        (No (0 ≡ succ n : ℕ) (λ zs ⇒ zero-not-succ n zs)))
+    (λ m p ⇒
+      dec.drop (m ≡ 0 : ℕ) (Dec (succ m ≡ 0 : ℕ)) p
+        (No (succ m ≡ 0 : ℕ) (λ sz ⇒ succ-not-zero m sz)))
+    (λ m n ⇒
+      dec.elim (m ≡ n : ℕ) (λ _ ⇒ Dec (succ m ≡ succ n : ℕ))
+        (λ yy ⇒ Yes (succ m ≡ succ n : ℕ) (δ 𝑖  ⇒ succ (yy @𝑖)))
+        (λ nn ⇒ No  (succ m ≡ succ n : ℕ) (λ yy ⇒ nn (succ-inj m n yy))))
+    m n
+
+
+def0 Ordering : ★ = {lt, eq, gt}
+
+namespace ordering {
+  def from : 0.(A : ★) → ω.A → ω.A → ω.A → Ordering → A =
+    λ A lt eq gt o ⇒
+    case o return A of { 'lt ⇒ lt; 'eq ⇒ eq; 'gt ⇒ gt }
+
+  def drop : 0.(A : ★) → Ordering → A → A =
+    λ A o x ⇒ case o return A of { 'lt ⇒ x; 'eq ⇒ x; 'gt ⇒ x }
+
+  def eq : Ordering → Ordering → Bool =
+    λ x y ⇒
+    case x return Bool of {
+      'lt ⇒ case y return Bool of { 'lt ⇒ 'true;  'eq ⇒ 'false; 'gt ⇒ 'false };
+      'eq ⇒ case y return Bool of { 'lt ⇒ 'false; 'eq ⇒ 'true;  'gt ⇒ 'false };
+      'gt ⇒ case y return Bool of { 'lt ⇒ 'false; 'eq ⇒ 'false; 'gt ⇒ 'true  };
+    }
+}
+
+def compare : ℕ → ℕ → Ordering =
+  elim-pair (λ _ _ ⇒ Ordering)
+    'eq
+    (λ _ o   ⇒ ordering.drop Ordering o 'lt)
+    (λ _ o   ⇒ ordering.drop Ordering o 'gt)
+    (λ _ _ x ⇒ x)
+
+def lt : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ ordering.eq (compare m n) 'lt
+def eq : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ ordering.eq (compare m n) 'eq
+def gt : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ ordering.eq (compare m n) 'gt
+def ne : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ bool.not (eq m n)
+def le : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ bool.not (gt m n)
+def ge : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ bool.not (lt m n)
+
+
+def0 plus-zero : (m : ℕ) → m ≡ plus m 0 : ℕ =
+  λ m ⇒
+  case m return m' ⇒ m' ≡ plus m' 0 : ℕ of {
+    zero        ⇒ δ _ ⇒ 0;
+    succ m', ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
+  }
+
+def0 plus-succ : (m n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ =
+  λ m n ⇒
+  case m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of {
+    zero       ⇒ δ _ ⇒ succ n;
+    succ _, ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
+  }
+
+def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ =
+  λ m ⇒
+  case m return m' ⇒ 0 ≡ timesω m' 0 : ℕ of {
+    zero        ⇒ δ _ ⇒ zero;
+    succ m', ih ⇒ ih
+  }
+
+}
diff --git a/stdlib/pair.quox b/stdlib/pair.quox
new file mode 100644
index 0000000..9f93009
--- /dev/null
+++ b/stdlib/pair.quox
@@ -0,0 +1,67 @@
+namespace pair {
+
+def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x
+
+def uncurry :
+    0.(A : ★) → 0.(B : A → ★) → 0.(C : (x : A) → (B x) → ★) →
+    (f : (x : A) → (y : B x) → C x y) →
+    (p : Σ A B) → C (fst p) (snd p) =
+  λ A B C f p ⇒
+    case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y }
+
+def uncurry' :
+    0.(A B C : ★) → (A → B → C) → (A × B) → C =
+  λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C)
+
+def curry :
+    0.(A : ★) → 0.(B : A → ★) → 0.(C : (Σ A B) → ★) →
+    (f : (p : Σ A B) → C p) → (x : A) → (y : B x) → C (x, y) =
+  λ A B C f x y ⇒ f (x, y)
+
+def curry' :
+    0.(A B C : ★) → (A × B → C) → A → B → C =
+  λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C)
+
+def0 fst-snd :
+    (A : ★) → (B : A → ★) →
+    (p : Σ A B) → p ≡ (fst p, snd p) : Σ A B =
+  λ A B p ⇒ δ 𝑖 ⇒ p -- η
+
+def0 fst-eq :
+    (A : ★) → (B : A → ★) →
+    (p q : Σ A B) → p ≡ q : Σ A B → fst p ≡ fst q : A =
+  λ A B p q eq ⇒ δ 𝑖 ⇒ fst (eq @𝑖)
+
+def0 snd-eq :
+    (A : ★) → (B : A → ★) →
+    (p q : Σ A B) → (eq : p ≡ q : Σ A B) →
+    Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd p) (snd q) =
+  λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖)
+
+def0 pair-eq :
+    (A : ★) → (B : A → ★) →
+    (x0 x1 : A) → (y0 : B x0) → (y1 : B x1) →
+    (xx : x0 ≡ x1 : A) → (yy : Eq (𝑖 ⇒ B (xx @𝑖)) y0 y1) →
+    (x0, y0) ≡ (x1, y1) : ((x : A) × B x) =
+  λ A B x0 x1 y0 y1 xx yy ⇒ δ 𝑖 ⇒ (xx @𝑖, yy @𝑖)
+
+def map :
+    0.(A A' : ★) →
+    0.(B : A → ★) → 0.(B' : A' → ★) →
+    (f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
+    Σ A B → Σ A' B' =
+  λ A A' B B' f g p ⇒
+    case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) }
+
+def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' =
+  λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g)
+
+def map-fst : 0.(A A' B : ★) → (A → A') → A × B → A' × B =
+  λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x)
+
+def map-snd : 0.(A B B' : ★) → (B → B') → A × B → A × B' =
+  λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f
+
+}
+
+def0 Σ   = pair.Σ
diff --git a/stdlib/qty.quox b/stdlib/qty.quox
new file mode 100644
index 0000000..673b4d4
--- /dev/null
+++ b/stdlib/qty.quox
@@ -0,0 +1,156 @@
+load "misc.quox"
+
+def0 Qty : ★ = {"zero", one, any}
+
+def0 NzQty : ★ = {one, any}
+
+def nz : NzQty → Qty =
+  λ π ⇒ case π return Qty of { 'one ⇒ 'one; 'any ⇒ 'any }
+
+def dup! : (π : Qty) → Dup Qty π =
+  λ π ⇒ case π return π' ⇒ Dup Qty π' of {
+    'zero ⇒ (['zero], [δ _ ⇒ ['zero]]);
+    'one  ⇒ (['one],  [δ _ ⇒ ['one]]);
+    'any  ⇒ (['any],  [δ _ ⇒ ['any]]);
+  }
+
+def dup : (π : Qty) → [ω.Qty] =
+  λ π ⇒ dup.valω Qty π (dup! π)
+
+def drop : 0.(A : ★) → Qty → A → A =
+  λ A π x ⇒ case π return A of {
+    'zero ⇒ x;
+    'one  ⇒ x;
+    'any  ⇒ x;
+  }
+
+def if-zero : 0.(A : ★) → Qty → ω.A → ω.A → A =
+  λ A π z nz ⇒
+  case π return A of { 'zero ⇒ z; 'one ⇒ nz; 'any ⇒ nz }
+
+def plus : Qty → ω.Qty → Qty =
+  λ π ρ ⇒
+  case π return Qty of {
+    'zero ⇒ ρ;
+    'one  ⇒ if-zero Qty ρ 'one 'any;
+    'any  ⇒ 'any;
+  }
+
+def times : Qty → ω.Qty → Qty =
+  λ π ρ ⇒
+  case π return Qty of {
+    'zero ⇒ 'zero;
+    'one  ⇒ ρ;
+    'any  ⇒ if-zero Qty ρ 'zero 'any;
+  }
+
+def0 FUN : Qty → (A : ★) → (A → ★) → ★ =
+  λ π A B ⇒
+  case π return ★ of {
+    'zero ⇒ 0.(x : A) → B x;
+    'one  ⇒ 1.(x : A) → B x;
+    'any  ⇒ ω.(x : A) → B x;
+  }
+
+def0 FUN-NZ : NzQty → (A : ★) → (A → ★) → ★ =
+  λ π A B ⇒
+  case π return ★ of {
+    'one  ⇒ 1.(x : A) → B x;
+    'any  ⇒ ω.(x : A) → B x;
+  }
+
+def0 Fun : Qty → ★ → ★ → ★ =
+  λ π A B ⇒ FUN π A (λ _ ⇒ B)
+
+def0 FunNz : NzQty → ★ → ★ → ★ =
+  λ π A B ⇒ FUN-NZ π A (λ _ ⇒ B)
+
+def0 Box : Qty → ★ → ★ =
+  λ π A ⇒
+  case π return ★ of {
+    'zero ⇒ [0.A];
+    'one  ⇒ [1.A];
+    'any  ⇒ [ω.A];
+  }
+
+def0 BoxNz : NzQty → ★ → ★ =
+  λ π A ⇒
+  case π return ★ of {
+    'one  ⇒ [1.A];
+    'any  ⇒ [ω.A];
+  }
+
+def0 unbox : (π : Qty) → (A : ★) → Box π A → A =
+  λ π A ⇒
+  case π return π' ⇒ Box π' A → A of {
+    'zero ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+    'one  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+    'any  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+  }
+
+def0 unbox0 = unbox 'zero
+def0 unbox1 = unbox 'one
+def0 unboxω = unbox 'any
+
+def0 unbox-nz : (π : NzQty) → (A : ★) → BoxNz π A → A =
+  λ π A ⇒
+  case π return π' ⇒ BoxNz π' A → A of {
+    'one  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+    'any  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+  }
+
+def0 unbox-nz1 = unbox-nz 'one
+def0 unbox-nzω = unbox-nz 'any
+
+def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
+            FUN π A B → (x : Box π A) → B (unbox π A x) =
+  λ π A B ⇒
+  case π
+  return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x)
+  of {
+    'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox0 A x') of { [x] ⇒ f x };
+    'one  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox1 A x') of { [x] ⇒ f x };
+    'any  ⇒ λ f x ⇒ case x return x' ⇒ B (unboxω A x') of { [x] ⇒ f x };
+  }
+
+def apply' : (π : Qty) → 0.(A B : ★) → Fun π A B → (x : Box π A) → B =
+  λ π A B ⇒ apply π A (λ _ ⇒ B)
+
+def apply-nz : (π : NzQty) → 0.(A : ★) → 0.(B : A → ★) →
+               FUN-NZ π A B → (x : BoxNz π A) → B (unbox-nz π A x) =
+  λ π A B ⇒
+  case π
+  return π' ⇒ FUN-NZ π' A B → (x : BoxNz π' A) → B (unbox-nz π' A x)
+  of {
+    'one  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox-nz1 A x') of { [x] ⇒ f x };
+    'any  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox-nzω A x') of { [x] ⇒ f x };
+  }
+
+def apply-nz' : (π : NzQty) → 0.(A B : ★) → FunNz π A B → (x : BoxNz π A) → B =
+  λ π A B ⇒ apply-nz π A (λ _ ⇒ B)
+
+def lam : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
+          ((x : Box π A) → B (unbox π A x)) → FUN π A B =
+  λ π A B ⇒
+    case π
+    return π' ⇒ ((x : Box π' A) → B (unbox π' A x)) → FUN π' A B of {
+      'zero ⇒ λ f x ⇒ f [x];
+      'one  ⇒ λ f x ⇒ f [x];
+      'any  ⇒ λ f x ⇒ f [x];
+    }
+
+def lam' : (π : Qty) → 0.(A B : ★) → (Box π A → B) → Fun π A B =
+  λ π A B ⇒ lam π A (λ _ ⇒ B)
+
+def lam-nz : (π : NzQty) → 0.(A : ★) → 0.(B : A → ★) →
+             ((x : BoxNz π A) → B (unbox-nz π A x)) → FUN-NZ π A B =
+  λ π A B ⇒
+    case π
+    return π' ⇒ ((x : BoxNz π' A) → B (unbox-nz π' A x)) → FUN-NZ π' A B of {
+      'one  ⇒ λ f x ⇒ f [x];
+      'any  ⇒ λ f x ⇒ f [x];
+    }
+
+def lam-nz' : (π : NzQty) → 0.(A B : ★) → (BoxNz π A → B) → FunNz π A B =
+  λ π A B ⇒ lam-nz π A (λ _ ⇒ B)
+
diff --git a/stdlib/string.quox b/stdlib/string.quox
new file mode 100644
index 0000000..f59c799
--- /dev/null
+++ b/stdlib/string.quox
@@ -0,0 +1,144 @@
+load "bool.quox"
+load "list.quox"
+load "maybe.quox"
+load "either.quox"
+
+namespace char {
+
+postulate0 Char : ★
+
+#[compile-scheme "(lambda (c) c)"]
+postulate dup : Char → [ω.Char]
+
+#[compile-scheme "char->integer"]
+postulate to-ℕ : Char → ℕ
+
+#[compile-scheme "integer->char"]
+postulate from-ℕ : ℕ → Char
+
+def space   = from-ℕ 0x20
+def tab     = from-ℕ 0x09
+def newline = from-ℕ 0x0a
+
+def test-via-ℕ : (ω.ℕ → ω.ℕ → Bool) → (ω.Char → ω.Char → Bool) =
+  λ p c d ⇒ p (to-ℕ c) (to-ℕ d)
+def lt = test-via-ℕ nat.lt
+def eq = test-via-ℕ nat.eq
+def gt = test-via-ℕ nat.gt
+def le = test-via-ℕ nat.le
+def ne = test-via-ℕ nat.ne
+def ge = test-via-ℕ nat.ge
+
+postulate0 eq-iff-nat : (c d : Char) → Iff (c ≡ d : Char) (to-ℕ c ≡ to-ℕ d : ℕ)
+
+def eq? : DecEq Char =
+  λ c d ⇒
+  let0 Ty = (c ≡ d : Char) ∷ ★ in
+  dec.elim (to-ℕ c ≡ to-ℕ d : ℕ) (λ _ ⇒ Dec Ty)
+    (λ y ⇒ Yes Ty ((snd (eq-iff-nat c d)) y))
+    (λ n ⇒ No  Ty (λ y ⇒ n ((fst (eq-iff-nat c d)) y)))
+    (nat.eq? (to-ℕ c) (to-ℕ d))
+
+def ws? : ω.Char → Bool =
+  λ c ⇒ bool.or (bool.or (eq c space) (eq c tab)) (eq c newline)
+
+def digit? : ω.Char → Bool =
+  λ c ⇒ bool.and (ge c (from-ℕ 0x30)) (le c (from-ℕ 0x39))
+
+def digit-val : Char → Maybe ℕ =
+  λ c ⇒ case dup c return Maybe ℕ of { [c] ⇒
+    bool.if (Maybe ℕ) (digit? c)
+      (Just ℕ (nat.minus (to-ℕ c) 0x30))
+      (Nothing ℕ)
+  }
+
+}
+
+def0 Char = char.Char
+
+namespace string {
+
+#[compile-scheme "string->list"]
+postulate to-scheme-list : String → list.SchemeList Char
+
+def to-list : String → List Char =
+  λ str ⇒ list.from-scheme Char (to-scheme-list str)
+
+#[compile-scheme "list->string"]
+postulate from-scheme-list : list.SchemeList Char → String
+
+def from-list : List Char → String =
+  λ cs ⇒ from-scheme-list (list.to-scheme Char cs)
+
+def foldl : 0.(A : ★) → A → ω.(A → Char → A) → String → A =
+  λ A z f str ⇒ list.foldl Char A z f (to-list str)
+
+def foldlω : 0.(A : ★) → ω.A → ω.(ω.A → ω.Char → A) → ω.String → A =
+  λ A z f str ⇒ list.foldlω Char A z f (to-list str)
+
+def split : ω.(ω.Char → Bool) → ω.String → List String =
+  λ p str ⇒
+    list.map (List Char) String from-list
+      (list.split Char p (to-list str))
+
+def break : ω.(ω.Char → Bool) → ω.String → String × String =
+  λ p str ⇒
+  letω pair = list.break Char p (to-list str) in
+  (from-list (fst pair), from-list (snd pair))
+
+def reverse : String → String =
+  λ str ⇒ from-list (list.reverse Char (to-list str))
+
+#[compile-scheme "(lambda% (y n a b) (if (string=? a b) y n))"]
+postulate eq' : 0.(A : ★) → A → A → ω.String → ω.String → A
+def eq : ω.String → ω.String → Bool = eq' Bool 'true 'false
+
+def null : ω.String → Bool = eq ""
+def not-null : ω.String → Bool = λ s ⇒ bool.not (null s)
+
+#[compile-scheme "(lambda (str) str)"]
+postulate dup : String → [ω.String]
+
+postulate0 dup-ok : (str : String) → dup str ≡ [str] : [ω.String]
+
+def dup! : (str : String) → Dup String str =
+  dup-from-parts String dup dup-ok
+
+
+def to-ℕ : String → Maybe ℕ =
+  letω add-digit : Maybe ℕ → ℕ → Maybe ℕ =
+    maybe.fold ℕ (ℕ → Maybe ℕ) (λ d ⇒ Just ℕ d)
+      (λ n d ⇒ Just ℕ (nat.plus (nat.times 10 n) d)) in
+  letω drop : Maybe ℕ → Maybe ℕ =
+    maybe.fold ℕ (Maybe ℕ) (Nothing ℕ)
+      (λ n ⇒ nat.drop (Maybe ℕ) n (Nothing ℕ)) in
+  letω add-digit-c : Maybe ℕ → Char → Maybe ℕ =
+    λ acc c ⇒
+      maybe.fold ℕ (Maybe ℕ → Maybe ℕ) drop (λ n acc ⇒ add-digit acc n)
+        (char.digit-val c) acc in
+  λ str ⇒
+    case dup str return Maybe ℕ of { [str] ⇒
+      bool.if (Maybe ℕ) (not-null str)
+        (foldl (Maybe ℕ) (Just ℕ 0) add-digit-c str)
+        (Nothing ℕ)
+    }
+
+def to-ℕ-or-0 : String → ℕ =
+  λ str ⇒ maybe.fold ℕ ℕ 0 (λ x ⇒ x) (to-ℕ str)
+
+
+#[compile-scheme
+ "(lambda% (yes no str)
+    (let [(len (string-length str))]
+      (if (= len 0)
+        no
+        (let [(first (string-ref str 0))
+              (rest  (substring str 1 len))]
+          (% yes first rest)))))"]
+postulate uncons' : 0.(A : ★) → ω.A → ω.(Char → String → A) → String → A
+
+def uncons : String → Maybe (Char × String) =
+  let0 Pair : ★ = Char × String in
+  uncons' (Maybe Pair) (Nothing Pair) (λ c s ⇒ Just Pair (c, s))
+
+}
diff --git a/stdlib/sub.quox b/stdlib/sub.quox
new file mode 100644
index 0000000..61128a4
--- /dev/null
+++ b/stdlib/sub.quox
@@ -0,0 +1,159 @@
+load "misc.quox"
+load "either.quox"
+load "maybe.quox"
+
+namespace sub {
+
+def0 Irr : (A : ★) → ★ =
+  λ A ⇒ (x y : A) → x ≡ y : A
+
+def0 Irr1 : (A : ★) → (A → ★) → ★ =
+  λ A P ⇒ (x : A) → Irr (P x)
+
+def0 Irr2 : (A B : ★) → (A → B → ★) → ★ =
+  λ A B P ⇒ (x : A) → (y : B) → Irr (P x y)
+
+def0 Sub : (A : ★) → (P : A → ★) → ★ =
+  λ A P ⇒ (x : A) × [0. P x]
+
+
+def sub : 0.(A : ★) → 0.(P : A → ★) → (x : A) → 0.(P x) → Sub A P =
+  λ A P x p ⇒ (x, [p])
+
+def sub? : 0.(A : ★) → 0.(P : A → ★) → (ω.(x : A) → Dec (P x)) →
+           ω.A → Maybe (Sub A P) =
+  λ A P p? x ⇒
+    dec.elim (P x) (λ _ ⇒ Maybe (Sub A P))
+      (λ y ⇒ Just (Sub A P) (x, [y]))
+      (λ n ⇒ Nothing (Sub A P))
+      (p? x)
+
+
+def val : 0.(A : ★) → 0.(P : A → ★) → Sub A P → A =
+  λ A P s ⇒ case s return A of { (x, p) ⇒ drop0 (P x) A p x }
+
+def0 proof : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (fst s) =
+  λ A P s ⇒ get0 (P (fst s)) (snd s)
+
+{-
+
+def0 proof' : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (fst s) =
+  λ A P s ⇒ get0 (P (fst s)) (snd s)
+
+def0 val-fst : (A : ★) → (P : A → ★) →
+               (s : Sub A P) → val A P s ≡ fst s : A =
+  λ A P s ⇒
+    case s return s' ⇒ val A P s' ≡ fst s' : A of {
+      (x, p) ⇒ drop0-eq (P x) A p x
+    }
+
+def0 proof : 0.(A : ★) → 0.(P : A → ★) → (s : Sub A P) → P (val A P s) =
+  λ A P s ⇒ coe (𝑖 ⇒ P (val-fst A P s @𝑖)) @1 @0 (proof' A P s)
+
+postulate0 proof-snd' : (A : ★) → (P : A → ★) → (s : Sub A P) →
+                  Eq (𝑖 ⇒ P (val-fst A P s @𝑖)) (proof A P s) (proof' A P s)
+
+postulate0 proof-snd : (A : ★) → (P : A → ★) → (s : Sub A P) →
+                 Eq (𝑖 ⇒ [0.P (val-fst A P s @𝑖)]) [proof A P s] (snd s)
+
+#![log (all, 10) (equal, 100)]
+def0 val-proof-eq : (A : ★) → (P : A → ★) → (s : Sub A P) →
+                    sub A P (val A P s) (proof A P s) ≡ s : Sub A P =
+  λ A P s ⇒
+    case s return s' ⇒ sub A P (val A P s') (proof A P s') ≡ s' : Sub A P
+    of { (xxxxx, p) ⇒
+      case p
+      return p' ⇒
+        sub A P (val A P (xxxxx, p')) (proof A P (xxxxx, p')) ≡ (xxxxx, p') : Sub A P
+      of { [p0] ⇒
+        δ 𝑖 ⇒ (val-fst A P (xxxxx, [p0]) @𝑖, proof-snd A P (xxxxx, [p0]) @𝑖)
+      }
+    }
+#![log pop]
+
+def elim' : 0.(A : ★) → 0.(P : A → ★) →
+            0.(R : (x : A) → P x → ★) →
+            (1.(x : A) → 0.(p : P x) → R x p) →
+            (s : Sub A P) → R (val A P s) (proof A P s) =
+  λ A P R p s ⇒ p (val A P s) (proof A P s)
+
+{-
+def elim : 0.(A : ★) → 0.(P : A → ★) →
+           0.(R : Sub A P → ★) →
+           (1.(x : A) → 0.(p : P x) → R (x, [p])) →
+           (s : Sub A P) → R s =
+  λ A P R p s ⇒ p (val A P s) (proof A P s)
+-}
+
+-}
+
+
+
+def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ =
+  λ A P s ⇒ Dup A (fst s)
+    -- (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]]
+
+def subdup-to-dup :
+    0.(A : ★) → 0.(P : A → ★) →
+    0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s =
+  λ A P s sd ⇒
+    case sd return Dup (Sub A P) s of { (sω, ss0) ⇒
+    case ss0 return Dup (Sub A P) s of { [ss0] ⇒
+      case sω
+      return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s
+      of { [s!] ⇒ λ ss' ⇒
+        let ω.p  : [0.P (fst s)] = revive0 (P (fst s)) (snd s);
+            0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss' in
+        ([(s!, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @0 p)],
+         [δ 𝑗 ⇒ [(ss @𝑗, coe (𝑖 ⇒ [0.P (ss @𝑖)]) @1 @𝑗 p)]])
+      } ss0
+    }}
+
+def subdup : 0.(A : ★) → 0.(P : A → ★) →
+             ((x : A) → Dup A x) →
+             (s : Sub A P) → SubDup A P s =
+  λ A P dup s ⇒
+    case s return s' ⇒ SubDup A P s' of { (x, p) ⇒
+      drop0 (P x) (Dup A x) p (dup x)
+    }
+
+def dup! : 0.(A : ★) → 0.(P : A → ★) → ((x : A) → Dup A x) →
+           (s : Sub A P) → Dup (Sub A P) s =
+  λ A P dupA s ⇒ subdup-to-dup A P s (subdup A P dupA s)
+
+
+def0 irr1-het : (A : ★) → (P : A → ★) → Irr1 A P →
+                (x y : A) → (p : P x) → (q : P y) →
+                (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) p q =
+  λ A P pirr x y p q xy ⇒ δ 𝑖 ⇒
+    pirr (xy @𝑖) (coe (𝑗 ⇒ P (xy @𝑗)) @0 @𝑖 p) (coe (𝑗 ⇒ P (xy @𝑗)) @1 @𝑖 q) @𝑖
+
+def0 irr2-het : (A B : ★) → (P : A → B → ★) → Irr2 A B P →
+                (x₀ x₁ : A) → (y₀ y₁ : B) → (p : P x₀ y₀) → (q : P x₁ y₁) →
+                (xx : x₀ ≡ x₁ : A) → (yy : y₀ ≡ y₁ : B) →
+                Eq (𝑖 ⇒ P (xx @𝑖) (yy @𝑖)) p q =
+  λ A B P pirr x₀ x₁ y₀ y₁ p q xx yy ⇒ δ 𝑖 ⇒
+    pirr (xx @𝑖) (yy @𝑖)
+         (coe (𝑗 ⇒ P (xx @𝑗) (yy @𝑗)) @0 @𝑖 p)
+         (coe (𝑗 ⇒ P (xx @𝑗) (yy @𝑗)) @1 @𝑖 q) @𝑖
+
+
+def0 sub-eq : (A : ★) → (P : A → ★) → Irr1 A P →
+              (x y : Sub A P) → fst x ≡ fst y : A → x ≡ y : Sub A P =
+  λ A P pirr x y xy0 ⇒ δ 𝑖 ⇒
+    let proof = proof A P in
+    (xy0 @𝑖, [irr1-het A P pirr (fst x) (fst y) (proof x) (proof y) xy0 @𝑖])
+
+
+def eq? : 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) →
+          DecEq A → DecEq (Sub A P) =
+  λ A P pirr aeq? s t ⇒
+    let0 EQ : ★ = s ≡ t : Sub A P in
+    dec.elim (fst s ≡ fst t : A) (λ _ ⇒ Dec EQ)
+      (λ y ⇒ Yes EQ (sub-eq A P pirr s t y))
+      (λ n ⇒ No  EQ (λ eq ⇒ n (δ 𝑖 ⇒ fst (eq @𝑖))))
+      (aeq? (fst s) (fst t))
+
+}
+
+def0 Sub = sub.Sub