examples

examples/bool.quox

@@ -0,0 +1,29 @@
+load "misc.quox";
+
+namespace bool {
+
+def0 Bool : ★₀ = {true, false};
+
+def boolω : 1.Bool → [ω.Bool] =
+  λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };
+
+def if : 0.(A : ★₀) → 1.Bool → ω.A → ω.A → A =
+  λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };
+
+-- [todo]: universe lifting
+def0 If : 1.Bool → 0.★₀ → 0.★₀ → ★₀ =
+  λ b T F ⇒ case1 b return ★₀ of { 'true ⇒ T; 'false ⇒ F };
+
+def0 T : ω.Bool → ★₀ = λ b ⇒ If b True False;
+
+def true-not-false : Not ('true ≡ 'false : Bool) =
+  λ eq ⇒ coe [i ⇒ T (eq @i)] @0 @1 '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;
+
+}
+
+def0 Bool = bool.Bool;

examples/either.quox

@@ -1,32 +1,76 @@
+load "misc.quox";
+load "bool.quox";
+
+namespace either {
+
 def0 Tag : ★₀ = {left, right};
 
-def0 Payload : 0.(A : ★₀) → 0(B : .★₀) → 1.Tag → ★₀ =
+def0 Payload : 0.(A : ★₀) → 0.(B : ★₀) → 1.Tag → ★₀ =
   λ A B tag ⇒ case1 tag return ★₀ of { 'left ⇒ A; 'right ⇒ B };
 
 def0 Either : 0.★₀ → 0.★₀ → ★₀ =
   λ A B ⇒ (tag : Tag) × Payload A B tag;
 
-defω Left : 0.(A : ★₀) → 0.(B : ★₀) → 1.A → Either A B =
+def Left : 0.(A : ★₀) → 0.(B : ★₀) → 1.A → Either A B =
   λ A B x ⇒ ('left, x);
 
-defω Right : 0.(A : ★₀) → 0.(B : ★₀) → 1.B → Either A B =
+def Right : 0.(A : ★₀) → 0.(B : ★₀) → 1.B → Either A B =
   λ A B x ⇒ ('right, x);
 
-defω either-elim :
+def elim' :
+    0.(A : ★₀) → 0.(B : ★₀) →
+    0.(P : 0.(Either A B) → ★₀) →
+    ω.(1.(x : A) → P (Left  A B x)) →
+    ω.(1.(x : B) → P (Right A B x)) →
+    1.(t : Tag) → 1.(a : Payload A B t) → P (t, a) =
+  λ A B P f g t ⇒
+    case1 t
+    return t' ⇒ 1.(a : Payload A B t') → P (t', a)
+    of { 'left ⇒ f; 'right ⇒ g };
+
+def elim :
     0.(A : ★₀) → 0.(B : ★₀) →
     0.(P : 0.(Either A B) → ★₀) →
     ω.(1.(x : A) → P (Left  A B x)) →
     ω.(1.(x : B) → P (Right A B x)) →
     1.(x : Either A B) → P x =
-  λ A B P f g x ⇒
-    case1 x return x' ⇒ P x' of {
-      (tag, value) ⇒
-        (case1 tag
-         return tag' ⇒
-           0.(eq : (tag ≡ tag' : Tag)) →
-           P (tag, coerce [i ⇒ Payload A B (eq i)] @0 @1 value)
-         of {
-           'left  ⇒ λ eq ⇒ f value;
-           'right ⇒ λ eq ⇒ g value
-         }) (δ _ ⇒ tag)
-    };
+  λ A B P f g e ⇒
+    case1 e return e' ⇒ P e' of { (t, a) ⇒ elim' A B P f g t a };
+
+
+}
+
+def0 Either = either.Either;
+def  Left   = either.Left;
+def  Right  = either.Right;
+
+
+namespace dec {
+
+def0 Dec : 0.★₀ → ★₀ = λ 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];
+
+def0 DecEq : 0.★₀ → ★₀ =
+  λ A ⇒ ω.(x : A) → ω.(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)) →
+    1.(x : Dec A) → P x =
+  λ A P f g ⇒
+    either.elim [0.A] [0.Not A] P
+      (λ y ⇒ case0 y return y' ⇒ P (Left  [0.A] [0.Not A] y') of {[y'] ⇒ f y'})
+      (λ n ⇒ case0 n return n' ⇒ P (Right [0.A] [0.Not A] n') of {[n'] ⇒ g n'});
+
+def bool : 0.(A : ★₀) → 1.(Dec A) → Bool =
+  λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false);
+
+}
+
+def0 Dec   = dec.Dec;
+def0 DecEq = dec.DecEq;
+def  Yes   = dec.Yes;
+def  No    = dec.No;

examples/list.quox

@@ -1,3 +1,7 @@
+load "nat.quox";
+
+namespace list {
+
 def0 Vec : 0.ℕ → 0.★₀ → ★₀ =
   λ n A ⇒
   caseω n return ★₀ of {
@@ -29,10 +33,10 @@ def foldr : 0.(A : ★₀) → 0.(B : ★₀) →
   λ A B z c xs ⇒
     case1 xs return B of { (len, elems) ⇒ foldr' A B z c len elems };
 
-load "nat.quox";
+def sum : 1.(List ℕ) → ℕ = foldr ℕ ℕ 0 nat.plus;
 
-def sum : 1.(List ℕ) → ℕ = foldr ℕ ℕ 0 plus;
-
-def numbers : List ℕ = (5, (0, 1, 2, 3, 4, 5, 'nil));
+def numbers : List ℕ = (5, (0, 1, 2, 3, 4, 'nil));
 
 def number-sum : sum numbers ≡ 10 : ℕ = δ _ ⇒ 10;
+
+}

examples/misc.quox

@@ -1,14 +1,22 @@
+def0 True : ★₀ = {true};
+
+def0 False : ★₀ = {};
+def0 Not : 0.★₀ → ★₀ = λ A ⇒ ω.A → False;
+
+def void : 0.(A : ★₀) → 0.False → A =
+  λ A v ⇒ case0 v return A of { };
+
 def0 Pred : 0.★₀ → ★₁ = λ A ⇒ 0.A → ★₀;
 
 def0 All : 0.(A : ★₀) → 0.(Pred A) → ★₁ =
   λ A P ⇒ 1.(x : A) → P x;
 
-defω cong :
+def cong :
     0.(A : ★₀) → 0.(P : Pred A) →
     1.(p : All A P) →
     0.(x : A) → 0.(y : A) → 1.(xy : x ≡ y : A) →
-    Eq [i ⇒ P (xy @i)] (p x) (p y) =
-  λ A P p x y xy ⇒ δ i ⇒ p (xy @i);
+    Eq [𝑖 ⇒ P (xy @𝑖)] (p x) (p y) =
+  λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖);
 
 def0 eq-f :
     0.(A : ★₀) → 0.(P : Pred A) →
@@ -16,27 +24,18 @@ def0 eq-f :
     0.A → ★₀ =
   λ A P p q x ⇒ p x ≡ q x : P x;
 
-defω funext :
+def funext :
     0.(A : ★₀) → 0.(P : Pred A) →
     0.(p : All A P) → 0.(q : All A P) →
     1.(All A (eq-f A P p q)) →
     p ≡ q : All A P =
-  λ A P p q eq ⇒ δ i ⇒ λ x ⇒ eq x @i;
+  λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖;
 
-def0 T : ω.{true, false} → ★₀ =
-  λ b ⇒ caseω b return ★₀ of { 'true ⇒ {tt}; 'false ⇒ {} };
+def sym : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) →
+          1.(x ≡ y : A) → y ≡ x : A =
+  λ A x y eq ⇒ δ 𝑖 ⇒ comp [A] @0 @1 (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 };
 
-defω absurd :
-    0.('true ≡ 'false : {true, false}) → 0.(A : ★₀) → A =
-  λ eq A ⇒
-    case0 coe [i ⇒ T (eq @i)] @0 @1 'tt return A of { };
-
-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 };
+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 ⇒ δ 𝑖 ⇒
+    comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 };

examples/nat.quox

@@ -1,9 +1,14 @@
-def dup-ℕ : 1.ℕ → [ω.ℕ] =
+load "misc.quox";
+load "bool.quox";
+load "either.quox";
+
+namespace nat {
+
+def dup : 1.ℕ → [ω.ℕ] =
   λ n ⇒
   case1 n return [ω.ℕ] of {
-    zero ⇒ [zero];
-    succ _, 1.d ⇒
-      case1 d return [ω.ℕ] of { [d] ⇒ [succ d] }
+    zero        ⇒ [zero];
+    succ _, 1.d ⇒ case1 d return [ω.ℕ] of { [d] ⇒ [succ d] }
   };
 
 def plus : 1.ℕ → 1.ℕ → ℕ =
@@ -13,7 +18,7 @@ def plus : 1.ℕ → 1.ℕ → ℕ =
     succ _, 1.p ⇒ succ p
   };
 
-def times-ω : 1.ℕ → ω.ℕ → ℕ =
+def timesω : 1.ℕ → ω.ℕ → ℕ =
   λ m n ⇒
   case1 m return ℕ of {
     zero        ⇒ zero;
@@ -21,18 +26,89 @@ def times-ω : 1.ℕ → ω.ℕ → ℕ =
   };
 
 def times : 1.ℕ → 1.ℕ → ℕ =
-  λ m n ⇒
-  case1 dup-ℕ n return ℕ of {
-    [n] ⇒ times-ω m n
-  };
+  λ m n ⇒ case1 dup n return ℕ of { [n] ⇒ timesω m n };
 
-def pred : 1.ℕ → ℕ =
-  λ n ⇒
-  case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n };
+def pred : 1.ℕ → ℕ = λ n ⇒ case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n };
 
-def0 pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
-  λ n ⇒ δ i ⇒ n;
+def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
+  λ n ⇒ δ 𝑖 ⇒ n;
 
 def0 succ-inj : 0.(m : ℕ) → 0.(n : ℕ) →
                 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ =
-  λ m n eq ⇒ δ i ⇒ pred (eq @i);
+  λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖);
+
+
+def0 IsSucc : 0.ℕ → ★₀ =
+  λ n ⇒ caseω n return ★₀ of { zero ⇒ False; succ _ ⇒ True };
+
+def isSucc? : ω.(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 @𝑖)] @0 @1 'true;
+
+
+def0 not-succ-self : 0.(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)
+  }
+
+
+def eq? : DecEq ℕ =
+  λ m ⇒
+  caseω m
+  return m' ⇒ ω.(n : ℕ) → Dec (m' ≡ n : ℕ)
+  of {
+    zero ⇒ λ n ⇒
+      caseω n return n' ⇒ Dec (zero ≡ n' : ℕ) of {
+        zero    ⇒ Yes (zero ≡ zero    : ℕ) (δ _ ⇒ zero);
+        succ n' ⇒ No  (zero ≡ succ n' : ℕ) (λ eq ⇒ zero-not-succ n' eq)
+      };
+    succ m', ω.ih ⇒ λ n ⇒
+      caseω n return n' ⇒ Dec (succ m' ≡ n' : ℕ) of {
+        zero    ⇒ No (succ m' ≡ zero : ℕ) (λ eq ⇒ succ-not-zero m' eq);
+        succ n' ⇒
+          dec.elim (m' ≡ n' : ℕ) (λ _ ⇒ Dec (succ m' ≡ succ n' : ℕ))
+            (λ y ⇒ Yes (succ m' ≡ succ n' : ℕ) (δ 𝑖 ⇒ succ (y @𝑖)))
+            (λ n ⇒ No  (succ m' ≡ succ n' : ℕ) (λ eq ⇒ n (succ-inj m' n' eq)))
+            (ih n')
+      }
+  };
+
+def eqb : 1.ℕ → 1.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq? m n);
+
+
+def0 plus-zero : 0.(m : ℕ) → m ≡ plus m 0 : ℕ =
+  λ m ⇒
+  caseω m return m' ⇒ m' ≡ plus m' 0 : ℕ of {
+    zero         ⇒ δ _ ⇒ zero;
+    succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
+  };
+
+def0 plus-succ : 0.(m : ℕ) → 0.(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 plus-comm : 0.(m : ℕ) → 0.(n : ℕ) → plus m n ≡ plus n m : ℕ =
+  λ m n ⇒
+  caseω m return m' ⇒ plus m' n ≡ plus n m' : ℕ of {
+    zero ⇒ plus-zero n;
+    succ m', ω.ih ⇒
+      trans ℕ (succ (plus m' n)) (succ (plus n m')) (plus n (succ m'))
+        (δ 𝑖 ⇒ succ (ih @𝑖))
+        (plus-succ n m')
+  };
+
+}

examples/pair.quox

@@ -0,0 +1,52 @@
+namespace pair {
+
+def0 Σ : 0.(A : ★₀) → 0.(0.A → ★₀) → ★₀ = λ A B ⇒ (x : A) × B x;
+
+def fst : 0.(A : ★₀) → 0.(B : 0.A → ★₀) →
+          ω.(Σ A B) → A =
+  λ A B p ⇒ caseω p return A of { (x, _) ⇒ x };
+
+def snd : 0.(A : ★₀) → 0.(B : 0.A → ★₀) →
+          ω.(p : Σ A B) → B (fst A B p) =
+  λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y };
+
+def uncurry :
+    0.(A : ★₀) → 0.(B : 0.A → ★₀) → 0.(C : 0.(x : A) → 0.(B x) → ★₀) →
+    1.(f : 1.(x : A) → 1.(y : B x) → C x y) →
+    1.(p : Σ A B) → C (fst A B p) (snd A B p) =
+  λ A B C f p ⇒
+    case1 p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y };
+
+def curry :
+    0.(A : ★₀) → 0.(B : 0.A → ★₀) → 0.(C : 0.(Σ A B) → ★₀) →
+    1.(f : 1.(p : Σ A B) → C p) → 1.(x : A) → 1.(y : B x) → C (x, y) =
+  λ A B C f x y ⇒ f (x, y);
+
+def0 fst-snd :
+    0.(A : ★₀) → 0.(B : 0.A → ★₀) →
+    1.(p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B =
+  λ A B p ⇒
+    case1 p
+    return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B
+    of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) };
+
+def map :
+    0.(A : ★₀) → 0.(A' : ★₀) →
+    0.(B : 0.A → ★₀) → 0.(B' : 0.A' → ★₀) →
+    1.(f : 1.A → A') → 1.(g : 0.(x : A) → 1.(B x) → B' (f x)) →
+    1.(Σ A B) → Σ A' B' =
+  λ A A' B B' f g p ⇒
+    case1 p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
+
+def map' :
+    0.(A : ★₀) → 0.(A' : ★₀) →
+    0.(B : ★₀) → 0.(B' : ★₀) →
+    1.(f : 1.A → A') → 1.(g : 1.B → B') →
+    1.(A × B) → A' × B' =
+  λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g);
+
+}
+
+def0 Σ   = pair.Σ;
+def  fst = pair.fst;
+def  snd = pair.snd;