From bb8d2464af1f709ab36e72c118e63f8a8276b122 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 18 Sep 2023 21:52:51 +0200
Subject: [PATCH] add fst and snd

---
 lib/Quox/Displace.idr             |   2 +
 lib/Quox/Equal.idr                |  21 +++++
 lib/Quox/FreeVars.idr             |   4 +
 lib/Quox/Parser/FromParser.idr    |   6 ++
 lib/Quox/Parser/Lexer.idr         |   1 +
 lib/Quox/Parser/Parser.idr        |  19 +++-
 lib/Quox/Parser/Syntax.idr        |   3 +
 lib/Quox/Pretty.idr               |   4 +-
 lib/Quox/Syntax/Term/Base.idr     |  10 +++
 lib/Quox/Syntax/Term/Pretty.idr   |  10 +++
 lib/Quox/Syntax/Term/Subst.idr    |   4 +
 lib/Quox/Syntax/Term/Tighten.idr  |   8 ++
 lib/Quox/Typechecker.idr          |  20 +++++
 lib/Quox/Whnf/Coercion.idr        |  82 ++++++++++++-----
 lib/Quox/Whnf/ComputeElimType.idr |  12 ++-
 lib/Quox/Whnf/Interface.idr       |  94 ++++++++++----------
 lib/Quox/Whnf/Main.idr            | 143 +++++++++++++++++++-----------
 17 files changed, 319 insertions(+), 124 deletions(-)

diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr
index 1945936..8b8c07c 100644
--- a/lib/Quox/Displace.idr
+++ b/lib/Quox/Displace.idr
@@ -49,6 +49,8 @@ parameters (k : Universe)
     doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
     doDisplace (CasePair qty pair ret body loc) =
       CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
+    doDisplace (Fst pair loc) = Fst (doDisplace pair) loc
+    doDisplace (Snd pair loc) = Snd (doDisplace pair) loc
     doDisplace (CaseEnum qty tag ret arms loc) =
       CaseEnum qty (doDisplace tag) (doDisplaceS ret)
                (assert_total $ map doDisplace arms) loc
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 6dddc39..95d6d9c 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -544,6 +544,27 @@ namespace Elim
   compare0Inner' defs ctx sg e'@(CasePair {}) f' ne nf =
     clashE defs ctx sg e' f'
 
+  --  Ψ | Γ ⊢ e = f ⇒ (x : A) × B
+  -- ------------------------------
+  --  Ψ | Γ ⊢ fst e = fst f ⇒ A
+  compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf =
+    local_ Equal $ do
+      ety <- compare0Inner defs ctx sg e f
+      fst <$> expectSig defs ctx sg eloc ety
+  compare0Inner' defs ctx sg e@(Fst {}) f _ _ =
+    clashE defs ctx sg e f
+
+  --  Ψ | Γ ⊢ e = f ⇒ (x : A) × B
+  -- ------------------------------------
+  --  Ψ | Γ ⊢ snd e = snd f ⇒ B[fst e/x]
+  compare0Inner' defs ctx sg (Snd e eloc) (Snd f floc) ne nf =
+    local_ Equal $ do
+      ety <- compare0Inner defs ctx sg e f
+      (_, tsnd) <- expectSig defs ctx sg eloc ety
+      pure $ sub1 tsnd (Fst e eloc)
+  compare0Inner' defs ctx sg e@(Snd {}) f _ _ =
+    clashE defs ctx sg e f
+
   --  Ψ | Γ ⊢ e = f ⇒ {𝐚s}
   --  Ψ | Γ, x : {𝐚s} ⊢ Q = R
   --  Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr
index 6bde3f6..e4031b9 100644
--- a/lib/Quox/FreeVars.idr
+++ b/lib/Quox/FreeVars.idr
@@ -196,6 +196,8 @@ HasFreeVars (Elim d) where
   fv (B i _) = only i
   fv (App {fun, arg, _}) = fv fun <+> fv arg
   fv (CasePair {pair, ret, body, _}) = fv pair <+> fv ret <+> fv body
+  fv (Fst pair _) = fv pair
+  fv (Snd pair _) = fv pair
   fv (CaseEnum {tag, ret, arms, _}) =
     fv tag <+> fv ret <+> foldMap fv (values arms)
   fv (CaseNat {nat, ret, zero, succ, _}) =
@@ -269,6 +271,8 @@ HasFreeDVars Elim where
   fdv (B {}) = none
   fdv (App {fun, arg, _}) = fdv fun <+> fdv arg
   fdv (CasePair {pair, ret, body, _}) = fdv pair <+> fdvT ret <+> fdvT body
+  fdv (Fst pair _) = fdv pair
+  fdv (Snd pair _) = fdv pair
   fdv (CaseEnum {tag, ret, arms, _}) =
     fdv tag <+> fdvT ret <+> foldMap fdv (values arms)
   fdv (CaseNat {nat, ret, zero, succ, _}) =
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 1f05ab9..63f8055 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -141,6 +141,12 @@ mutual
         <*> fromPTermTScope ds ns [< x, y] body
         <*> pure loc
 
