example updates

- misc.All doesn't need to be a ★¹
- add pair.map-fst and pair.map-snd
- add bool.dup!
- tweak quantities in eta.from-false
- add fail.quox to all.quox
- add qty.quox

examples/all.quox

@@ -6,3 +6,5 @@ load "nat.quox"
 load "pair.quox"
 load "list.quox"
 load "eta.quox"
+load "fail.quox"
+load "qty.quox"

examples/bool.quox

@@ -18,8 +18,13 @@ def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B =
 
 def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False;
 
-def boolω : Bool → [ω.Bool] =
-  λ b ⇒ if [ω.Bool] b ['true] ['false];
+def dup! : (b : Bool) → [ω. Sing Bool b] =
+  λ b ⇒ if-dep (λ b ⇒ [ω. Sing Bool b]) b
+    [('true,  [δ _ ⇒ 'true])]
+    [('false, [δ _ ⇒ 'false])];
+
+def dup : Bool → [ω. Bool] =
+  λ b ⇒ appω (Sing Bool b) Bool (sing.val Bool b) (dup! b);
 
 def true-not-false : Not ('true ≡ 'false : Bool) =
   λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true;

examples/eta.quox

@@ -18,8 +18,8 @@ def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A
   λ A B P e p ⇒ p
 
 -- not exactly η, but kinda related
-def0 from-false : (A : ★) → (P : (False → A) → ★) → (f : False → A) →
-                  P (λ x ⇒ void A x) → P f =
+def0 from-false : (A : ★) → (P : (0.False → A) → ★) → (f : 0.False → A) →
+                  P (void A) → P f =
   λ A P f p ⇒ p
 
 }

examples/misc.quox

@@ -6,7 +6,7 @@ def0 Not : ★ → ★ = λ A ⇒ ω.A → False
 def void : 0.(A : ★) → 0.False → A =
   λ A v ⇒ case0 v return A of { }
 
-def0 All : (A : ★) → (0.A → ★) → ★¹ =
+def0 All : (A : ★) → (0.A → ★) → ★ =
   λ A P ⇒ (x : A) → P x
 
 def0 cong :

examples/pair.quox

@@ -28,7 +28,7 @@ def curry :
   λ A B C f x y ⇒ f (x, y);
 
 def curry' :
-    0.(A B C : ★) → ((A × B) → C) → A → B → C =
+    0.(A B C : ★) → (A × B → C) → A → B → C =
   λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C);
 
 def0 fst-snd :
@@ -54,13 +54,19 @@ def map :
     0.(A A' : ★) →
     0.(B : A → ★) → 0.(B' : A' → ★) →
     (f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
-    (Σ A B) → Σ A' B' =
+    Σ A B → Σ A' B' =
   λ A A' B B' f g p ⇒
     case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
 
 def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' =
   λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g);
 
+def map-fst : 0.(A A' B : ★) → (A → A') → A × B → A' × B =
+  λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x);
+
+def map-snd : 0.(A B B' : ★) → (B → B') → A × B → A × B' =
+  λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f;
+
 }
 
 def0 Σ   = pair.Σ;

examples/qty.quox

@@ -0,0 +1,73 @@
+def0 Qty : ★ = {"zero", one, any}
+
+def dup : Qty → [ω.Qty] =
+  λ π ⇒ case π return [ω.Qty] of {
+    'zero ⇒ ['zero];
+    'one  ⇒ ['one];
+    'any  ⇒ ['any];
+  }
+
+def drop : 0.(A : ★) → Qty → A → A =
+  λ A π x ⇒ case π return A of {
+    'zero ⇒ x;
+    'one  ⇒ x;
+    'any  ⇒ x;
+  }
+
+def if-zero : 0.(A : ★) → Qty → ω.A → ω.A → A =
+  λ A π z nz ⇒
+  case π return A of { 'zero ⇒ z; 'one ⇒ nz; 'any ⇒ nz }
+
+def plus : Qty → Qty → Qty =
+  λ π ρ ⇒
+  case π return Qty of {
+    'zero ⇒ ρ;
+    'one  ⇒ if-zero Qty ρ 'one 'any;
+    'any  ⇒ drop Qty ρ 'any;
+  }
+
+def times : Qty → Qty → Qty =
+  λ π ρ ⇒
+  case π return Qty of {
+    'zero ⇒ drop Qty ρ 'zero;
+    'one  ⇒ ρ;
+    'any  ⇒ if-zero Qty ρ 'zero 'any;
+  }
+
+def0 FUN : Qty → (A : ★) → (A → ★) → ★ =
+  λ π A B ⇒
+  case π return ★ of {
+    'zero ⇒ 0.(x : A) → B x;
+    'one  ⇒ 1.(x : A) → B x;
+    'any  ⇒ ω.(x : A) → B x;
+  }
+
+def0 Fun : Qty → ★ → ★ → ★ =
+  λ π A B ⇒ FUN π A (λ _ ⇒ B)
+
+def0 Box : Qty → ★ → ★ =
+  λ π A ⇒
+  case π return ★ of {
+    'zero ⇒ [0.A];
+    'one  ⇒ [1.A];
+    'any  ⇒ [ω.A];
+  }
+
+def0 unbox : (π : Qty) → (A : ★) → Box π A → A =
+  λ π A ⇒
+  case π return π' ⇒ Box π' A → A of {
+    'zero ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+    'one  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+    'any  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
+  }
+
+def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
+            FUN π A B → (x : Box π A) → B (unbox π A x) =
+  λ π A B ⇒
+  case π
+  return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x)
+  of {
+    'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'zero A x') of { [x] ⇒ f x };
+    'one  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'one  A x') of { [x] ⇒ f x };
+    'any  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'any  A x') of { [x] ⇒ f x };
+  }