some more example stuff

examples/bool.quox

@@ -4,19 +4,25 @@ 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-dep¹ (λ _ ⇒ ★) b A B);
+
+def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False;
+
 def boolω : Bool → [ω.Bool] =
-  λ b ⇒ case b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };
-
-def if : 0.(A : ★) → Bool → ω.A → ω.A → A =
-  λ A b t f ⇒ case b return A of { 'true ⇒ t; 'false ⇒ f };
-
-def0 If : Bool → ★ → ★ → ★ =
-  λ b T F ⇒ case b return ★ of { 'true ⇒ T; 'false ⇒ F };
-
-def0 T : Bool → ★ = λ b ⇒ If b True False;
+  λ b ⇒ if [ω.Bool] b ['true] ['false];
 
 def true-not-false : Not ('true ≡ 'false : Bool) =
-  λ eq ⇒ coe (i ⇒ T (eq @i)) 'true;
+  λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true;
 
 
 -- [todo] infix

examples/list.quox

@@ -1,6 +1,6 @@
 load "nat.quox";
 
-namespace list {
+namespace vec {
 
 def0 Vec : ℕ → ★ → ★ =
   λ n A ⇒
@@ -9,33 +9,58 @@ def0 Vec : ℕ → ★ → ★ =
     succ _, 0.Tail ⇒ A × Tail
   };
 
+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 ⇒ λ n ⇒
+        case n return n' ⇒ P 0 n' of { 'nil ⇒ pn };
+      succ n, ih ⇒ λ c ⇒
+        case c return c' ⇒ P (succ n) c' of {
+          (first, rest) ⇒ pc first n rest (ih rest)
+        }
+    };
+
+}
+
+def0 Vec = vec.Vec;
+
+
+namespace list {
+
 def0 List : ★ → ★ =
   λ A ⇒ (len : ℕ) × Vec len A;
 
-def nil : 0.(A : ★) → List A =
+def Nil : 0.(A : ★) → List A =
   λ A ⇒ (0, 'nil);
 
-def cons : 0.(A : ★) → A → List A → List A =
+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 foldr' : 0.(A B : ★) →
-             B → ω.(A → B → B) → (n : ℕ) → Vec n A → B =
-  λ A B z c n ⇒
-  case n return n' ⇒ Vec n' A → B of {
-    zero ⇒
-      λ nil ⇒ case nil return B of { 'nil ⇒ z };
-    succ n, 1.ih ⇒
-      λ cons ⇒ case cons return B of { (first, rest) ⇒ c first (ih rest) }
-  };
+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 foldr : 0.(A B : ★) → B → ω.(A → B → B) → List A → B =
-  λ A B z c xs ⇒
-  case xs return B of { (len, elems) ⇒ foldr' A B z c len elems };
+  λ A B z f xs ⇒ elim A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs;
 
-def sum : List ℕ → ℕ = foldr ℕ ℕ 0 nat.plus;
+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);
 
-def numbers : List ℕ = (5, (0, 1, 2, 3, 4, 'nil));
-
-def number-sum : sum numbers ≡ 10 : ℕ = δ _ ⇒ 10;
+-- [fixme] the List¹ in the last argument is a bit weird
+def0 All : (A : ★) → (P : A → ★) → List¹ A → ★ =
+  λ A P ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps);
 
 }
+
+def0 List = list.List;

examples/maybe.quox

@@ -42,7 +42,7 @@ def0 nothing-unique :
 
 def elim :
     0.(A : ★) →
-    0.(P : 0.(Maybe A) → ★) →
+    0.(P : Maybe A → ★) →
     ω.(P (Nothing A)) →
     ω.((x : A) → P (Just A x)) →
     (x : Maybe A) → P x =