From 0aafa0f6c02205e3c6ca9d2c9c3e3b8ae9ed447c Mon Sep 17 00:00:00 2001
From: russoul <me@russoul.me>
Date: Thu, 21 Dec 2023 03:05:07 +0400
Subject: [PATCH] Implement let definitions where RHS is a large type

---
 nova-api.ipkg                                 |  2 +-
 nova.ipkg                                     |  2 +-
 src/idris/Nova/Core/Context.idr               | 79 +++++++++++++----
 src/idris/Nova/Core/Conversion.idr            |  4 +
 src/idris/Nova/Core/Evaluation.idr            |  5 +-
 src/idris/Nova/Core/Language.idr              | 12 ++-
 .../Core/{FreeVariable.idr => Occurrence.idr} |  3 +-
 src/idris/Nova/Core/Pretty.idr                | 32 +++++++
 src/idris/Nova/Core/Rigidity.idr              |  1 +
 src/idris/Nova/Core/Shrinking.idr             |  5 ++
 src/idris/Nova/Core/Substitution.idr          | 41 ++++++++-
 src/idris/Nova/Core/Unification.idr           | 20 +++++
 src/idris/Nova/Surface/Elaboration.idr        | 84 ++++++++++++++++---
 src/idris/Nova/Surface/Language.idr           | 20 ++++-
 src/idris/Nova/Surface/Parser.idr             | 29 ++++++-
 src/idris/Nova/Surface/Shunting.idr           |  6 ++
 src/idris/Nova/Surface/Tactic/Unfold.idr      | 17 ++++
 src/nova/Test.nova                            | 38 +++++++++
 src/text/Internals/NovaFoundation.txt         | 29 +++++++
 19 files changed, 392 insertions(+), 37 deletions(-)
 rename src/idris/Nova/Core/{FreeVariable.idr => Occurrence.idr} (98%)

diff --git a/nova-api.ipkg b/nova-api.ipkg
index 26ecd58..d18639a 100644
--- a/nova-api.ipkg
+++ b/nova-api.ipkg
@@ -15,10 +15,10 @@ modules =
         , Nova.Core.Context
         , Nova.Core.Conversion
         , Nova.Core.Evaluation
-        , Nova.Core.FreeVariable
         , Nova.Core.Language
         , Nova.Core.Monad
         , Nova.Core.Name
+        , Nova.Core.Occurrence
         , Nova.Core.Pretty
         , Nova.Core.Rigidity
         , Nova.Core.Shrinking
diff --git a/nova.ipkg b/nova.ipkg
index d54980f..c4dd222 100644
--- a/nova.ipkg
+++ b/nova.ipkg
@@ -15,10 +15,10 @@ modules =
         , Nova.Core.Context
         , Nova.Core.Conversion
         , Nova.Core.Evaluation
-        , Nova.Core.FreeVariable
         , Nova.Core.Language
         , Nova.Core.Monad
         , Nova.Core.Name
+        , Nova.Core.Occurrence
         , Nova.Core.Pretty
         , Nova.Core.Rigidity
         , Nova.Core.Shrinking
diff --git a/src/idris/Nova/Core/Context.idr b/src/idris/Nova/Core/Context.idr
index 9d09f3b..a39f560 100644
--- a/src/idris/Nova/Core/Context.idr
+++ b/src/idris/Nova/Core/Context.idr
@@ -8,38 +8,87 @@ import Nova.Core.Substitution
 ||| Σ ⊦ Δ(↑(x Σ₁))
 ||| Σ Δ(↑(x Σ₁)) ⊦ A(↑(x Σ₁)) type
 public export
-lookupSignature : Signature -> VarName -> Maybe (Context, Nat, Typ)
-lookupSignature [<] x = Nothing
-lookupSignature (sig :< (x, ElemEntry ctx ty)) y = M.do
+lookupElemSignature : Signature -> VarName -> Maybe (Context, Nat, Typ)
+lookupElemSignature [<] x = Nothing
+lookupElemSignature (sig :< (x, ElemEntry ctx ty)) y = do
   case x == y of
     True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim ty Wk)
     False => do
-      (ctx, i, ty) <- lookupSignature sig y
+      (ctx, i, ty) <- lookupElemSignature sig y
       Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
-lookupSignature (sig :< (x, LetElemEntry ctx _ ty)) y = M.do
+lookupElemSignature (sig :< (x, LetElemEntry ctx _ ty)) y = do
   case x == y of
     True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim ty Wk)
     False => do
-      (ctx, i, ty) <- lookupSignature sig y
+      (ctx, i, ty) <- lookupElemSignature sig y
       Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
+lookupElemSignature (sig :< (x, TypeEntry {})) y = do
+  (ctx, i, ty) <- lookupElemSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
+lookupElemSignature (sig :< (x, LetTypeEntry {})) y = do
+  (ctx, i, ty) <- lookupElemSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim ty Wk)
 
-||| TODO: Factor this out
 public export
-lookupLetSignature : Signature -> VarName -> Maybe (Context, Nat, Elem, Typ)
-lookupLetSignature [<] x = Nothing
-lookupLetSignature (sig :< (x, ElemEntry ctx ty)) y = M.do
+lookupTypeSignature : Signature -> VarName -> Maybe (Context, Nat)
+lookupTypeSignature [<] x = Nothing
+lookupTypeSignature (sig :< (x, ElemEntry ctx ty)) y = do
+  (ctx, i) <- lookupTypeSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i)
+lookupTypeSignature (sig :< (x, LetElemEntry ctx _ ty)) y = do
+  (ctx, i) <- lookupTypeSignature sig y
+  Just (subst ctx SubstSignature.Wk, S i)
+lookupTypeSignature (sig :< (x, TypeEntry ctx)) y = do
   case x == y of
-    True => Nothing
+    True => Just (subst ctx SubstSignature.Wk, 0)
     False => do
