examples

examples/list.quox

@@ -1,4 +1,3 @@
-
 def0 Vec : 0.ℕ → 0.★₀ → ★₀ =
   λ n A ⇒
   caseω n return ★₀ of {
@@ -9,81 +8,31 @@ def0 Vec : 0.ℕ → 0.★₀ → ★₀ =
 def0 List : 0.★₀ → ★₀ =
   λ A ⇒ (len : ℕ) × Vec len A;
 
-
-defω nil : 0.(A : ★₀) → List 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) };
 
-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)
+def foldr' : 0.(A : ★₀) → 0.(B : ★₀) →
+             1.B → ω.(1.A → 1.B → B) → 1.(n : ℕ) → 1.(Vec n A) → B =
+  λ A B z c n ⇒
+    case1 n return n' ⇒ 1.(Vec n' A) → B of {
+      zero ⇒
+        λ nil ⇒ case1 nil return B of { 'nil ⇒ z };
+      succ n, 1.ih ⇒
+        λ cons ⇒ case1 cons return B of { (first, rest) ⇒ c first (ih rest) }
     };
 
-{-
--- 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.B → ω.(1.A → 1.B → B) → 1.(List A) → B =
+  λ A B z c xs ⇒
+    case1 xs return B of { (len, elems) ⇒ foldr' A B z c len elems };
 
-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;
+load "nat.quox";
 
--- ...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 sum : 1.(List ℕ) → ℕ = foldr ℕ ℕ 0 plus;
 
-defω plus : 1.ℕ → 1.ℕ → ℕ =
-  λ m n ⇒
-  case1 m return ℕ of {
-    zero         ⇒ n;
-    succ _, 1.mn ⇒ succ mn
-  };
+def numbers : List ℕ = (5, (0, 1, 2, 3, 4, 5, 'nil));
 
--- 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;
--}
+def number-sum : sum numbers ≡ 10 : ℕ = δ _ ⇒ 10;

examples/misc.quox

@@ -35,3 +35,8 @@ defω sym : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) →
            1.(x ≡ y : A) → y ≡ x : A =
   λ A x y eq ⇒ δ i ⇒
     comp [A] @0 @1 (eq @0) @i { 0 j ⇒ eq @j; 1 _ ⇒ eq @0 };
+
+defω trans : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) → 0.(z : A) →
+             ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
+  λ A x y z eq1 eq2 ⇒ δ i ⇒
+    comp [A] @0 @1 (eq1 @i) @i { 0 _ ⇒ eq1 @0; 1 j ⇒ eq2 @j };

examples/nat.quox

@@ -1,4 +1,4 @@
-defω dup-ℕ : 1.ℕ → [ω.ℕ] =
+def dup-ℕ : 1.ℕ → [ω.ℕ] =
   λ n ⇒
   case1 n return [ω.ℕ] of {
     zero ⇒ [zero];
@@ -6,29 +6,33 @@ defω dup-ℕ : 1.ℕ → [ω.ℕ] =
       case1 d return [ω.ℕ] of { [d] ⇒ [succ d] }
   };
 
-defω plus : 1.ℕ → 1.ℕ → ℕ =
+def plus : 1.ℕ → 1.ℕ → ℕ =
   λ m n ⇒
   case1 m return ℕ of {
     zero        ⇒ n;
     succ _, 1.p ⇒ succ p
   };
 
-defω times-ω : 1.ℕ → ω.ℕ → ℕ =
+def times-ω : 1.ℕ → ω.ℕ → ℕ =
   λ m n ⇒
   case1 m return ℕ of {
     zero        ⇒ zero;
     succ _, 1.t ⇒ plus n t
   };
 
-defω times : 1.ℕ → 1.ℕ → ℕ =
+def times : 1.ℕ → 1.ℕ → ℕ =
   λ m n ⇒
   case1 dup-ℕ n return ℕ of {
     [n] ⇒ times-ω m n
   };
 
-defω pred : 1.ℕ → ℕ =
+def pred : 1.ℕ → ℕ =
   λ n ⇒
   case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n };
 
 def0 pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
   λ n ⇒ δ i ⇒ n;
+
+def0 succ-inj : 0.(m : ℕ) → 0.(n : ℕ) →
+                0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ =
+  λ m n eq ⇒ δ i ⇒ pred (eq @i);