+    Fst pair loc =>
+      map E $ Fst <$> fromPTermElim ds ns pair <*> pure loc
+
+    Snd pair loc =>
+      map E $ Snd <$> fromPTermElim ds ns pair <*> pure loc
+
     Case pi tag (r, ret) (CaseEnum arms _) loc =>
       map E $ CaseEnum (fromPQty pi)
         <$> fromPTermElim ds ns tag
diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr
index a6b1fee..d4359d4 100644
--- a/lib/Quox/Parser/Lexer.idr
+++ b/lib/Quox/Parser/Lexer.idr
@@ -203,6 +203,7 @@ reserved =
    Word "caseω" `Or` Word "case#",
    Word1 "return",
    Word1 "of",
+   Word1 "fst", Word1 "snd",
    Word1 "_",
    Word1 "Eq",
    Word "λ" `Or` Word "fun",
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index 549d09d..ba90021 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -372,10 +372,23 @@ eqTerm : FileName -> Grammar True PTerm
 eqTerm fname = withLoc fname $
   resC "Eq" *> mustWork [|Eq (typeLine fname) (termArg fname) (termArg fname)|]
 
+export
+resAppTerm : FileName -> (word : String) -> (0 _ : IsReserved word) =>
+             (PTerm -> Loc -> PTerm) -> Grammar True PTerm
+resAppTerm fname word f = withLoc fname $
+  resC word *> mustWork [|f (termArg fname)|]
+
 export
 succTerm : FileName -> Grammar True PTerm
-succTerm fname = withLoc fname $
-  resC "succ" *> mustWork [|Succ (termArg fname)|]
+succTerm fname = resAppTerm fname "succ" Succ
+
+export
+fstTerm : FileName -> Grammar True PTerm
+fstTerm fname = resAppTerm fname "fst" Fst
+
+export
+sndTerm : FileName -> Grammar True PTerm
+sndTerm fname = resAppTerm fname "snd" Snd
 
 ||| a dimension argument with an `@` prefix, or
 ||| a term argument with no prefix
@@ -403,6 +416,8 @@ appTerm fname =
   <|> splitUniverseTerm fname
   <|> eqTerm fname
   <|> succTerm fname
+  <|> fstTerm fname
+  <|> sndTerm fname
   <|> normalAppTerm fname
 
 export
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index 335eb49..b95e351 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -73,6 +73,7 @@ namespace PTerm
       | Sig PatVar PTerm PTerm Loc
       | Pair PTerm PTerm Loc
       | Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
+      | Fst PTerm Loc | Snd PTerm Loc
 
       | Enum (List TagVal) Loc
       | Tag TagVal Loc
@@ -113,6 +114,8 @@ Located PTerm where
   (App  _ _           loc).loc = loc
   (Sig  _ _ _         loc).loc = loc
   (Pair _ _           loc).loc = loc
+  (Fst  _             loc).loc = loc
+  (Snd  _             loc).loc = loc
   (Case _ _ _ _       loc).loc = loc
   (Enum _             loc).loc = loc
   (Tag  _             loc).loc = loc
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 1da3743..7d8c80c 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -234,7 +234,7 @@ prettyDBind = hl DVar . prettyBind'
 export %inline
 typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
 eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
-ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
+ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD :
   {opts : LayoutOpts} -> Eff Pretty (Doc opts)
 typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
 arrowD    = hl Delim  . text =<< ifUnicode "→" "->"
@@ -261,6 +261,8 @@ compD     = hl Syntax $ text "comp"
 undD      = hl Syntax $ text "_"
 cstD      = hl Syntax $ text "="
 pipeD     = hl Syntax $ text "|"
+fstD      = hl Syntax $ text "fst"
+sndD      = hl Syntax $ text "snd"
 
 
 export
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 1023dfd..7778b9f 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -155,6 +155,12 @@ mutual
                (loc : Loc) ->
                Elim d n
 
+    ||| first element of a pair. only works in non-linear contexts.
+    Fst : (pair : Elim d n) -> (loc : Loc) -> Elim d n
+
+    ||| second element of a pair. only works in non-linear contexts.
+    Snd : (pair : Elim d n) -> (loc : Loc) -> Elim d n
+
     ||| enum matching
     CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
                (ret : ScopeTerm d n) ->
@@ -369,6 +375,8 @@ Located (Elim d n) where
   (B _ loc).loc                 = loc
   (App _ _ loc).loc             = loc
   (CasePair _ _ _ _ loc).loc    = loc
+  (Fst _ loc).loc               = loc
+  (Snd _ loc).loc               = loc
   (CaseEnum _ _ _ _ loc).loc    = loc
   (CaseNat _ _ _ _ _ _ loc).loc = loc
   (CaseBox _ _ _ _ loc).loc     = loc
@@ -417,6 +425,8 @@ Relocatable (Elim d n) where
   setLoc loc (App fun arg _) = App fun arg loc
   setLoc loc (CasePair qty pair ret body _) =
     CasePair qty pair ret body loc