-      (ctx, i, rhs, ty) <- lookupLetSignature sig y
-      Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
-lookupLetSignature (sig :< (x, LetElemEntry ctx rhs ty)) y = M.do
+      (ctx, i) <- lookupTypeSignature sig y
+      Just (subst ctx SubstSignature.Wk, S i)
+lookupTypeSignature (sig :< (x, LetTypeEntry ctx rhs)) y = do
+  case x == y of
+    True => Just (subst ctx SubstSignature.Wk, 0)
+    False => do
+      (ctx, i) <- lookupTypeSignature sig y
+      Just (subst ctx SubstSignature.Wk, S i)
+
+public export
+lookupLetElemSignature : Signature -> VarName -> Maybe (Context, Nat, Elem, Typ)
+lookupLetElemSignature [<] x = Nothing
+lookupLetElemSignature (sig :< (x, ElemEntry ctx ty)) y = do
+ (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
+lookupLetElemSignature (sig :< (x, TypeEntry {})) y = do
+ (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
+lookupLetElemSignature (sig :< (x, LetTypeEntry {})) y = do
+ (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
+lookupLetElemSignature (sig :< (x, LetElemEntry ctx rhs ty)) y = do
   case x == y of
     True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
     False => do
-      (ctx, i, rhs, ty) <- lookupLetSignature sig y
+      (ctx, i, rhs, ty) <- lookupLetElemSignature sig y
       Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk, SignatureSubstElim ty Wk)
 
+public export
+lookupLetTypeSignature : Signature -> VarName -> Maybe (Context, Nat, Typ)
+lookupLetTypeSignature [<] x = Nothing
+lookupLetTypeSignature (sig :< (x, ElemEntry ctx ty)) y = do
+ (ctx, i, rhs) <- lookupLetTypeSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+lookupLetTypeSignature (sig :< (x, TypeEntry {})) y = do
+ (ctx, i, rhs) <- lookupLetTypeSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+lookupLetTypeSignature (sig :< (x, LetElemEntry {})) y = do
+ (ctx, i, rhs) <- lookupLetTypeSignature sig y
+ Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+lookupLetTypeSignature (sig :< (x, LetTypeEntry ctx rhs)) y = do
+  case x == y of
+    True => Just (subst ctx SubstSignature.Wk, 0, SignatureSubstElim rhs Wk)
+    False => do
+      (ctx, i, rhs) <- lookupLetTypeSignature sig y
+      Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
+
 namespace Index
   ||| Looks up a signature entry by index. Weakens the result to be typed in the original signature.
   public export
diff --git a/src/idris/Nova/Core/Conversion.idr b/src/idris/Nova/Core/Conversion.idr
index 79ab4ae..c723057 100644
--- a/src/idris/Nova/Core/Conversion.idr
+++ b/src/idris/Nova/Core/Conversion.idr
@@ -34,6 +34,10 @@ mutual
       conv sig omega a0 a1 `and` conv sig omega b0 b1
     convNu sig omega (ElEqTy a0 b0 ty0) (ElEqTy a1 b1 ty1) =
       conv sig omega a0 a1 `and` conv sig omega b0 b1 `and` conv sig omega ty0 ty1
+    convNu sig omega (SignatureVarElim x0 sigma) (SignatureVarElim x1 tau) =
+     return (x0 == x1)
+        `and`
+      conv sig omega sigma tau
     convNu _ _ _ _ = return False
 
     public export
diff --git a/src/idris/Nova/Core/Evaluation.idr b/src/idris/Nova/Core/Evaluation.idr
index 9d0309e..0b8684a 100644
--- a/src/idris/Nova/Core/Evaluation.idr
+++ b/src/idris/Nova/Core/Evaluation.idr
@@ -7,8 +7,6 @@ import Nova.Core.Monad
 import Nova.Core.Language
 import Nova.Core.Substitution
 
---TODO: El should evaluate both in closed and open cases
-
 -- Closed term evaluation
 
 mutual
@@ -171,6 +169,7 @@ mutual
         _ => throw "closedEval(OmegaVarElim)"
     closedEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     closedEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
+    closedEvalNu sig omega (SignatureVarElim idx tau) = return (SignatureVarElim idx tau)
 
     ||| Σ ⊦ a ⇝ a' : A
     ||| Σ must only contain let-elem's
@@ -214,6 +213,8 @@ mutual
         Nothing => throw "openEval/Type(OmegaVarElim(Nothing))"
     openEvalNu sig omega (TyEqTy a0 a1) = return $ TyEqTy a0 a1
     openEvalNu sig omega (ElEqTy a0 a1 ty) = return $ ElEqTy a0 a1 ty
+    openEvalNu sig omega (SignatureVarElim k sigma) = M.do
+      return (SignatureVarElim k sigma)
 
     ||| Σ ⊦ a ⇝ a' : A
     ||| Computes head-normal form w.r.t. (~) relation used in unification.
diff --git a/src/idris/Nova/Core/Language.idr b/src/idris/Nova/Core/Language.idr
index 905e476..8dea55d 100644
--- a/src/idris/Nova/Core/Language.idr
+++ b/src/idris/Nova/Core/Language.idr
@@ -9,7 +9,9 @@ mutual
   public export
   data SignatureEntryInstance : Type where
     ElemEntryInstance : Elem -> SignatureEntryInstance
-    LetEntryInstance : SignatureEntryInstance
+    LetElemEntryInstance : SignatureEntryInstance
+    TypeEntryInstance : Typ -> SignatureEntryInstance
+    LetTypeEntryInstance : SignatureEntryInstance
 
   namespace SubstSignature
     ||| σ : Σ₀ ⇒ Σ₁
@@ -89,6 +91,8 @@ mutual
       SignatureSubstElim : Typ -> SubstSignature -> Typ
       ||| Xᵢ(σ)
       OmegaVarElim : OmegaName -> SubstContext -> Typ
+      ||| Xᵢ(σ)
+      SignatureVarElim : Nat -> SubstContext -> Typ
 
   namespace E
     public export
@@ -166,6 +170,10 @@ data SignatureEntry : Type where
   ElemEntry : Context -> Typ -> SignatureEntry
   ||| Γ ⊦ a : A
   LetElemEntry : Context -> Elem -> Typ -> SignatureEntry
+  ||| Γ ⊦ type
+  TypeEntry : Context -> SignatureEntry
+  ||| Γ ⊦ A
+  LetTypeEntry : Context -> Typ -> SignatureEntry
 
 Signature = SnocList (VarName, SignatureEntry)
 
@@ -174,6 +182,8 @@ namespace SignatureEntry
   getContext : SignatureEntry -> Context
   getContext (ElemEntry ctx ty)= ctx
   getContext (LetElemEntry ctx rhs ty) = ctx
+  getContext (TypeEntry ctx)= ctx
+  getContext (LetTypeEntry ctx rhs) = ctx
 
 public export
 data MetaKind = NoSolve | SolveByUnification | SolveByElaboration
diff --git a/src/idris/Nova/Core/FreeVariable.idr b/src/idris/Nova/Core/Occurrence.idr
similarity index 98%
rename from src/idris/Nova/Core/FreeVariable.idr
rename to src/idris/Nova/Core/Occurrence.idr
index 045e9cd..4507385 100644
--- a/src/idris/Nova/Core/FreeVariable.idr
+++ b/src/idris/Nova/Core/Occurrence.idr
@@ -1,4 +1,4 @@
-module Nova.Core.FreeVariable
+module Nova.Core.Occurrence
 
 import Data.AVL
 
@@ -44,6 +44,7 @@ mutual
       [| unite (freeOmegaName sig omega a) (freeOmegaName sig omega b) |]
     freeOmegaNameNu sig omega (ElEqTy a b ty) = M.do
       [| unite3 (freeOmegaName sig omega a) (freeOmegaName sig omega b) (freeOmegaName sig omega ty) |]
+    freeOmegaNameNu sig omega (SignatureVarElim j sigma) = freeOmegaName sig omega sigma
 
     ||| Compute free occurrences of Ω variables in the term modulo open evaluation.
     public export
diff --git a/src/idris/Nova/Core/Pretty.idr b/src/idris/Nova/Core/Pretty.idr
index 8117ab8..b242732 100644
--- a/src/idris/Nova/Core/Pretty.idr
+++ b/src/idris/Nova/Core/Pretty.idr
@@ -106,6 +106,10 @@ wrapTyp (El {}) lvl doc =
   case lvl <= 3 of
     True => return doc
     False => return (parens' doc)
+wrapTyp (SignatureVarElim {}) lvl doc =
+  case lvl <= 3 of
+    True => return doc
+    False => return (parens' doc)
 
 wrapElem : Elem -> Level -> Doc Ann -> M (Doc Ann)
 wrapElem (PiTy x dom cod) lvl doc =
@@ -392,6 +396,12 @@ mutual
     annotate Form "∈"
      <++>
     !(prettyTyp sig omega ctx ty 0)
+  prettyTyp' sig omega ctx (SignatureVarElim k sigma) = M.do
+    x <- prettySignatureVar sig k
+    return $
+      x
+       <+>
+      parens' !(prettySubstContext sig omega ctx sigma)
 
   public export
   prettyTyp : Signature
@@ -632,6 +642,8 @@ mutual
   prettySignatureEntry : Signature -> Omega -> VarName -> SignatureEntry -> M (Doc Ann)
    -- Γ ⊦ χ : A
    -- Γ ⊦ χ ≔ e : A
+   -- Γ ⊦ χ type
+   -- Γ ⊦ χ ≔ A type
   prettySignatureEntry sig omega x (ElemEntry ctx ty) = return $
     !(prettyContext sig omega ctx)
      <++>
@@ -656,6 +668,26 @@ mutual
     annotate Keyword ":"
      <++>
     !(prettyTyp sig omega (map fst ctx) ty 0)
+  prettySignatureEntry sig omega x (TypeEntry ctx) = return $
+    !(prettyContext sig omega ctx)
+     <++>
+    annotate Keyword "⊦"
+     <++>
+    annotate ContextVar (pretty x)
+     <++>
+    annotate Keyword "type"
+  prettySignatureEntry sig omega x (LetTypeEntry ctx e) = return $
+    !(prettyContext sig omega ctx)
+     <++>
+    annotate Keyword "⊦"
+     <++>
+    annotate ContextVar (pretty x)
+     <++>
+    annotate Keyword "≔"
+     <++>
+    !(prettyTyp sig omega (map fst ctx) e 0)
+     <++>
+    annotate Keyword "type"
 
   public export
   prettyConstraintEntry : Signature -> Omega -> ConstraintEntry -> M (Doc Ann)
diff --git a/src/idris/Nova/Core/Rigidity.idr b/src/idris/Nova/Core/Rigidity.idr
index 3dc519d..5990c16 100644
--- a/src/idris/Nova/Core/Rigidity.idr
+++ b/src/idris/Nova/Core/Rigidity.idr
@@ -34,6 +34,7 @@ mutual
         Nothing => assert_total $ idris_crash "isRigidNu(SignatureVarElim)(3)"
     isRigidNu sig omega (TyEqTy x y) = return True
     isRigidNu sig omega (ElEqTy x y z) = return True
+    isRigidNu sig omega (SignatureVarElim {}) = return True
 
     ||| A term is rigid if
     ||| there is no (~) that changes its constructor.
diff --git a/src/idris/Nova/Core/Shrinking.idr b/src/idris/Nova/Core/Shrinking.idr
index a0353fe..a899e88 100644
--- a/src/idris/Nova/Core/Shrinking.idr
+++ b/src/idris/Nova/Core/Shrinking.idr
@@ -93,6 +93,11 @@ mutual
       b <- shrink b gamma1Len gamma2Len
       c <- shrink c gamma1Len gamma2Len
       return (ElEqTy a b c)
+    shrinkNu (SignatureVarElim k sigma) gamma1Len gamma2Len = MMaybe.do
+      -- Σ₀ (Γ ⊦ χ : A) Σ₁ ⊦ σ : Δ ⇒ Γ
+      -- Σ₀ (Γ ⊦ χ : A) Σ₁ Δ ⊦ χ σ
+      sigma <- shrink sigma gamma1Len gamma2Len
+      return (SignatureVarElim k sigma)
 
     ||| Γ₀ ⊦ Γ₁ ctx
     ||| Γ₀ ⊦ Γ₂ ctx
diff --git a/src/idris/Nova/Core/Substitution.idr b/src/idris/Nova/Core/Substitution.idr
index 0304a5f..0042538 100644
--- a/src/idris/Nova/Core/Substitution.idr
+++ b/src/idris/Nova/Core/Substitution.idr
@@ -86,8 +86,12 @@ mutual
       subst (SignatureSubstElim t sigma1) spine
     substSignatureVar (S k) (Ext tau _) sigma1 spine =
       substSignatureVar k tau sigma1 spine
-    substSignatureVar 0 (Ext tau (LetEntryInstance {})) sigma1 spine =
-      assert_total $ idris_crash "Elem.substSignatureVar(LetEntryInstance)"
+    substSignatureVar 0 (Ext tau (LetElemEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetElemEntryInstance)"
+    substSignatureVar 0 (Ext tau (TypeEntryInstance t)) sigma1 spine = FailSt.do
+      assert_total $ idris_crash "Elem.substSignatureVar(TypeEntryInstance)"
+    substSignatureVar 0 (Ext tau (LetTypeEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetTypeEntryInstance)"
     substSignatureVar x Terminal sigma1 spine = assert_total $ idris_crash "substSignatureVar(Terminal)"
 
     ||| xᵢ(σ : Γ₁ ⇒ Γ₂)(τ : Γ₀ ⇒ Γ₁)
@@ -259,6 +263,27 @@ mutual
     subst ElEqVal tau = ElEqVal
 
   namespace D
+    public export
+    substSignatureVar : Nat -> SubstSignature -> SubstSignature -> SubstContext -> Typ
+    substSignatureVar x Id Id spine = SignatureVarElim x spine
+    substSignatureVar x Id sigma1 spine = substSignatureVar x sigma1 Id spine
+    substSignatureVar x Wk sigma1 spine = substSignatureVar (S x) sigma1 Id spine
+    substSignatureVar x (Chain Id tau) sigma spine = substSignatureVar x tau sigma spine
+    substSignatureVar x (Chain tau0 tau1) sigma1 spine = substSignatureVar x tau0 (Chain tau1 sigma1) spine
+    -- Σ (Δ ⊦ χ : A) | Γ ⊦ χ₀(ē)[τ, t] = t(ē[τ, t])
+    -- Σ (Δ ⊦ χ : A) | Γ ⊦ χ₁₊ᵢ(ē)[τ, t] = χᵢ(ē[τ, t])[τ]
+    substSignatureVar 0 (Ext tau (ElemEntryInstance t)) sigma1 spine = FailSt.do
+      assert_total $ idris_crash "Elem.substSignatureVar(ElemEntryInstance)"
+    substSignatureVar (S k) (Ext tau _) sigma1 spine =
+      substSignatureVar k tau sigma1 spine
+    substSignatureVar 0 (Ext tau (LetElemEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetElemEntryInstance)"
+    substSignatureVar 0 (Ext tau (TypeEntryInstance t)) sigma1 spine = FailSt.do
+      subst (SignatureSubstElim t sigma1) spine
+    substSignatureVar 0 (Ext tau (LetTypeEntryInstance {})) sigma1 spine =
+      assert_total $ idris_crash "Elem.substSignatureVar(LetTypeEntryInstance)"
+    substSignatureVar x Terminal sigma1 spine = assert_total $ idris_crash "substSignatureVar(Terminal)"
+
     public export
     subst : Typ -> SubstSignature -> Typ
     subst (PiTy x a b) sigma = PiTy x (SignatureSubstElim a sigma) (SignatureSubstElim b sigma)
@@ -276,6 +301,7 @@ mutual
     subst (OmegaVarElim k tau) sigma = OmegaVarElim k (subst tau sigma)
     subst (TyEqTy a0 a1) tau = TyEqTy (SignatureSubstElim a0 tau) (SignatureSubstElim a1 tau)
     subst (ElEqTy a0 a1 ty) tau = ElEqTy (SignatureSubstElim a0 tau) (SignatureSubstElim a1 tau) (SignatureSubstElim ty tau)
+    subst (SignatureVarElim k tau) sigma = substSignatureVar k sigma Id (subst tau sigma)
 
   namespace E
     ||| t(σ)
@@ -307,6 +333,7 @@ mutual
     subst (OmegaVarElim k sigma) tau = OmegaVarElim k (Chain sigma tau)
     subst (TyEqTy a0 a1) tau = TyEqTy (ContextSubstElim a0 tau) (ContextSubstElim a1 tau)
     subst (ElEqTy a0 a1 ty) tau = ElEqTy (ContextSubstElim a0 tau) (ContextSubstElim a1 tau) (ContextSubstElim ty tau)
+    subst (SignatureVarElim k sigma) tau = SignatureVarElim k (Chain sigma tau)
 
   namespace List
     public export
@@ -354,12 +381,18 @@ mutual
       ||| σ⁺(E) : Σ₀ E(σ) ⇒ Σ₁ E
       ||| σ⁺(Γ ⊦ x : A) : Σ₀ (Γ(σ) ⊦ x : A(σ)) ⇒ Σ₁ (Γ ⊦ x : A)
       ||| σ⁺(Γ ⊦ x ≔ e : A) : Σ₀ (Γ(σ) ⊦ x ≔ e(σ) : A(σ)) ⇒ Σ₁ (Γ ⊦ x ≔ e : A)
+      ||| σ⁺(Γ ⊦ X type) : Σ₀ (Γ(σ) ⊦ X type) ⇒ Σ₁ (Γ ⊦ X type)
+      ||| σ⁺(Γ ⊦ X ≔ A type) : Σ₀ (Γ(σ) ⊦ X ≔ A(σ) type) ⇒ Σ₁ (Γ ⊦ X ≔ A type)
       public export
       Under : SubstSignature -> SignatureEntry -> SubstSignature
       Under sigma (ElemEntry ctx ty) =
         Ext (Chain sigma Wk) (ElemEntryInstance $ SignatureVarElim 0 Id)
       Under sigma (LetElemEntry ctx e ty) =
-        Ext (Chain sigma Wk) LetEntryInstance
+        Ext (Chain sigma Wk) LetElemEntryInstance
+      Under sigma (TypeEntry ctx) =
+        Ext (Chain sigma Wk) (TypeEntryInstance $ SignatureVarElim 0 Id)
+      Under sigma (LetTypeEntry ctx rhs) =
+        Ext (Chain sigma Wk) LetTypeEntryInstance
 
       ||| σ : Σ₀ ⇒ Σ₁
       ||| Σ₁ ⊦ Δ sig
@@ -385,6 +418,8 @@ namespace SignatureEntry
   subst : SignatureEntry -> SubstSignature -> SignatureEntry
   subst (ElemEntry ctx ty) sigma = ElemEntry (subst ctx sigma) (SignatureSubstElim ty sigma)
   subst (LetElemEntry ctx e ty) sigma = LetElemEntry (subst ctx sigma) (SignatureSubstElim e sigma) (SignatureSubstElim ty sigma)
+  subst (TypeEntry ctx) sigma = TypeEntry (subst ctx sigma)
+  subst (LetTypeEntry ctx rhs) sigma = LetTypeEntry (subst ctx sigma) (SignatureSubstElim rhs sigma)
 
 namespace EntryList
   public export
diff --git a/src/idris/Nova/Core/Unification.idr b/src/idris/Nova/Core/Unification.idr
index ba45b20..3547507 100644
--- a/src/idris/Nova/Core/Unification.idr
+++ b/src/idris/Nova/Core/Unification.idr
@@ -185,6 +185,20 @@ mutual
       b <- invert sig omega ctx delta sigma b
       ty <- invert sig omega ctx delta sigma ty
       return (ElEqTy a b ty)
+    invertNu sig omega ctx delta sigma (SignatureVarElim k tau) = MMaybe.do
+      tau' <- invert sig omega sigma tau ctx delta getCtx
+      return (SignatureVarElim k tau')
+     where
+      getCtx : Context
+      getCtx =
+        case (splitAt sig k) of
+          Nothing => assert_total $ idris_crash "invertNu(SignatureVarElim)(1)"
+          Just (_, (_, e), rest) =>
+            case subst e (WkN $ 1 + length rest) of
+             TypeEntry xi {} => xi
+             LetTypeEntry xi rhs => xi
+             ElemEntry {} => assert_total $ idris_crash "invertNu(SignatureVarElim)(ElemEntry)"
+             LetElemEntry {} => assert_total $ idris_crash "invertNu(SignatureVarElim)(LetElemEntry)"
 
     public export
     invert : Signature -> Omega -> Context -> Context -> SubstContext -> Typ -> M (Maybe Typ)
@@ -315,6 +329,8 @@ mutual
             case subst e (WkN $ 1 + length rest) of
              ElemEntry xi {} => xi
              LetElemEntry xi {} => xi
+             TypeEntry {} => assert_total $ idris_crash "invertNu(SignatureVarElim)(TypeEntry)"
+             LetTypeEntry {} => assert_total $ idris_crash "invertNu(SignatureVarElim)(LetTypeEntry)"
     invertNu sig omega ctx delta sigma (OmegaVarElim k tau) = MMaybe.do
       tau' <- invert sig omega sigma tau ctx delta getOmega
       return (OmegaVarElim k tau')
@@ -393,6 +409,7 @@ mutual
     occursNu sig omega (OmegaVarElim j sigma) k = return (j == k) `or` occurs sig omega sigma k
     occursNu sig omega (TyEqTy a b) k = occurs sig omega a k `or` occurs sig omega b k
     occursNu sig omega (ElEqTy a b ty) k = occurs sig omega a k `or` occurs sig omega b k `or` occurs sig omega ty k
+    occursNu sig omega (SignatureVarElim j sigma) k = occurs sig omega sigma k
 
     public export
     occurs : Signature -> Omega -> Typ -> OmegaName -> M Bool
@@ -711,6 +728,8 @@ namespace Type'
   -- El ? = 𝕌 type <=> ⊥
   unifyElAgainstRigid sig omega ctx el UniverseTy = M.do
     return (Disunifier "El ? = 𝕌 doesn't have solutions for ?")
+  unifyElAgainstRigid sig omega ctx el (SignatureVarElim {}) = M.do
+    return (Stuck "El ? = Xᵢ σ")
   unifyElAgainstRigid sig omega ctx el NatTy = M.do
     return (Success [ ElemConstraint ctx el NatTy UniverseTy] [] [])
   unifyElAgainstRigid sig omega ctx el (PiTy x dom cod) = M.do
@@ -1125,6 +1144,7 @@ progressElemMetaNu sig omega ctx idx (El x) = return (Stuck "No canonical Elem e
 progressElemMetaNu sig omega ctx idx (ContextSubstElim x y) = assert_total $ idris_crash "progressElemMetaNu(ContextSubstElim)"
 progressElemMetaNu sig omega ctx idx (SignatureSubstElim x y) = assert_total $ idris_crash "progressElemMetaNu(SignatureSubstElim)"
 progressElemMetaNu sig omega ctx idx (OmegaVarElim str x) = return (Stuck "No canonical Elem exists")
+progressElemMetaNu sig omega ctx idx (SignatureVarElim str x) = return (Stuck "No canonical Elem exists")
 
 progressMeta : Signature -> Omega -> OmegaName -> MetaBindingEntry -> UnifyM MetaProgress
 progressMeta sig omega idx (MetaType ctx _) = return (Stuck "Skipping Type meta")
diff --git a/src/idris/Nova/Surface/Elaboration.idr b/src/idris/Nova/Surface/Elaboration.idr
index d9a19a3..dc7cb6d 100644
--- a/src/idris/Nova/Surface/Elaboration.idr
+++ b/src/idris/Nova/Surface/Elaboration.idr
@@ -14,7 +14,7 @@ import Text.PrettyPrint.Prettyprinter
 import Nova.Core.Context
 import Nova.Core.Conversion
 import Nova.Core.Evaluation
-import Nova.Core.FreeVariable
+import Nova.Core.Occurrence
 import Nova.Core.Language
 import Nova.Core.Monad
 import Nova.Core.Name
@@ -452,7 +452,7 @@ mutual
         addSemanticToken (r0, BoundVarAnn)
         return (Success omega [ElemElimElaboration ctx vTm vTy es meta ty])
       Nothing =>
-        case lookupSignature sig x of
+        case lookupElemSignature sig x of
           Just ([<], idx, vTy) => M.do
             addSemanticToken (r0, ElimAnn)
             return (Success omega [ElemElimElaboration ctx (SignatureVarElim idx Terminal) vTy es meta ty])
@@ -608,12 +608,18 @@ mutual
         let omega = Elem.instantiateByElaboration omega meta (OmegaVarElim n (WkN (length ctx `minus` length regctxPrefix)))
         return (Success omega [])
   elabElemNu sig omega ctx (App r (Unfold r0 x) []) meta ty = M.do
-    case lookupLetSignature sig x of
+    case lookupLetElemSignature sig x of
       Just ([<], idx, vRhs, vTy) =>
         return (Success omega [ElemElimElaboration ctx ElEqVal (ElEqTy (SignatureVarElim idx Id) vRhs vTy) [] meta ty])
       Just (sigCtx, idx, vRhs, vTy) =>
         return (Error "Non-empty signature context not supported yet for signature name: \{x}")
-      Nothing => return (Error "Undefined signature name: \{x}")
+      Nothing =>
+        case lookupLetTypeSignature sig x of
+          Just ([<], idx, vRhs) =>
+            return (Success omega [ElemElimElaboration ctx TyEqVal (TyEqTy (SignatureVarElim idx Id) vRhs) [] meta ty])
+          Just (sigCtx, idx, vRhs) =>
+            return (Error "Non-empty signature context not supported yet for signature name: \{x}")
+          Nothing => return (Error "Undefined signature name: \{x}")
   elabElemNu sig omega ctx (App r (Unfold r0 x) _) meta ty = M.do
     return (Error "!\{x} applied to a wrong number of arguments")
   -- Π-β A (x. B) (x. f) e : (x ↦ f) e ≡ f[e/x] ∈ B[e/x]
@@ -856,9 +862,29 @@ mutual
   elabType sig omega ctx (SigmaVal r a b) meta =
     return (Error "(_, _) is not a type")
   elabType sig omega ctx tm@(App r (Var r0 x) es) meta = M.do
-    (omega, t') <- liftUnifyM $ newElemMeta omega ctx UniverseTy SolveByElaboration
-    let omega = Typ.instantiateByElaboration omega meta (El (OmegaVarElim t' Id))
-    return (Success omega [ElemElaboration ctx tm t' UniverseTy])
+    case (lookupTypeSignature sig x, es) of
+      (Just ([<], idx), []) => M.do
+        addSemanticToken (r0, ElimAnn)
+        let omega = Typ.instantiateByElaboration omega meta (SignatureVarElim idx Terminal)
+        return (Success omega [])
+      (Just ([<], idx), _ :: _) => M.do
+        return (Error "Type variable \{x} applied to a spine")
+      (Just (_ :< _, idx), _) =>
+        return (Error "Non-empty signature context not supported yet for name: \{x}")
+      (Nothing, es) =>
+        case (lookup x omega, es) of
+          (Just (LetType [<] _), []) => M.do
+            addSemanticToken (r0, ElimAnn)
+            let omega = Typ.instantiateByElaboration omega meta (OmegaVarElim x Terminal)
+            return (Success omega [])
+          (Just (LetType (_ :< _) _), _) => M.do
+            return (Error "Non-empty signature context not supported yet for name: \{x}")
+          (Just (LetType [<] _), _ :: _) => M.do
+            return (Error "Type variable \{x} applied to a spine")
+          _ => M.do
+           (omega, t') <- liftUnifyM $ newElemMeta omega ctx UniverseTy SolveByElaboration
+           let omega = Typ.instantiateByElaboration omega meta (El (OmegaVarElim t' Id))
+           return (Success omega [ElemElaboration ctx tm t' UniverseTy])
   elabType sig omega ctx (App r (OneVal x) _) meta = M.do
     return (Error "() is not a type")
   elabType sig omega ctx (App r (NatVal0 x) _) meta = M.do
@@ -1042,6 +1068,7 @@ mutual
       (omega, ty) <- applyRewrite sig omega gamma ty pty prf direct
       return (omega, ElEqTy a b ty)
     applyRewriteNu sig omega gamma (ElEqTy a b ty) p prf direct = error (range p, "Failing at _ ≡ _ ∈ _")
+    applyRewriteNu sig omega gamma (SignatureVarElim k sigma) p prf direct = error (range p, "Failing at Xᵢ")
 
     public export
     applyRewrite : Params => Signature -> Omega -> Context -> Typ -> OpFreeTerm -> SurfaceTerm -> Bool -> ElabM (Either (Range, Doc Ann) (Omega, Typ))
@@ -1552,6 +1579,27 @@ elabTopLevelEntry sig omega (DefineSignature r x ty rhs) = M.do
     | Error omega (Right (con, err)) => return (Left (UnificationError omega (con, err)))
   let omega = insert (x, LetElem [<] (OmegaVarElim rhs' Id) (OmegaVarElim ty' Id)) omega
   return (Right (sig, omega))
+elabTopLevelEntry sig omega (LetTypeSignature r x rhs) = M.do
+  print_ Debug STDOUT "Elaborating \{x}"
+  (omega, rhs') <- liftUnifyM $ newTypeMeta omega [<] SolveByElaboration
+  let probs = [TypeElaboration [<] rhs rhs']
+  Success omega <- solve sig omega probs
+    | Stuck omega stuckElab stuckCons => return (Left (Stuck omega stuckElab stuckCons))
+    | Error omega (Left (elab, err)) => return (Left (ElaborationError omega (elab, err)))
+    | Error omega (Right (con, err)) => return (Left (UnificationError omega (con, err)))
+  let sig = sig :< (x, LetTypeEntry [<] (OmegaVarElim rhs' Id))
+  let omega = subst omega Wk
+  return (Right (sig, omega))
+elabTopLevelEntry sig omega (DefineTypeSignature r x rhs) = M.do
+  print_ Debug STDOUT "Elaborating \{x}"
+  (omega, rhs') <- liftUnifyM $ newTypeMeta omega [<] SolveByElaboration
+  let probs = [TypeElaboration [<] rhs rhs']
+  Success omega <- solve sig omega probs
+    | Stuck omega stuckElab stuckCons => return (Left (Stuck omega stuckElab stuckCons))
+    | Error omega (Left (elab, err)) => return (Left (ElaborationError omega (elab, err)))
+    | Error omega (Right (con, err)) => return (Left (UnificationError omega (con, err)))
+  let omega = insert (x, LetType [<] (OmegaVarElim rhs' Id)) omega
+  return (Right (sig, omega))
 
 public export
 elabFile : Params
@@ -1575,6 +1623,18 @@ elabFile sig omega ops (LetSignature r x ty rhs ::: []) = M.do
   Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (LetSignature r x ty rhs))
     | Left err => return (Left (x, r, sig, err))
   return (Right (sig, omega, ops))
+elabFile sig omega ops (LetTypeSignature r x rhs ::: []) = M.do
+  Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (LetTypeSignature r x rhs))
+    | Left err => return (Left (x, r, sig, err))
+  return (Right (sig, omega, ops))
+elabFile sig omega ops (DefineTypeSignature r x rhs ::: []) = M.do
+  Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (DefineTypeSignature r x rhs))
+    | Left err => return (Left (x, r, sig, err))
+  return (Right (sig, omega, ops))
+elabFile sig omega ops (DefineSignature r x ty rhs ::: []) = M.do
+  Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (DefineSignature r x ty rhs))
+    | Left err => return (Left (x, r, sig, err))
+  return (Right (sig, omega, ops))
 elabFile sig omega ops (Syntax r op ::: e' :: es) = M.do
   elabFile sig omega (ops :< op) (e' ::: es)
 elabFile sig omega ops (TypingSignature r x ty ::: e' :: es) = M.do
@@ -1587,11 +1647,15 @@ elabFile sig omega ops (LetSignature r x ty rhs ::: e' :: es) = M.do
   Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (LetSignature r x ty rhs))
     | Left err => return (Left (x, r, sig, err))
   elabFile sig omega ops (e' ::: es)
-elabFile sig omega ops (DefineSignature r x ty rhs ::: []) = M.do
-  Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (DefineSignature r x ty rhs))
+elabFile sig omega ops (LetTypeSignature r x rhs ::: e' :: es) = M.do
+  Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (LetTypeSignature r x rhs))
     | Left err => return (Left (x, r, sig, err))
-  return (Right (sig, omega, ops))
+  elabFile sig omega ops (e' ::: es)
 elabFile sig omega ops (DefineSignature r x ty rhs ::: e' :: es) = M.do
   Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (DefineSignature r x ty rhs))
     | Left err => return (Left (x, r, sig, err))
   elabFile sig omega ops (e' ::: es)
+elabFile sig omega ops (DefineTypeSignature r x rhs ::: e' :: es) = M.do
+  Right (sig, omega) <- elabTopLevelEntry sig omega !(liftMEither $ shuntTopLevel (cast ops) (DefineTypeSignature r x rhs))
+    | Left err => return (Left (x, r, sig, err))
+  elabFile sig omega ops (e' ::: es)
diff --git a/src/idris/Nova/Surface/Language.idr b/src/idris/Nova/Surface/Language.idr
index 210f318..108512c 100644
--- a/src/idris/Nova/Surface/Language.idr
+++ b/src/idris/Nova/Surface/Language.idr
@@ -20,7 +20,7 @@ import Nova.Surface.Operator
 -- e⁺{1} = e{≥3} | (e⁺{≥0}) | .π₁ | .π₂ | {e{≥0}}
 -- ē⁺ ::= ␣ e⁺{1} ē⁺ | ·
 
--- top-level ::= assume x : e{≥0} | let x : e{≥0} ≔ e{≥0} | define x : e{≥0} ≔ e{≥0}
+-- top-level ::= assume x : e{≥0} | let x : e{≥0} ≔ e{≥0} | define x : e{≥0} ≔ e{≥0} | let-type x ≔ e{≥0} | define-type x ≔ e{≥0}
 
 
 mutual
@@ -127,7 +127,7 @@ mutual
       RewriteInv : Range -> Term -> Term -> Tactic
       ||| rewrite e{≥4} e{≥4}
       Rewrite : Range -> Term -> Term -> Tactic
-      ||| Let x ≔ e{≥0}
+      ||| let x ≔ e{≥0}
       Let : Range -> VarName -> Term -> Tactic
 
   namespace OpFreeTactic
@@ -337,6 +337,10 @@ namespace Term
     DefineSignature : Range -> VarName -> Term -> Term -> TopLevel
     ||| syntax ... : ...
     Syntax : Range -> Operator -> TopLevel
+    ||| let-type x ≔ t
+    LetTypeSignature : Range -> VarName -> Term -> TopLevel
+    ||| define-type x ≔ t
+    DefineTypeSignature : Range -> VarName -> Term -> TopLevel
 
 namespace OpFreeTerm
   public export
@@ -349,6 +353,10 @@ namespace OpFreeTerm
     ||| define x : T
     |||          ≔ t
     DefineSignature : Range -> VarName -> OpFreeTerm -> OpFreeTerm -> OpFreeTopLevel
+    ||| let-type x ≔ t
+    LetTypeSignature : Range -> VarName -> OpFreeTerm -> OpFreeTopLevel
+    ||| define-type x ≔ t
+    DefineTypeSignature : Range -> VarName -> OpFreeTerm -> OpFreeTopLevel
 
 covering
 public export
@@ -361,6 +369,10 @@ Show TopLevel where
     "define \{x} : \{show ty} ≔ \{show rhs}"
   show (Syntax r op) =
     "syntax ..."
+  show (LetTypeSignature r x rhs) =
+    "let-type \{x} ≔ \{show rhs}"
+  show (DefineTypeSignature r x rhs) =
+    "define-type \{x} ≔ \{show rhs}"
 
 covering
 public export
@@ -371,6 +383,10 @@ Show OpFreeTopLevel where
     "let \{x} : \{show ty} ≔ \{show rhs}"
   show (DefineSignature r x ty rhs) =
     "define \{x} : \{show ty} ≔ \{show rhs}"
+  show (LetTypeSignature r x rhs) =
+    "let-type \{x} ≔ \{show rhs}"
+  show (DefineTypeSignature r x rhs) =
+    "define-type \{x} ≔ \{show rhs}"
 
 namespace OpFreeTerm
   public export
diff --git a/src/idris/Nova/Surface/Parser.idr b/src/idris/Nova/Surface/Parser.idr
index 13e9b8a..34a7ae3 100644
--- a/src/idris/Nova/Surface/Parser.idr
+++ b/src/idris/Nova/Surface/Parser.idr
@@ -546,6 +546,33 @@ mutual
     rhs <- located (term 0)
     pure (DefineSignature (l + fst rhs) (snd x) ty (snd rhs))
 
+  public export
+  letTypeSignature : Rule TopLevel
+  letTypeSignature = do
+    l <- delim "let-type"
+    commit
+    spaceDelim
+    x <- located var
+    appendSemanticToken (fst x, ElimAnn)
+    spaceDelim
+    delim_ "≔"
+    spaceDelim
+    rhs <- located (term 0)
+    pure (LetTypeSignature (l + fst rhs) (snd x) (snd rhs))
+
+  public export
+  defineTypeSignature : Rule TopLevel
+  defineTypeSignature = do
+    l <- delim "define-type"
+    commit
+    spaceDelim
+    x <- located var
+    appendSemanticToken (fst x, ElimAnn)
+    spaceDelim
+    delim_ "≔"
+    spaceDelim
+    rhs <- located (term 0)
+    pure (DefineTypeSignature (l + fst rhs) (snd x) (snd rhs))
 
   namespace TopLevel
     public export
@@ -611,7 +638,7 @@ mutual
 
   public export
   topLevel : Rule TopLevel
-  topLevel = typingSignature <|> letSignature <|> defineSignature <|> syntax
+  topLevel = typingSignature <|> letTypeSignature <|> defineTypeSignature <|> letSignature <|> defineSignature <|> syntax
 
   public export
   surfaceFile : Rule (List1 TopLevel)
diff --git a/src/idris/Nova/Surface/Shunting.idr b/src/idris/Nova/Surface/Shunting.idr
index eada86c..75f224f 100644
--- a/src/idris/Nova/Surface/Shunting.idr
+++ b/src/idris/Nova/Surface/Shunting.idr
@@ -318,4 +318,10 @@ mutual
     ty <- shunt ops ty 0
     rhs <- shunt ops rhs 0
     return (DefineSignature r x ty rhs)
+  shuntTopLevel ops (LetTypeSignature r x rhs) = MEither.do
+    rhs <- shunt ops rhs 0
+    return (LetTypeSignature r x rhs)
+  shuntTopLevel ops (DefineTypeSignature r x rhs) = MEither.do
+    rhs <- shunt ops rhs 0
+    return (DefineTypeSignature r x rhs)
   shuntTopLevel ops (Syntax x y) = error "Trying to shunt a syntax definition"
diff --git a/src/idris/Nova/Surface/Tactic/Unfold.idr b/src/idris/Nova/Surface/Tactic/Unfold.idr
index 2c872ae..2108f9c 100644
--- a/src/idris/Nova/Surface/Tactic/Unfold.idr
+++ b/src/idris/Nova/Surface/Tactic/Unfold.idr
@@ -57,6 +57,23 @@ mutual
     applyUnfoldNu sig omega ctx (ElEqTy a b ty) (ElEqTy _ pa pb pty) = MEither.do
       return (ElEqTy !(applyUnfold sig omega ctx a pa) !(applyUnfold sig omega ctx b pb) !(applyUnfold sig omega ctx ty pty))
     applyUnfoldNu sig omega ctx (ElEqTy a b ty) p = error (range p)
+    applyUnfoldNu sig omega ctx tm@(SignatureVarElim x subst) (App r (Var _ y) []) = MEither.do
+      case !(liftM $ conv sig omega subst Terminal) of
+        True =>
+          case lookupSignature sig x of
+            Just (x, _) =>
+              case x == y of
+                True => return tm
+                False => error r
+            Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+        False => error r
+    applyUnfoldNu sig omega ctx tm@(SignatureVarElim x sigma) (App r (Box _) []) = MEither.do
+      case lookupSignature sig x of
+        Just (x, LetTypeEntry ctx rhs) =>
+          return (ContextSubstElim rhs sigma)
+        Just (x, _) => error r
+        Nothing => throw "applyUnfoldNu(SignatureVarElim)"
+    applyUnfoldNu sig omega ctx (SignatureVarElim x sigma) p = error (range p)
 
     public export
     applyUnfold : Signature -> Omega -> SnocList VarName -> Typ -> OpFreeTerm -> M (Either Range Typ)
diff --git a/src/nova/Test.nova b/src/nova/Test.nova
index 93157e7..997393e 100644
--- a/src/nova/Test.nova
+++ b/src/nova/Test.nova
@@ -266,6 +266,21 @@ define ℕ-left-cancel : (x y z : ℕ) → (x + y ≡ x + z ∈ ℕ) → (y ≡
                        )
                        x p
 
+define plus-assoc : (x y z : ℕ) → x + (y + z) ≡ (x + y) + z ∈ ℕ
+                  ≔ x y z ↦ ℕ-elim (y. x + (y + z) ≡ (x + y) + z ∈ ℕ)
+                      -- x + z = x + z
+                      (tac rewrite⁻¹ (_ ☐ ≡ _ ∈ _) (plus-left-Z ?);
+                           rewrite⁻¹ (_ ≡ _ ☐ _ ∈ _) (plus-right-Z ?);
+                           exact Refl;
+                      )
+                      (y. H.
+                        tac rewrite⁻¹ (_ ☐ ≡ _ ∈ _) (plus-left-S ? ?);
+                            rewrite⁻¹ (☐ ≡ _ ∈ _) (plus-right-S ? ?);
+                            rewrite⁻¹ (_ ≡ _ ☐ _ ∈ _) (plus-right-S ? ?);
+                            rewrite⁻¹ (_ ≡ ☐ ∈ _) (plus-left-S ? ?);
+                            exact cong (x ↦ S x) H;
+                      )
+                      y
 
 -- [] ++ ys = ys
 -- (x :: xs) ++ ys = x :: (xs ++ ys)
@@ -360,3 +375,26 @@ let _∘_ : {A B C : 𝕌} → (B → C) → (A → B) → (A → C)
 
 let _≅_ : 𝕌 → 𝕌 → 𝕌
         ≔ A B ↦ (f : A → B) ⨯ (g : B → A) ⨯ (g ∘ f ≡ id ∈ ?) ⨯ (f ∘ g ≡ id ∈ ?)
+
+let-type Monoid
+     ≔ (A : 𝕌)
+         ⨯ (z : A)
+         ⨯ (_+_ : A → A → A)
+         ⨯ ((x : A) → z + x ≡ x ∈ A)
+         ⨯ ((x : A) → x + z ≡ x ∈ A)
+         ⨯ ((x y z : A) → x + (y + z) ≡ (x + y) + z ∈ A)
+
+let-type Commut-Monoid
+     ≔ (A : 𝕌)
+         ⨯ (z : A)
+         ⨯ (_+_ : A → A → A)
+         ⨯ ((x : A) → z + x ≡ x ∈ A)
+         ⨯ ((x : A) → x + z ≡ x ∈ A)
+         ⨯ ((x y z : A) → x + (y + z) ≡ (x + y) + z ∈ A)
+         ⨯ ((x y : A) → x + y ≡ y + x ∈ A)
+
+define ℕ-Monoid : Monoid
+                ≔ tac unfold ☐; exact ℕ, Z, _+_ , plus-left-Z, plus-right-Z, plus-assoc;
+
+define ℕ-Commut-Monoid : Commut-Monoid
+                ≔ tac unfold ☐; exact ℕ, Z, _+_ , plus-left-Z, plus-right-Z, plus-assoc, plus-commut;
diff --git a/src/text/Internals/NovaFoundation.txt b/src/text/Internals/NovaFoundation.txt
index 33e5242..d371be4 100644
--- a/src/text/Internals/NovaFoundation.txt
+++ b/src/text/Internals/NovaFoundation.txt
@@ -95,6 +95,15 @@ We have:
 
 ///////// Inference rules (sig entry) //////////
 
+Σ sig
+--------------------
+Σ ⊦ (Γ ⊦ type) entry
+
+Σ sig
+Σ Γ ⊦ A type
+----------------------
+Σ ⊦ (Γ ⊦ A type) entry
+
 Σ sig
 Σ Γ ⊦ A type
 -----------------
@@ -113,6 +122,8 @@ We have:
 Σ₀ ⊦ E(σ) entry
      (Γ ⊦ A)(σ) = Γ(σ) ⊦ A(σ)
      (Γ ⊦ a : A)(σ) = Γ(σ) ⊦ a(σ) : A(σ)
+     (Γ ⊦ type)(σ) = Γ(σ) ⊦ type
+     (Γ ⊦ A type)(σ) = Γ(σ) ⊦ A(σ) type
 
 ///////// Inference rules (sig entry instance) //////////
 
@@ -122,18 +133,30 @@ We have:
 -----------------
 Σ ⊦ γ.a : (Γ ⊦ A)
 
+Σ sig
+Σ Γ ⊦ A type
+--------------------
+Σ ⊦ γ.A : (Γ ⊦ type)
+
 Σ sig
 Σ Γ ⊦ a : A
 -------------------
 Σ ⊦ _ : (Γ ⊦ a : A)
 
+Σ sig
+Σ Γ ⊦ A type
+--------------------
+Σ ⊦ _ : (Γ ⊦ A type)
+
 Σ₁ ⊦ E entry
 Σ₁ ⊦ e : E
 σ : Σ₀ ⇒ Σ₁
 --------------------------------------- //Defined by meta-level induction
 Σ₀ ⊦ e(σ) : E(σ)
      (γ.a)(σ) = γ. a(σ) : (Γ(σ) ⊦ A(σ))
+     (γ.A)(σ) = γ. A(σ) : (Γ(σ) ⊦ type)
      _(σ) = _ : (Γ(σ) ⊦ a(σ) : A(σ))
+     _(σ) = _ : (Γ(σ) ⊦ A(σ) type)
 
 ///////// Inference rules (sig substitution) //////////
 
@@ -387,6 +410,9 @@ id ∘ σ = σ : Σ₀ ⇒ Σ₁
 -------------------------------
 Σ Ξ ⊦ A(σ)(τ) = A(σ ∘ τ) type
 
+Σ (Γ ⊦ X : type) Γ ⊦ X type
+
+Σ (Γ ⊦ X ≔ A : type) Γ ⊦ X type
 
 ///////// Inference rules (tel) //////////
 
@@ -490,6 +516,9 @@ id ∘ σ = σ : Σ₀ ⇒ Σ₁
 -----------------------
 Σ (Γ ⊦ x : A) Γ ⊦ x : A
 
+---------------------------
+Σ (Γ ⊦ x ≔ a : A) Γ ⊦ x : A
+
 Σ Γ ⊦ t : A
 Σ ⊦ σ : Δ ⇒ Γ
 -----------------