add η for pairs in zero contexts

examples/eta.quox

@@ -3,6 +3,7 @@ load "misc.quox"
 namespace eta {
 
 def0 Π : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) → B x
+def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x
 
 def0 function : (A : ★) → (B : A → Type) → (P : Π A B → ★) → (f : Π A B) →
                 P (λ x ⇒ f x) → P f =
@@ -12,6 +13,10 @@ def0 box : (A : ★) → (P : [ω.A] → ★) → (e : [ω.A]) →
            P [case1 e return A of {[x] ⇒ x}] → P e =
   λ A P e p ⇒ p
 
+def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A B) →
+            P (fst e, snd e) → P e =
+  λ 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 =

examples/pair.quox

@@ -2,18 +2,21 @@ namespace pair {
 
 def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x;
 
+{-
+-- now builtins
 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 : 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 : 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) =
+    (p : Σ A B) → C (fst p) (snd p) =
   λ A B C f p ⇒
-    case p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y };
+    case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y };
 
 def uncurry' :
     0.(A B C : ★) → (A → B → C) → (A × B) → C =
@@ -30,22 +33,22 @@ def curry' :
 
 def0 fst-snd :
     (A : ★) → (B : A → ★) →
-    (p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B =
+    (p : Σ A B) → p ≡ (fst p, snd p) : Σ A B =
   λ A B p ⇒
     case p
-    return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B
+    return p' ⇒ p' ≡ (fst p', snd 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 =
+    (p q : Σ A B) → p ≡ q : Σ A B → fst p ≡ fst q : A =
-  λ A B p q eq ⇒ δ 𝑖 ⇒ fst A B (eq @𝑖);
+  λ A B p q eq ⇒ δ 𝑖 ⇒ fst (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) =
+    Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd p) (snd q) =
-  λ A B p q eq ⇒ δ 𝑖 ⇒ snd A B (eq @𝑖);
+  λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖);
 
 def map :
     0.(A A' : ★) →
@@ -61,5 +64,5 @@ def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A'
 }
 
 def0 Σ   = pair.Σ;
-def  fst = pair.fst;
+-- def  fst = pair.fst;
-def  snd = pair.snd;
+-- def  snd = pair.snd;

lib/Quox/Equal.idr

@@ -233,12 +233,20 @@ namespace Term
 
       (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
 
-      (Pair {}, E _)     => clashT s.loc ctx ty s t
+      (E e,            Pair fst snd _) => eta s.loc e fst snd
-      (E _,     Pair {}) => clashT s.loc ctx ty s t
+      (Pair fst snd _, E f)            => eta s.loc f fst snd
 
       (Pair {}, t) => wrongType t.loc ctx ty t
       (E _,     t) => wrongType t.loc ctx ty t
       (s,       _) => wrongType s.loc ctx ty s
+  where
+    eta : Loc -> Elim 0 n -> Term 0 n -> Term 0 n -> Eff EqualInner ()
+    eta loc e s t =
+      case sg of
+        SZero => do
+          compare0 defs ctx sg fst                          (E $ Fst e e.loc) s
+          compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
+        SOne => clashT loc ctx ty s t
 
   compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
     case (s, t) of