From 7bd959e919c0c92df2cfb70bfe6c277cb60836ce Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 17 Sep 2023 14:41:29 +0200
Subject: [PATCH] some example stuff

---
 examples/misc.quox |  3 +++
 examples/pair.quox | 25 ++++++++++++++++++-------
 2 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/examples/misc.quox b/examples/misc.quox
index bbad8e6..defcffd 100644
--- a/examples/misc.quox
+++ b/examples/misc.quox
@@ -44,6 +44,9 @@ def appω : 0.(A B : ★) → ω.(f : A → B) → [ω.A] → [ω.B] =
   λ A B f x ⇒
   case x return [ω.B] of { [x'] ⇒ [f x'] }
 
+def0 HEq : (A B : ★) → A → B → ★¹ =
+  λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y
+
 
 def0 Sing : (A : ★) → A → ★ =
   λ A x ⇒ (val : A) × [0. val ≡ x : A]
diff --git a/examples/pair.quox b/examples/pair.quox
index d37680b..c1527c5 100644
--- a/examples/pair.quox
+++ b/examples/pair.quox
@@ -1,15 +1,15 @@
 namespace pair {
 
-def0 Σ : (A : ★) → (0.A → ★) → ★ = λ A B ⇒ (x : A) × B x;
+def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x;
 
-def fst : 0.(A : ★) → 0.(B : 0.A → ★) → ω.(Σ A B) → A =
+def fst : 0.(A : ★) → 0.(B : 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) =
+def snd : 0.(A : ★) → 0.(B : 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) → ★) →
+    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 A B p) (snd A B p) =
   λ A B C f p ⇒
@@ -20,7 +20,7 @@ def uncurry' :
   λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C);
 
 def curry :
-    0.(A : ★) → 0.(B : 0.A → ★) → 0.(C : 0.(Σ A B) → ★) →
+    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);
 
@@ -29,16 +29,27 @@ def curry' :
   λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C);
 
 def0 fst-snd :
-    (A : ★) → (B : 0.A → ★) →
+    (A : ★) → (B : A → ★) →
     (p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B =
   λ A B p ⇒
     case p
     return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B
     of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) };
 
+def0 fst-eq :
+    (A : ★) → (B : A → ★) →
+    (p q : Σ A B) → p ≡ q : Σ A B → fst A B p ≡ fst A B q : A =
+  λ A B p q eq ⇒ δ 𝑖 ⇒ fst A B (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 A B p) (snd A B q) =
+  λ A B p q eq ⇒ δ 𝑖 ⇒ snd A B (eq @𝑖);
+
 def map :
     0.(A A' : ★) →
-    0.(B : 0.A → ★) → 0.(B' : 0.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 ⇒