+  setLoc loc (Fst pair _) = Fst pair loc
+  setLoc loc (Snd pair _) = Fst pair loc
   setLoc loc (CaseEnum qty tag ret arms _) =
     CaseEnum qty tag ret arms loc
   setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index ab40679..29db4b6 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -493,6 +493,16 @@ prettyElim dnames tnames (CasePair qty pair ret body _) = do
   prettyCase dnames tnames qty pair ret
     [MkCaseArm pat [<] [< x, y] body.term]
 
+prettyElim dnames tnames (Fst pair _) =
+  parensIfM App =<< do
+    pair <- prettyTArg dnames tnames (E pair)
+    prettyAppD !fstD [pair]
+
+prettyElim dnames tnames (Snd pair _) =
+  parensIfM App =<< do
+    pair <- prettyTArg dnames tnames (E pair)
+    prettyAppD !sndD [pair]
+
 prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
   arms <- for (SortedMap.toList arms) $ \(tag, body) =>
     pure $ MkCaseArm !(prettyTag tag) [<] [<] body
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 60f1a11..00814d8 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -299,6 +299,10 @@ mutual
       nclo $ App (f // th // ph) (s // th // ph) loc
     pushSubstsWith th ph (CasePair pi p r b loc) =
       nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
+    pushSubstsWith th ph (Fst pair loc) =
+      nclo $ Fst (pair // th // ph) loc
+    pushSubstsWith th ph (Snd pair loc) =
+      nclo $ Snd (pair // th // ph) loc
     pushSubstsWith th ph (CaseEnum pi t r arms loc) =
       nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
                (map (\b => b // th // ph) arms) loc
diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr
index 4a18c54..0f5a312 100644
--- a/lib/Quox/Syntax/Term/Tighten.idr
+++ b/lib/Quox/Syntax/Term/Tighten.idr
@@ -87,6 +87,10 @@ mutual
                  <*> tightenS p ret
                  <*> tightenS p body
                  <*> pure loc
+  tightenE' p (Fst pair loc) =
+    Fst <$> tightenE p pair <*> pure loc
+  tightenE' p (Snd pair loc) =
+    Snd <$> tightenE p pair <*> pure loc
   tightenE' p (CaseEnum qty tag ret arms loc) =
     CaseEnum qty <$> tightenE p tag
                  <*> tightenS p ret
@@ -202,6 +206,10 @@ mutual
                  <*> dtightenS p ret
                  <*> dtightenS p body
                  <*> pure loc
+  dtightenE' p (Fst pair loc) =
+    Fst <$> dtightenE p pair <*> pure loc
+  dtightenE' p (Snd pair loc) =
+    Snd <$> dtightenE p pair <*> pure loc
   dtightenE' p (CaseEnum qty tag ret arms loc) =
     CaseEnum qty <$> dtightenE p tag
                  <*> dtightenS p ret
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 96f3d9e..9145e04 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -379,6 +379,26 @@ mutual
       qout = pi * pairres.qout + bodyout
     }
 
+  infer' ctx sg (Fst pair loc) = do
+    -- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
+    pairres <- inferC ctx sg pair
+    (tfst, _) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
+    -- then Ψ | Γ ⊢ σ · fst e ⇒ A ⊳ ωΣ
+    pure $ InfRes {
+      type = tfst,
+      qout = Any * pairres.qout
+    }
+
+  infer' ctx sg (Snd pair loc) = do
+    -- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
+    pairres <- inferC ctx sg pair
+    (_, tsnd) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
+    -- then Ψ | Γ ⊢ σ · snd e ⇒ B[fst e/x] ⊳ ωΣ
+    pure $ InfRes {
+      type = sub1 tsnd (Fst pair loc),
+      qout = Any * pairres.qout
+    }
+
   infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index a46d3e8..831ee8d 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -23,12 +23,12 @@ where
 
 parameters {auto _ : CanWhnf Term Interface.isRedexT}
            {auto _ : CanWhnf Elim Interface.isRedexE}
-           {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (pi : SQty)
+           {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
   ||| reduce a function application `App (Coe ty p q val) s loc`
   export covering
   piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
           (val, s : Term d n) -> Loc ->
-          Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
   piCoe sty@(S [< i] ty) p q val s loc = do
     -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
     -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
@@ -42,17 +42,17 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
         body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc
         s1   = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc)
                     (s // shift 1) s.loc
-    whnf defs ctx pi $ CoeT i (sub1 res s1) p q body loc
+    whnf defs ctx sg $ CoeT i (sub1 res s1) p q body loc
 
   ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc`
   export covering
   sigCoe : (qty : Qty) ->
            (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
            (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
-           Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
   sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
-    -- ⇝
+    --   ⇝
     -- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
     -- of { (a, b) ⇒
     --   e[(coe [i ⇒ A] @p @q a)/a,
@@ -68,17 +68,57 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
           (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
             (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
         b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
-    whnf defs ctx pi $ CasePair qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
 
+  ||| reduce a pair projection `Fst (Coe ty p q val) loc`
+  export covering
+  fstCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+           Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
+  fstCoe sty@(S [< i] ty) p q val loc = do
+    -- fst (coe (𝑖 ⇒ (x : A) × B) @p @q s)
+    --   ⇝
+    -- coe (𝑖 ⇒ A) @p @q (fst (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
+    --
+    -- type-case is used to expose A,B if the type is neutral
+    let ctx1 = extendDim i ctx
+    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
+    (tfst, _) <- tycaseSig defs ctx1 ty
+    whnf defs ctx sg $
+      Coe (ST [< i] tfst) p q
+          (E (Fst (Ann val (ty // one p) val.loc) val.loc)) loc
+
+  ||| reduce a pair projection `Snd (Coe ty p q val) loc`
+  export covering
+  sndCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+           Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
+  sndCoe sty@(S [< i] ty) p q val loc = do
+    -- snd (coe (𝑖 ⇒ (x : A) × B) @p @q s)
+    --   ⇝
+    -- coe (𝑖 ⇒ B[coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑖 (fst (s ∷ (x : A) × B))/x]) @p @q
+    --     (snd (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
+    --
+    -- type-case is used to expose A,B if the type is neutral
+    let ctx1 = extendDim i ctx
+    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
+    (tfst, tsnd) <- tycaseSig defs ctx1 ty
+    whnf defs ctx sg $
+      Coe (ST [< i] $ sub1 tsnd $
+            Coe (ST [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2))
+                (weakD 1 p) (BV 0 loc)
+                (E (Fst (Ann (dweakT 1 val) ty val.loc) val.loc)) loc)
+          p q
+          (E (Snd (Ann val (ty // one p) val.loc) val.loc))
+          loc
+
   ||| reduce a dimension application `DApp (Coe ty p q val) r loc`
   export covering
   eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
           (r : Dim d) -> Loc ->
-          Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
   eqCoe sty@(S [< j] ty) p q val r loc = do
     -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
-    -- ⇝
+    --   ⇝
     -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
     --   @r { 0 j ⇒ L; 1 j ⇒ R }
     let ctx1 = extendDim j ctx
@@ -86,23 +126,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
     let a'   = dsub1 a (weakD 1 r)
         val' = E $ DApp (Ann val (ty // one p) val.loc) r loc
-    whnf defs ctx pi $ CompH j a' p q val' r j s j t loc
+    whnf defs ctx sg $ CompH j a' p q val' r j s j t loc
 
   ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
   export covering
   boxCoe : (qty : Qty) ->
            (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
            (ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
-           Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
   boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
-    -- ⇝
+    --   ⇝
     -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
     let ctx1 = extendDim i ctx
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     ta <- tycaseBOX defs ctx1 ty
     let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
-    whnf defs ctx pi $ CaseBox qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
@@ -110,13 +150,13 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   export covering
   pushCoe : BindName ->
             (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
-            (0 pc : So (canPushCoe pi ty s)) =>
-            Eff Whnf (NonRedex Elim d n defs pi)
+            (0 pc : So (canPushCoe sg ty s)) =>
+            Eff Whnf (NonRedex Elim d n defs sg)
   pushCoe i ty p q s loc =
     case ty of
       -- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
       TYPE l tyLoc =>
-        whnf defs ctx pi $ Ann s (TYPE l tyLoc) loc
+        whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc
 
       -- η expand it so that whnf for App can deal with it
       --
@@ -125,7 +165,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
       Pi {} =>
         let inner = Coe (SY [< i] ty) p q s loc in
-        whnf defs ctx pi $
+        whnf defs ctx sg $
           Ann (LamY !(mnb "y" loc)
                   (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
               (ty // one q) loc
@@ -147,12 +187,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
                    (tfst // (BV 0 loc ::: shift 2))
                    (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
             snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
-        whnf defs ctx pi $
+        whnf defs ctx sg $
           Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
 
       -- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
       Enum cases tyLoc =>
-        whnf defs ctx pi $ Ann s (Enum cases tyLoc) loc
+        whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
 
       -- η expand, same as for Π
       --
@@ -161,14 +201,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
       Eq {} =>
         let inner = Coe (SY [< i] ty) p q s loc in
-        whnf defs ctx pi $
+        whnf defs ctx sg $
           Ann (DLamY !(mnb "k" loc)
                   (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
               (ty // one q) loc
 
       -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
       Nat tyLoc =>
-        whnf defs ctx pi $ Ann s (Nat tyLoc) loc
+        whnf defs ctx sg $ Ann s (Nat tyLoc) loc
 
       -- η expand
       --
@@ -185,4 +225,4 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
               loc
             }
         in
-        whnf defs ctx pi $ Ann (Box (E inner) loc) (ty // one q) loc
+        whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr
index 9e73fd1..1f299b9 100644
--- a/lib/Quox/Whnf/ComputeElimType.idr
+++ b/lib/Quox/Whnf/ComputeElimType.idr
@@ -41,11 +41,21 @@ computeElimType defs ctx pi e {ne} =
     App f s loc =>
       case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
         Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
-        t                => throw $ ExpectedPi loc ctx.names t
+        ty               => throw $ ExpectedPi loc ctx.names ty
 
     CasePair {pair, ret, _} =>
       pure $ sub1 ret pair
 
+    Fst pair loc =>
+      case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
+        Sig {fst, _} => pure fst
+        ty           => throw $ ExpectedSig loc ctx.names ty
+
+    Snd pair loc =>
+      case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
+        Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
+        ty           => throw $ ExpectedSig loc ctx.names ty
+
     CaseEnum {tag, ret, _} =>
       pure $ sub1 ret tag
 
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index 68bb919..fd10b0e 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -155,24 +155,24 @@ isK _      = False
 ||| - `val` is a constructor form
 public export %inline
 canPushCoe : SQty -> (ty, val : Term {}) -> Bool
-canPushCoe pi (TYPE  {}) _         = True
-canPushCoe pi (Pi    {}) _         = True
-canPushCoe pi (Lam   {}) _         = False
-canPushCoe pi (Sig   {}) (Pair {}) = True
-canPushCoe pi (Sig   {}) _         = False
-canPushCoe pi (Pair  {}) _         = False
-canPushCoe pi (Enum  {}) _         = True
-canPushCoe pi (Tag   {}) _         = False
-canPushCoe pi (Eq    {}) _         = True
-canPushCoe pi (DLam  {}) _         = False
-canPushCoe pi (Nat   {}) _         = True
-canPushCoe pi (Zero  {}) _         = False
-canPushCoe pi (Succ  {}) _         = False
-canPushCoe pi (BOX   {}) _         = True
-canPushCoe pi (Box   {}) _         = False
-canPushCoe pi (E     {}) _         = False
-canPushCoe pi (CloT  {}) _         = False
-canPushCoe pi (DCloT {}) _         = False
+canPushCoe sg (TYPE  {}) _         = True
+canPushCoe sg (Pi    {}) _         = True
+canPushCoe sg (Lam   {}) _         = False
+canPushCoe sg (Sig   {}) (Pair {}) = True
+canPushCoe sg (Sig   {}) _         = False
+canPushCoe sg (Pair  {}) _         = False
+canPushCoe sg (Enum  {}) _         = True
+canPushCoe sg (Tag   {}) _         = False
+canPushCoe sg (Eq    {}) _         = True
+canPushCoe sg (DLam  {}) _         = False
+canPushCoe sg (Nat   {}) _         = True
+canPushCoe sg (Zero  {}) _         = False
+canPushCoe sg (Succ  {}) _         = False
+canPushCoe sg (BOX   {}) _         = True
+canPushCoe sg (Box   {}) _         = False
+canPushCoe sg (E     {}) _         = False
+canPushCoe sg (CloT  {}) _         = False
+canPushCoe sg (DCloT {}) _         = False
 
 
 mutual
@@ -184,40 +184,44 @@ mutual
   |||    an application whose head is an annotated lambda,
   |||    a case expression whose head is an annotated constructor form, etc
   ||| 4. a redundant annotation, or one whose term or type is reducible
-  ||| 5. a coercion `coe (𝑖 ⇒ A) @p @pi s` where:
+  ||| 5. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
   |||      a. `A` is reducible or a type constructor, or
   |||      b. `𝑖` is not mentioned in `A`
   |||         ([fixme] should be A‹0/𝑖› = A‹1/𝑖›), or
-  |||      c. `p = pi`
-  ||| 6. a composition `comp A @p @pi s @r {⋯}`
-  |||    where `p = pi`, `r = 0`, or `r = 1`
+  |||      c. `p = q`
+  ||| 6. a composition `comp A @p @q s @r {⋯}`
+  |||    where `p = q`, `r = 0`, or `r = 1`
   ||| 7. a closure
   public export
   isRedexE : RedexTest Elim
-  isRedexE defs pi (F {x, u, _}) {d, n} =
+  isRedexE defs sg (F {x, u, _}) {d, n} =
     isJust $ lookupElim x u defs {d, n}
-  isRedexE _ pi (B {}) = False
-  isRedexE defs pi (App {fun, _}) =
-    isRedexE defs pi fun || isLamHead fun
-  isRedexE defs pi (CasePair {pair, _}) =
-    isRedexE defs pi pair || isPairHead pair
-  isRedexE defs pi (CaseEnum {tag, _}) =
-    isRedexE defs pi tag || isTagHead tag
-  isRedexE defs pi (CaseNat {nat, _}) =
-    isRedexE defs pi nat || isNatHead nat
-  isRedexE defs pi (CaseBox {box, _}) =
-    isRedexE defs pi box || isBoxHead box
-  isRedexE defs pi (DApp {fun, arg, _}) =
-    isRedexE defs pi fun || isDLamHead fun || isK arg
-  isRedexE defs pi (Ann {tm, ty, _}) =
-    isE tm || isRedexT defs pi tm || isRedexT defs SZero ty
-  isRedexE defs pi (Coe {ty = S _ (N _), _}) = True
-  isRedexE defs pi (Coe {ty = S _ (Y ty), p, q, val, _}) =
-    isRedexT defs SZero ty || canPushCoe pi ty val || isYes (p `decEqv` q)
-  isRedexE defs pi (Comp {ty, p, q, r, _}) =
+  isRedexE _ sg (B {}) = False
+  isRedexE defs sg (App {fun, _}) =
+    isRedexE defs sg fun || isLamHead fun
+  isRedexE defs sg (CasePair {pair, _}) =
+    isRedexE defs sg pair || isPairHead pair || isYes (sg `decEq` SZero)
+  isRedexE defs sg (Fst pair _) =
+    isRedexE defs sg pair || isPairHead pair
+  isRedexE defs sg (Snd pair _) =
+    isRedexE defs sg pair || isPairHead pair
+  isRedexE defs sg (CaseEnum {tag, _}) =
+    isRedexE defs sg tag || isTagHead tag
+  isRedexE defs sg (CaseNat {nat, _}) =
+    isRedexE defs sg nat || isNatHead nat
+  isRedexE defs sg (CaseBox {box, _}) =
+    isRedexE defs sg box || isBoxHead box
+  isRedexE defs sg (DApp {fun, arg, _}) =
+    isRedexE defs sg fun || isDLamHead fun || isK arg
+  isRedexE defs sg (Ann {tm, ty, _}) =
+    isE tm || isRedexT defs sg tm || isRedexT defs SZero ty
+  isRedexE defs sg (Coe {ty = S _ (N _), _}) = True
+  isRedexE defs sg (Coe {ty = S _ (Y ty), p, q, val, _}) =
+    isRedexT defs SZero ty || canPushCoe sg ty val || isYes (p `decEqv` q)
+  isRedexE defs sg (Comp {ty, p, q, r, _}) =
     isYes (p `decEqv` q) || isK r
-  isRedexE defs pi (TypeCase {ty, ret, _}) =
-    isRedexE defs pi ty || isRedexT defs pi ret || isAnnTyCon ty
+  isRedexE defs sg (TypeCase {ty, ret, _}) =
+    isRedexE defs sg ty || isRedexT defs sg ret || isAnnTyCon ty
   isRedexE _ _ (CloE  {}) = True
   isRedexE _ _ (DCloE {}) = True
 
@@ -231,5 +235,5 @@ mutual
   isRedexT : RedexTest Term
   isRedexT _    _  (CloT  {}) = True
   isRedexT _    _  (DCloT {}) = True
-  isRedexT defs pi (E {e, _}) = isAnn e || isRedexE defs pi e
+  isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
   isRedexT _    _  _          = False
diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index 93f8515..6aff789 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -16,53 +16,88 @@ export covering CanWhnf Elim Interface.isRedexE
 
 covering
 CanWhnf Elim Interface.isRedexE where
-  whnf defs ctx rh (F x u loc) with (lookupElim x u defs) proof eq
-    _ | Just y  = whnf defs ctx rh $ setLoc loc y
+  whnf defs ctx sg (F x u loc) with (lookupElim x u defs) proof eq
+    _ | Just y  = whnf defs ctx sg $ setLoc loc y
     _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
 
   whnf _ _ _ (B i loc) = pure $ nred $ B i loc
 
   -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
-  whnf defs ctx rh (App f s appLoc) = do
-    Element f fnf <- whnf defs ctx rh f
+  whnf defs ctx sg (App f s appLoc) = do
+    Element f fnf <- whnf defs ctx sg f
     case nchoose $ isLamHead f of
       Left _ => case f of
         Ann (Lam {body, _}) (Pi {arg, res, _}) floc =>
           let s = Ann s arg s.loc in
-          whnf defs ctx rh $ Ann (sub1 body s) (sub1 res s) appLoc
-        Coe ty p q val _ => piCoe defs ctx rh ty p q val s appLoc
+          whnf defs ctx sg $ Ann (sub1 body s) (sub1 res s) appLoc
+        Coe ty p q val _ => piCoe defs ctx sg ty p q val s appLoc
       Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
 
   -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
   -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
-  whnf defs ctx rh (CasePair pi pair ret body caseLoc) = do
-    Element pair pairnf <- whnf defs ctx rh pair
+  --
+  -- 0 · case e return p ⇒ C of { (a, b) ⇒ u } ⇝
+  -- u[fst e/a, snd e/b] ∷ C[e/p]
+  whnf defs ctx sg (CasePair pi pair ret body caseLoc) = do
+    Element pair pairnf <- whnf defs ctx sg pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
         Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
           let fst = Ann fst tfst fst.loc
               snd = Ann snd (sub1 tsnd fst) snd.loc
           in
-          whnf defs ctx rh $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
+          whnf defs ctx sg $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
         Coe ty p q val _ => do
-          sigCoe defs ctx rh pi ty p q val ret body caseLoc
+          sigCoe defs ctx sg pi ty p q val ret body caseLoc
       Right np =>
-        pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np
+        case sg `decEq` SZero of
+          Yes Refl =>
+            whnf defs ctx SZero $
+              Ann (subN body [< Fst pair caseLoc, Snd pair caseLoc])
+                  (sub1 ret pair)
+                  caseLoc
+          No n0 =>
+            pure $ Element (CasePair pi pair ret body caseLoc)
+                           (pairnf `orNo` np `orNo` notYesNo n0)
+
+  -- fst ((s, t) ∷ (x : A) × B) ⇝ s ∷ A
+  whnf defs ctx sg (Fst pair fstLoc) = do
+    Element pair pairnf <- whnf defs ctx sg pair
+    case nchoose $ isPairHead pair of
+      Left _ => case pair of
+        Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
+          whnf defs ctx sg $ Ann fst tfst pairLoc
+        Coe ty p q val _ => do
+          fstCoe defs ctx sg ty p q val fstLoc
+      Right np =>
+        pure $ Element (Fst pair fstLoc) (pairnf `orNo` np)
+
+  -- snd ((s, t) ∷ (x : A) × B) ⇝ t ∷ B[(s ∷ A)/x]
+  whnf defs ctx sg (Snd pair sndLoc) = do
+    Element pair pairnf <- whnf defs ctx sg pair
+    case nchoose $ isPairHead pair of
+      Left _ => case pair of
+        Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
+          whnf defs ctx sg $ Ann snd (sub1 tsnd (Ann fst tfst fst.loc)) sndLoc
+        Coe ty p q val _ => do
+          sndCoe defs ctx sg ty p q val sndLoc
+      Right np =>
+        pure $ Element (Snd pair sndLoc) (pairnf `orNo` np)
 
   -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
   -- u ∷ C['a∷{a,…}/p]
-  whnf defs ctx rh (CaseEnum pi tag ret arms caseLoc) = do
-    Element tag tagnf <- whnf defs ctx rh tag
+  whnf defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
+    Element tag tagnf <- whnf defs ctx sg tag
     case nchoose $ isTagHead tag of
       Left _ => case tag of
         Ann (Tag t _) (Enum ts _) _ =>
           let ty = sub1 ret tag in
           case lookup t arms of
-            Just arm => whnf defs ctx rh $ Ann arm ty arm.loc
+            Just arm => whnf defs ctx sg $ Ann arm ty arm.loc
             Nothing  => throw $ MissingEnumArm caseLoc t (keys arms)
         Coe ty p q val _ =>
           -- there is nowhere an equality can be hiding inside an enum type
-          whnf defs ctx rh $
+          whnf defs ctx sg $
             CaseEnum pi (Ann val (dsub1 ty q) val.loc) ret arms caseLoc
       Right nt =>
         pure $ Element (CaseEnum pi tag ret arms caseLoc) $ tagnf `orNo` nt
@@ -72,37 +107,37 @@ CanWhnf Elim Interface.isRedexE where
   --
   -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
   --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
-  whnf defs ctx rh (CaseNat pi piIH nat ret zer suc caseLoc) = do
-    Element nat natnf <- whnf defs ctx rh nat
+  whnf defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
+    Element nat natnf <- whnf defs ctx sg nat
     case nchoose $ isNatHead nat of
       Left _ =>
         let ty = sub1 ret nat in
         case nat of
           Ann (Zero _) (Nat _) _ =>
-            whnf defs ctx rh $ Ann zer ty zer.loc
+            whnf defs ctx sg $ Ann zer ty zer.loc
           Ann (Succ n succLoc) (Nat natLoc) _ =>
             let nn = Ann n (Nat natLoc) succLoc
                 tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
             in
-            whnf defs ctx rh $ Ann tm ty caseLoc
+            whnf defs ctx sg $ Ann tm ty caseLoc
           Coe ty p q val _ =>
             -- same deal as Enum
-            whnf defs ctx rh $
+            whnf defs ctx sg $
               CaseNat pi piIH (Ann val (dsub1 ty q) val.loc) ret zer suc caseLoc
       Right nn => pure $
         Element (CaseNat pi piIH nat ret zer suc caseLoc) (natnf `orNo` nn)
 
   -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
   --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
-  whnf defs ctx rh (CaseBox pi box ret body caseLoc) = do
-    Element box boxnf <- whnf defs ctx rh box
+  whnf defs ctx sg (CaseBox pi box ret body caseLoc) = do
+    Element box boxnf <- whnf defs ctx sg box
     case nchoose $ isBoxHead box of
       Left _ => case box of
         Ann (Box val boxLoc) (BOX q bty tyLoc) _ =>
           let ty = sub1 ret box in
-          whnf defs ctx rh $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
+          whnf defs ctx sg $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
         Coe ty p q val _ =>
-          boxCoe defs ctx rh pi ty p q val ret body caseLoc
+          boxCoe defs ctx sg pi ty p q val ret body caseLoc
       Right nb =>
         pure $ Element (CaseBox pi box ret body caseLoc) (boxnf `orNo` nb)
 
@@ -110,35 +145,35 @@ CanWhnf Elim Interface.isRedexE where
   -- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
   --
   -- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
-  whnf defs ctx rh (DApp f p appLoc) = do
-    Element f fnf <- whnf defs ctx rh f
+  whnf defs ctx sg (DApp f p appLoc) = do
+    Element f fnf <- whnf defs ctx sg f
     case nchoose $ isDLamHead f of
       Left _ => case f of
         Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ =>
-          whnf defs ctx rh $
+          whnf defs ctx sg $
             Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p)
                 (dsub1 ty p) appLoc
         Coe ty p' q' val _ =>
-          eqCoe defs ctx rh ty p' q' val p appLoc
+          eqCoe defs ctx sg ty p' q' val p appLoc
       Right ndlh => case p of
         K e _ => do
-          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx rh f
+          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
             | ty => throw $ ExpectedEq ty.loc ctx.names ty
-          whnf defs ctx rh $
+          whnf defs ctx sg $
             ends (Ann (setLoc appLoc l) ty.zero appLoc)
                  (Ann (setLoc appLoc r) ty.one  appLoc) e
         B {} => pure $ Element (DApp f p appLoc) (fnf `orNo` ndlh `orNo` Ah)
 
   -- e ∷ A ⇝ e
-  whnf defs ctx rh (Ann s a annLoc) = do
-    Element s snf <- whnf defs ctx rh s
+  whnf defs ctx sg (Ann s a annLoc) = do
+    Element s snf <- whnf defs ctx sg s
     case nchoose $ isE s of
       Left  _  => let E e = s in pure $ Element e $ noOr2 snf
       Right ne => do
         Element a anf <- whnf defs ctx SZero a
         pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
 
-  whnf defs ctx rh (Coe sty p q val coeLoc) =
+  whnf defs ctx sg (Coe sty p q val coeLoc) =
     --   𝑖 ∉ fv(A)
     -- -------------------------------
     --   coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
@@ -148,30 +183,30 @@ CanWhnf Elim Interface.isRedexE where
       ([< i], Left ty) =>
         case p `decEqv` q of
           -- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
-          Yes _   => whnf defs ctx rh $ Ann val (dsub1 sty p) coeLoc
+          Yes _   => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
           No  npq => do
             Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
-            case nchoose $ canPushCoe rh ty val of
-              Left  pc  => pushCoe defs ctx rh i ty p q val coeLoc
+            case nchoose $ canPushCoe sg ty val of
+              Left  pc  => pushCoe defs ctx sg i ty p q val coeLoc
               Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
                                           (tynf `orNo` npc `orNo` notYesNo npq)
       (_, Right ty) =>
-        whnf defs ctx rh $ Ann val ty coeLoc
+        whnf defs ctx sg $ Ann val ty coeLoc
 
-  whnf defs ctx rh (Comp ty p q val r zero one compLoc) =
+  whnf defs ctx sg (Comp ty p q val r zero one compLoc) =
     case p `decEqv` q of
       -- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
-      Yes y   => whnf defs ctx rh $ Ann val ty compLoc
+      Yes y   => whnf defs ctx sg $ Ann val ty compLoc
       No  npq => case r of
         -- comp [A] @p @q s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹q/𝑗› ∷ A
-        K Zero _ => whnf defs ctx rh $ Ann (dsub1 zero q) ty compLoc
+        K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero q) ty compLoc
         -- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
-        K One  _ => whnf defs ctx rh $ Ann (dsub1 one  q) ty compLoc
+        K One  _ => whnf defs ctx sg $ Ann (dsub1 one  q) ty compLoc
         B {}     => pure $ Element (Comp ty p q val r zero one compLoc)
                                    (notYesNo npq `orNo` Ah)
 
-  whnf defs ctx rh (TypeCase ty ret arms def tcLoc) =
-    case rh `decEq` SZero of
+  whnf defs ctx sg (TypeCase ty ret arms def tcLoc) =
+    case sg `decEq` SZero of
       Yes Refl => do
         Element ty  tynf  <- whnf defs ctx SZero ty
         Element ret retnf <- whnf defs ctx SZero ret
@@ -181,12 +216,12 @@ CanWhnf Elim Interface.isRedexE where
           Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
                                      (tynf `orNo` retnf `orNo` nt)
       No _ =>
-        throw $ ClashQ tcLoc rh.qty Zero
+        throw $ ClashQ tcLoc sg.qty Zero
 
-  whnf defs ctx rh (CloE (Sub el th)) =
-    whnf defs ctx rh $ pushSubstsWith' id th el
-  whnf defs ctx rh (DCloE (Sub el th)) =
-    whnf defs ctx rh $ pushSubstsWith' th id el
+  whnf defs ctx sg (CloE (Sub el th)) =
+    whnf defs ctx sg $ pushSubstsWith' id th el
+  whnf defs ctx sg (DCloE (Sub el th)) =
+    whnf defs ctx sg $ pushSubstsWith' th id el
 
 covering
 CanWhnf Term Interface.isRedexT where
@@ -206,13 +241,13 @@ CanWhnf Term Interface.isRedexT where
   whnf _ _ _ t@(Box  {}) = pure $ nred t
 
   -- s ∷ A ⇝ s   (in term context)
-  whnf defs ctx rh (E e) = do
-    Element e enf <- whnf defs ctx rh e
+  whnf defs ctx sg (E e) = do
+    Element e enf <- whnf defs ctx sg e
     case nchoose $ isAnn e of
       Left  _  => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
       Right na => pure $ Element (E e) $ na `orNo` enf
 
-  whnf defs ctx rh (CloT (Sub tm th)) =
-    whnf defs ctx rh $ pushSubstsWith' id th tm
-  whnf defs ctx rh (DCloT (Sub tm th)) =
-    whnf defs ctx rh $ pushSubstsWith' th id tm
+  whnf defs ctx sg (CloT (Sub tm th)) =
+    whnf defs ctx sg $ pushSubstsWith' id th tm
+  whnf defs ctx sg (DCloT (Sub tm th)) =
+    whnf defs ctx sg $ pushSubstsWith' th id tm