From cf9bfc21592f230a14355fcf622f30699db9dde7 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 22 Jul 2023 21:26:20 +0200
Subject: [PATCH] example stuff

---
 examples/list.quox | 29 ++++++++++++++++++++++++++---
 examples/misc.quox | 29 +++++++++++++++++++++++++++++
 examples/nat.quox  | 13 +++++++++----
 3 files changed, 64 insertions(+), 7 deletions(-)

diff --git a/examples/list.quox b/examples/list.quox
index 970676e..cb6ac1e 100644
--- a/examples/list.quox
+++ b/examples/list.quox
@@ -24,6 +24,17 @@ def elim : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
         }
     };
 
+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)
+        }
+    }
+
 }
 
 def0 Vec = vec.Vec;
@@ -51,15 +62,27 @@ def elim : 0.(A : ★) → 0.(P : List A → ★) →
         len elems
     };
 
+-- [fixme] List A <: List¹ A should be automatic, imo
+def up : 0.(A : ★) → List A → List¹ A =
+  λ A xs ⇒
+  case xs return List¹ A of { (len, elems) ⇒
+    case nat.dup! len return List¹ A of { [p] ⇒
+      caseω p return List¹ A of { (lenω, eq0) ⇒
+        case eq0 return List¹ A of { [eq] ⇒
+          (lenω, vec.up A lenω (coe (𝑖 ⇒ Vec (eq @𝑖) A) @1 @0 elems))
+        }
+      }
+    }
+  };
+
 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 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);
 
--- [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 All : (A : ★) → (P : A → ★) → List A → ★ =
+  λ A P xs ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps) (up A xs);
 
 }
 
diff --git a/examples/misc.quox b/examples/misc.quox
index 6766739..8188a1d 100644
--- a/examples/misc.quox
+++ b/examples/misc.quox
@@ -32,3 +32,32 @@ def trans : 0.(A : ★) → 0.(x y z : A) →
             ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
   λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒
     comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }
+
+def appω : 0.(A B : ★) → ω.(f : A → B) → [ω.A] → [ω.B] =
+  λ A B f x ⇒
+  case x return [ω.B] of { [x'] ⇒ [f x'] };
+
+
+def0 Sing : (A : ★) → A → ★ =
+  λ A x ⇒ (val : A) × [0. val ≡ x : A];
+
+namespace sing {
+
+def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
+  λ A _ sg ⇒
+  case sg return A of { (x, eq) ⇒ case eq return A of { [_] ⇒ x } };
+
+def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
+  λ A x sg ⇒
+  case sg return sg' ⇒ val A x sg' ≡ x : A of { (x', eq) ⇒
+    case eq return eq' ⇒ val A x (x', eq') ≡ x : A of { [eq'] ⇒ eq' }
+  };
+
+def app : 0.(A B : ★) → 0.(x : A) →
+          (f : A → B) → Sing A x → Sing B (f x) =
+  λ A B x f sg ⇒
+  case sg return Sing B (f x) of { (x_, eq) ⇒
+    case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) }
+  };
+
+}
diff --git a/examples/nat.quox b/examples/nat.quox
index d0c0855..17715d4 100644
--- a/examples/nat.quox
+++ b/examples/nat.quox
@@ -4,13 +4,18 @@ load "either.quox";
 
 namespace nat {
 
-def dup : ℕ → [ω.ℕ] =
+def dup! : (n : ℕ) → [ω. Sing ℕ n] =
   λ n ⇒
-  case n return [ω.ℕ] of {
-    zero        ⇒ [zero];
-    succ _, 1.d ⇒ case d return [ω.ℕ] of { [d] ⇒ [succ d] }
+  case n return n' ⇒ [ω. Sing ℕ n'] of {
+    zero ⇒ [(zero, [δ _ ⇒ zero])];
+    succ n, 1.d ⇒
+      appω (Sing ℕ n) (Sing ℕ (succ n))
+        (sing.app ℕ ℕ n (λ n ⇒ succ n)) d
   };
 
+def dup : ℕ → [ω.ℕ] =
+  λ n ⇒ appω (Sing ℕ n) ℕ (sing.val ℕ n) (dup! n);
+
 def plus : ℕ → ℕ → ℕ =
   λ m n ⇒
   case m return ℕ of {