start of type stuff

old: (1 | 1 | x : A) ->
new: (x @ 1, 1 : A) ->

src/Quox.idr

@@ -11,11 +11,11 @@ export
 tm : Term 1 2
 tm =
   (Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
-    `DCloT` (DOne ::: id))
+    `DCloT` (K One ::: id))
     `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
 
 main : IO Unit
 main = do
   prettyTerm tm
   prettyTerm $ pushSubstsT tm
-  putStrLn ":qtuwu:"
+  putStrLn "\n:qtuwu:"

src/Quox/Context.idr

@@ -22,7 +22,7 @@ data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
 %name Telescope tel
 
 public export
-Telescope' : Type -> (from, to : Nat) -> Type
+Telescope' : (a : Type) -> (from, to : Nat) -> Type
 Telescope' a = Telescope (\_ => a)
 
 ||| a global context is actually just a telescope over no existing bindings
@@ -31,30 +31,30 @@ Context : (tm : Nat -> Type) -> (len : Nat) -> Type
 Context tm len = Telescope tm 0 len
 
 public export
-Context' : Type -> (len : Nat) -> Type
+Context' : (a : Type) -> (len : Nat) -> Type
 Context' a = Context (\_ => a)
 
 
 export
-toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
+toSnocList : Telescope {tm, _} -> SnocList (Exists tm)
 toSnocList [<]        = [<]
 toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
 
 private
-toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
+toListAcc : Telescope {tm, _} -> List (Exists tm) -> List (Exists tm)
 toListAcc [<]        acc = acc
 toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
 
 export %inline
-toList : Telescope tm _ _ -> List (Exists tm)
+toList : Telescope {tm, _} -> List (Exists tm)
 toList tel = toListAcc tel []
 
 export %inline
-toSnocList' : Telescope' a _ _ -> SnocList a
+toSnocList' : Telescope' {a, _} -> SnocList a
 toSnocList' = map snd . toSnocList
 
 export %inline
-toList' : Telescope' a _ _ -> List a
+toList' : Telescope' {a, _} -> List a
 toList' = map snd . toList
 
 
@@ -65,15 +65,20 @@ tel1 . [<]         = tel1
 tel1 . (tel2 :< s) = (tel1 . tel2) :< s
 
 
-export
-getWith : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
-getWith (ctx :< t) VZ     th = t // drop1 th
-getWith (ctx :< t) (VS i) th = getWith ctx i (drop1 th)
+public export
+getShift : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
+getShift (ctx :< t) VZ     by = t // drop1 by
+getShift (ctx :< t) (VS i) by = getShift ctx i (drop1 by)
 
 infixl 8 !!
-export %inline
+public export %inline
 (!!) : CanShift tm => Context tm len -> Var len -> tm len
-ctx !! i = getWith ctx i SZ
+ctx !! i = getShift ctx i SZ
+
+infixl 8 !?
+public export %inline
+(!?) : Context' tm len -> Var len -> tm
+ctx !? i = (ctx !! i) @{Const}
 
 
 ||| a triangle of bindings. each type binding in a context counts the ues of
@@ -88,7 +93,7 @@ Triangle' a = Context $ Context (\_ => a)
 
 export
 0 telescopeLTE : Telescope _ from to -> from `LTE` to
-telescopeLTE [<]        = reflexive {rel=LTE}
+telescopeLTE [<]        = reflexive {rel=Nat.LTE}
 telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
 
 export
@@ -97,7 +102,7 @@ export
 
 export %hint
 0 succGT : S n `GT` n
-succGT = LTESucc $ reflexive {rel=LTE}
+succGT = LTESucc $ reflexive {rel=Nat.LTE}
 
 
 parameters {auto _ : Applicative f}
@@ -173,36 +178,41 @@ zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
 
 
 export
-lengthPrf : Telescope _ from to -> Subset Nat $ \len => len + from = to
-lengthPrf [<]        = Element 0 Refl
-lengthPrf (tel :< _) = let len = lengthPrf tel in
-                       Element (S len.fst) (cong S len.snd)
+lengthPrf : Telescope _ from to -> (len : Nat ** len + from = to)
+lengthPrf [<]        = (0 ** Refl)
+lengthPrf (tel :< _) =
+  let len = lengthPrf tel in (S len.fst ** cong S len.snd)
+
+export
+lengthPrf0 : Context _ to -> (len : Nat ** len = to)
+lengthPrf0 ctx =
+  let (len ** prf) = lengthPrf ctx in
+  (len ** rewrite sym $ plusZeroRightNeutral len in prf)
 
 public export %inline
 length : Telescope {} -> Nat
 length = fst . lengthPrf
 
 
-parameters {0 acc : Nat -> Type}
-  export
-  foldl : (forall m, n. acc m -> tm n -> acc (S m)) ->
-          acc 0 -> (tel : Telescope tm from to) -> acc (length tel)
-  foldl f z [<]        = z
-  foldl f z (tel :< t) = f (foldl f z tel) t
+export
+foldl : {0 acc : Nat -> Type} ->
+        (f : forall n. acc n -> tm (n + from) -> acc (S n)) ->
+        (z : acc 0) -> (tel : Telescope tm from to) -> acc (length tel)
+foldl f z [<]        = z
+foldl f z (tel :< t) = f (foldl f z tel) (rewrite (lengthPrf tel).snd in t)
 
-parameters {auto _ : Monoid a}
-  export %inline
-  foldMap : (forall n. tm n -> a) -> Telescope tm from to -> a
-  foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
+export %inline
+foldMap : Monoid a => (forall n. tm n -> a) -> Telescope tm from to -> a
+foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
 
-  export %inline
-  fold : Telescope' a from to -> a
-  fold = foldMap id
+export %inline
+fold : Monoid a => Telescope' a from to -> a
+fold = foldMap id
 
-  ||| like `fold` but calculate the elements only when actually appending
-  export %inline
-  foldLazy : Telescope' (Lazy a) from to -> a
-  foldLazy = foldMap force
+||| like `fold` but calculate the elements only when actually appending
+export %inline
+foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
+foldLazy = foldMap force
 
 
 export %inline

src/Quox/Error.idr

@@ -12,8 +12,8 @@ import Control.Monad.RWS
 %default total
 
 
-||| a representation of a list's length. this is used in the `Ord` instance to
-||| transform the `Ord` constraints into `Eq`s
+||| a representation of a list's length. this is used in `implyAll` to transform
+||| the constraints one by one
 public export
 data Spine : List a -> Type where
   NIL  : Spine []
@@ -37,13 +37,12 @@ Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
 
 export %inline
 inj : ty `Elem` tys => ty -> OneOf tys
-inj value = One %search value
+inj @{elem} value = One {elem, value}
 
 ||| `All p types` computes a constraint for `p a` for each `a` in `types`
 public export
 All : (Type -> Type) -> List Type -> Type
-All p []      = ()
-All p (x::xs) = (p x, All p xs)
+All p = foldr (,) () . map p
 
 
 private
@@ -51,24 +50,28 @@ eq : All Eq types => OneOf types -> OneOf types -> Bool
 eq (One Here      x) (One Here      y) = x == y
 eq (One (There p) x) (One (There q) y) = eq (One p x) (One q y)
 eq (One Here      _) (One (There _) _) = False
-eq (One (There z) x) (One Here      y) = False
+eq (One (There _) _) (One Here      _) = False
 
 export %inline
 All Eq types => Eq (OneOf types) where (==) = eq
 
 
-private
-ordsToEqs : Spine types => All Ord types => All Eq types
-ordsToEqs @{NIL}     = ()
-ordsToEqs @{CONS tl} = (%search, ordsToEqs @{tl})
+export
+implyAll : (0 c, d : Type -> Type) ->
+           (forall a. c a -> d a) => Spine types => All c types => All d types
+implyAll c d @{q} @{spine} @{ps} = go spine ps where
+  go : forall types. Spine types -> All c types -> All d types
+  go NIL       _       = ()
+  go (CONS tl) (p, ps) = (q p, go tl ps)
+
 
 private %inline
 [eqOrds] (Spine types, All Ord types) => Eq (OneOf types) where
-  (==) = eq @{ordsToEqs}
+  (==) = eq @{implyAll Ord Eq}
 
 
 private
-cmp : All Ord types => OneOf types -> OneOf types -> Ordering
+cmp : All Ord types => (x, y : OneOf types) -> Ordering
 cmp (One Here      x) (One Here      y) = compare x y
 cmp (One Here      _) (One (There _) _) = LT
 cmp (One (There _) _) (One Here      _) = GT
@@ -79,11 +82,12 @@ export %inline
   compare = cmp
 
 
-private shw : All Show types => Prec -> OneOf types -> String
-shw d (One Here      value) = showPrec d value
-shw d (One (There p) value) = shw d $ One p value
-
-export %inline All Show types => Show (OneOf types) where showPrec = shw
+export %inline
+All Show types => Show (OneOf types) where
+  showPrec d = go where
+    go : forall types. All Show types => OneOf types -> String
+    go (One Here      value) = showPrec d value
+    go (One (There p) value) = go $ One p value
 
 
 public export
@@ -122,7 +126,7 @@ without' (y :: xs) (There p) = y :: without' xs p
 infix 9 `without`
 export %inline
 without : (xs : List a) -> (x : a) -> x `Elem` xs => List a
-xs `without` x = without' {x} xs %search
+(xs `without` x) @{e} = without' xs e
 
 
 private
@@ -135,7 +139,7 @@ get' (There y) (One (There p) x) = mapSnd {elem $= There} $ get' y (One p x)
 export %inline
 get : (0 err : Type) -> err `Elem` errs =>
       OneOf errs -> Either err (OneOf (errs `without` err))
-get _ = get' %search
+get _ @{e} = get' e
 
 
 export %inline
@@ -153,14 +157,12 @@ data Embed : List a -> List a -> Type where
   (::) : x `Elem` ys -> Embed xs ys -> Embed (x::xs) ys
 
 
-private
-embedElem' : Embed xs ys -> x `Elem` xs -> x `Elem` ys
-embedElem' (e :: _)  Here      = e
-embedElem' (_ :: es) (There p) = embedElem' es p
-
 export %inline
 embedElem : Embed xs ys => x `Elem` xs -> x `Elem` ys
-embedElem = embedElem' %search
+embedElem @{emb} = go emb where
+  go : forall xs. Embed xs ys -> x `Elem` xs -> x `Elem` ys
+  go (e :: _)  Here      = e
+  go (_ :: es) (There p) = go es p
 
 
 export %inline
@@ -205,7 +207,7 @@ implementation
   (Monad m, Embed errs1 errs2) =>
   MonadEmbed (ErrorT errs1 m) (ErrorT errs2 m)
 where
-  embed (MkErrorT act) = MkErrorT $ mapFst {elem $= embedElem} <$> act
+  embed (MkErrorT act) = MkErrorT $ act <&> mapFst {elem $= embedElem}
 
 
 export %inline

src/Quox/Eval.idr

@@ -1,130 +0,0 @@
-module Quox.Eval
-
--- todo list:
--- - understand nbe and use it
--- - take a proof of well-typedness as an argument,
---   to reduce the number of eithers
--- - remove the either if possible (should be???)
-
-import Quox.Syntax
-import Quox.Context
-
-import Data.DPair
-import Data.SortedMap
-
-%default total
-
-
-public export
-record Global where
-  constructor G
-  val : forall d, n. NotCloElim d n
-
-public export Globals : Type
-Globals = SortedMap Name Global
-
-export (!!) : Globals -> Name -> Maybe (Elim d n)
-gs !! x = map (\g => g.val.fst) $ lookup x gs
-  -- just `map (fst . val)` fails?
-
-
-mutual
-  public export isValue : Term d n -> Bool
-  isValue (TYPE {})          = True
-  isValue (Pi {arg, res, _}) = isValue arg && isValue res
-  isValue (Lam {body, _})    = isValue body
-  isValue (E e)              = isNeutral e
-  isValue (CloT  {})         = False
-  isValue (DCloT {})         = False
-
-  public export isNeutral : Elim d n -> Bool
-  isNeutral (F {})       = False
-  isNeutral (B {})       = True
-  isNeutral (fun :@ arg) = isNeutral fun && isValue arg
-  isNeutral (_ :# _)     = False
-  isNeutral (CloE {})    = False
-  isNeutral (DCloE {})   = False
-
-public export IsValue : Term d n -> Type
-IsValue = So . isValue
-
-public export IsNeutral : Elim d n -> Type
-IsNeutral = So . isNeutral
-
-public export Value : Nat -> Nat -> Type
-Value d n = Subset (Term d n) IsValue
-
-public export Neutral : Nat -> Nat -> Type
-Neutral d n = Subset (Elim d n) IsNeutral
-
-public export valT : (t : Term d n) -> (0 _ : IsValue t) => Value d n
-valT t = Element t %search
-
-public export neuE : (e : Elim d n) -> (0 _ : IsNeutral e) => Neutral d n
-neuE e = Element e %search
-
-
-data EvalError =
-    NotInScope Name
-  | NonFunction SomeElim
-
-
-parameters (globals : Globals)
-  mutual
-    export covering %inline
-    evalT : Term d n -> Either EvalError (Value d n)
-    evalT = uncurry evalT' . pushSubstsT
-
-    export covering %inline
-    evalE : Elim d n -> Either EvalError (Neutral d n)
-    evalE = uncurry evalE' . pushSubstsE
-
-    export covering
-    evalT' : (t : Term d n) -> (0 prf : IsNotCloT t) ->
-             Either EvalError (Value d n)
-
-    export covering
-    evalE' : (e : Elim d n) -> (0 prf : IsNotCloE e) ->
-             Either EvalError (Neutral d n)
-
-
-public export
-data AlphaResult =
-    Ok
-  | Clash  SomeTerm SomeTerm
-  | DClash SomeDim  SomeDim
-  | QClash Qty      Qty
-
-export
-Semigroup AlphaResult where
-  Ok  <+> res = res
-  res <+> _   = res
-
-export Monoid AlphaResult where neutral = Ok
-
-private %inline clash : Term d1 n1 -> Term d2 n2 -> AlphaResult
-clash s t = Clash (some2 s) (some2 t)
-
-
-||| check two quantities are exactly equal and fail if not
-export %inline
-alphaQ : (pi, rh : Qty) -> AlphaResult
-alphaQ pi rh = if pi == rh then Ok else QClash pi rh
-
-export %inline
-alphaD : (al, be : Dim d) -> AlphaResult
-alphaD al be = if al == be then Ok else DClash (some al) (some be)
-
-mutual
-  private
-  alphaT : (s, t : Term d n) -> AlphaResult
-
-  private
-  alphaE : (e, f : Elim d n) -> AlphaResult
-
-
-export %inline alphaV : (u, v : Value d n) -> AlphaResult
-alphaV u v = alphaT u.fst v.fst
-
-export %inline alphaN : (p, q : Neutral d n) -> AlphaResult
-alphaN p q = alphaE p.fst q.fst

src/Quox/Syntax.idr

@@ -1,6 +1,7 @@
 module Quox.Syntax
 
 import public Quox.Syntax.Dim
+import public Quox.Syntax.DimEq
 import public Quox.Syntax.Qty
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst

src/Quox/Syntax/Dim.idr

@@ -7,26 +7,44 @@ import Quox.Pretty
 %default total
 
 
+public export
+data DimConst = Zero | One
+%name DimConst e
+
+private DCRepr : Type
+DCRepr = Nat
+
+private %inline dcrepr : DimConst -> DCRepr
+dcrepr e = case e of Zero => 0; One => 1
+
+export Eq  DimConst where (==) = (==) `on` dcrepr
+export Ord DimConst where compare = compare `on` dcrepr
+
+
 public export
 data Dim : Nat -> Type where
-  DZero, DOne : Dim d
-  DBound : Var d -> Dim d
+  K : DimConst -> Dim d
+  B : Var d -> Dim d
 %name Dim.Dim p, q
 
 private DRepr : Type
 DRepr = Nat
 
 private %inline drepr : Dim n -> DRepr
-drepr d = case d of DZero => 0; DOne => 1; DBound i => 2 + i.nat
+drepr p = case p of K i => dcrepr i; B i => 2 + i.nat
 
 export Eq  (Dim n) where (==) = (==) `on` drepr
 export Ord (Dim n) where compare = compare `on` drepr
 
+export
+PrettyHL DimConst where
+  prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0"
+  prettyM One  = hl Dim <$> ifUnicode "𝟭" "1"
+
 export
 PrettyHL (Dim n) where
-  prettyM DZero      = hl Dim <$> ifUnicode "𝟬" "0"
-  prettyM DOne       = hl Dim <$> ifUnicode "𝟭" "1"
-  prettyM (DBound i) = prettyVar DVar DVarErr (!ask).dnames i
+  prettyM (K e) = prettyM e
+  prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i
 
 
 public export
@@ -41,10 +59,14 @@ prettyDSubst th =
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
 
 
-export FromVar Dim where fromVar = DBound
+export FromVar Dim where fromVar = B
+
+export
+CanShift Dim where
+  K e // _  = K e
+  B i // by = B (i // by)
 
 export
 CanSubst Dim Dim where
-  DZero    // _  = DZero
-  DOne     // _  = DOne
-  DBound i // th = th !! i
+  K e // _  = K e
+  B i // th = th !! i

src/Quox/Syntax/DimEq.idr

@@ -0,0 +1,135 @@
+module Quox.Syntax.DimEq
+
+import public Quox.Syntax.Var
+import public Quox.Syntax.Dim
+import public Quox.Syntax.Subst
+import public Quox.Context
+
+import Data.Maybe
+import Data.Nat
+import Data.DPair
+
+%default total
+
+
+public export
+DimEq' : Nat -> Type
+DimEq' = Context (Maybe . Dim)
+
+
+public export
+data DimEq : Nat -> Type where
+  ZeroIsOne : DimEq d
+  C         : (eqs : DimEq' d) -> DimEq d
+
+%name DimEq eqs
+
+
+export
+new' : (d : Nat) -> DimEq' d
+new' 0     = [<]
+new' (S d) = new' d :< Nothing
+
+export
+new : (d : Nat) -> DimEq d
+new d = C (new' d)
+
+
+export
+get : DimEq' d -> Dim d -> Dim d
+get _   (K e) = K e
+get eqs (B i) = fromMaybe (B i) $ (eqs !! i) @{Compose}
+
+export
+equal : DimEq d -> (p, q : Dim d) -> Bool
+equal ZeroIsOne p q = True
+equal (C eqs)   p q = get eqs p == get eqs q
+
+
+infixl 5 :<?
+export
+(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
+ZeroIsOne :<? d = ZeroIsOne
+C eqs     :<? d = C $ eqs :< d
+
+private
+checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d
+checkConst Zero Zero eqs = C eqs
+checkConst One  One  eqs = C eqs
+checkConst _    _    _   = ZeroIsOne
+
+
+export
+setConst : Var d -> DimConst -> DimEq' d -> DimEq d
+setConst VZ e (eqs :< Nothing)    = C $ eqs :< Just (K e)
+setConst VZ e (eqs :< Just (K f)) = checkConst e f $ eqs :< Just (K f)
+setConst VZ e (eqs :< Just (B i)) = setConst i e eqs :<? Just (K e)
+setConst (VS i) e (eqs :< x) =
+  setConst i e eqs :<? (if x == Just (B i) then Just (K e) else x)
+
+mutual
+  private
+  setVar' : (i, j : Var d) -> i `LT` j -> DimEq' d -> DimEq d
+  setVar' VZ (VS i) LTZ (eqs :< Nothing)    = C $ eqs :< Just (B i)
+  setVar' VZ (VS i) LTZ (eqs :< Just (K e)) = setConst i e eqs :<? Just (K e)
+  setVar' VZ (VS i) LTZ (eqs :< Just (B j)) = setVar i j eqs :<? Just (B (max i j))
+  setVar' (VS i) (VS j) (LTS lt) (eqs :< p) =
+    setVar' i j lt eqs :<? map (\k => if k == B i then B j else k) p
+
+  export
+  setVar : (i, j : Var d) -> DimEq' d -> DimEq d
+  setVar i j eqs =
+    case compareP i j of
+      IsLT lt => setVar' i j lt eqs
+      IsEQ    => C eqs
+      IsGT gt => setVar' j i gt eqs
+
+
+export
+set : (p, q : Dim d) -> DimEq d -> DimEq d
+set _ _ ZeroIsOne = ZeroIsOne
+set (K e) (K f) (C eqs) = checkConst e f eqs
+set (K e) (B i) (C eqs) = setConst i e eqs
+set (B i) (K e) (C eqs) = setConst i e eqs
+set (B i) (B j) (C eqs) = setVar   i j eqs
+
+
+export
+setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
+setSelf p ZeroIsOne = Refl
+setSelf (K Zero) (C eqs) = Refl
+setSelf (K One)  (C eqs) = Refl
+setSelf (B i)    (C eqs) with (compareP i i)
+  _ | IsLT lt = absurd lt
+  _ | IsEQ    = Refl
+  _ | IsGT gt = absurd gt
+
+
+
+public export
+Split : Nat -> Type
+Split d = (DimEq' d, DSubst (S d) d)
+
+export
+split1 : DimConst -> DimEq' (S d) -> Maybe (Split d)
+split1 e eqs = case setConst VZ e eqs of
+  ZeroIsOne    => Nothing
+  C (eqs :< _) => Just (eqs, K e ::: id)
+
+export
+split : DimEq' (S d) -> List (Split d)
+split eqs = toList (split1 Zero eqs) <+> toList (split1 One eqs)
+
+
+export
+splits' : DimEq' d -> List (DSubst d 0)
+splits' [<] = [id]
+splits' eqs@(_ :< _) = do
+  (eqs, th) <- split eqs
+  ph <- splits' eqs
+  pure $ th . ph
+
+export
+splits : DimEq d -> List (DSubst d 0)
+splits ZeroIsOne = []
+splits (C eqs) = splits' eqs

src/Quox/Syntax/Qty.idr

@@ -27,11 +27,16 @@ PrettyHL Qty where
       One  => ifUnicode "𝟭" "1"
       Any  => ifUnicode "𝛚" "*"
 
+private
+commas : List (Doc HL) -> List (Doc HL)
+commas [] = []
+commas [x] = [x]
+commas (x::xs) = (x <+> hl Delim ",") :: commas xs
+
 export %inline
 prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
 prettyQtyBinds =
-  map (align . sep) .
-  traverse (\pi => [|pretty0M pi <++> pure (hl Delim "|")|])
+  map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M
 
 
 public export

src/Quox/Syntax/Shift.idr

@@ -59,9 +59,9 @@ export
                by.nat + i.nat `LT` to
 shiftVarLT by i =
   rewrite plusSuccRightSucc by.nat i.nat in
-  transitive {rel=LTE}
+  transitive {rel=Nat.LTE}
     (plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
-    (replace {p=(\n => LTE n to)} (shiftDiff by) $ reflexive {rel=LTE})
+    (replace {p=(`LTE` to)} (shiftDiff by) $ reflexive {rel=Nat.LTE})
 
 
 public export
@@ -204,3 +204,11 @@ interface CanShift f where
   (//) : f from -> Shift from to -> f to
 
 export CanShift Var where i // by = shift by i
+
+namespace CanShift
+  export
+  [Compose] (Functor f, CanShift tm) => CanShift (f . tm) where
+    x // by = map (// by) x
+
+  export
+  [Const] CanShift (\_ => a) where x // _ = x

src/Quox/Syntax/Term.idr

@@ -34,7 +34,7 @@ mutual
     TYPE : (l : Universe) -> Term d n
 
     ||| function type
-    Pi  : (qty, qtm : Qty) -> (x : Name) ->
+    Pi  : (qtm, qty : Qty) -> (x : Name) ->
           (arg : Term d n) -> (res : Term d (S n)) -> Term d n
     ||| function term
     Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
@@ -126,9 +126,9 @@ mutual
   PrettyHL (Term d n) where
     prettyM (TYPE l) =
       parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
-    prettyM (Pi qty qtm x s t) =
+    prettyM (Pi qtm qty x s t) =
       parensIfM Outer $ hang 2 $
-        !(prettyBinder [qty, qtm] x s) <++> !arrowD
+        !(prettyBinder [qtm, qty] x s) <++> !arrowD
           <//> !(under T x $ prettyM t)
     prettyM (Lam x t) =
       parensIfM Outer $
@@ -172,8 +172,9 @@ mutual
   prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
   prettyBinder pis x a =
     pure $ parens $ hang 2 $
-      !(prettyQtyBinds pis) <//>
-      hsep [hl TVar !(prettyM x), colonD, !(withPrec Outer $ prettyM a)]
+      hsep [hl TVar !(prettyM x),
+            sep [!(prettyQtyBinds pis),
+                 hsep [colonD, !(withPrec Outer $ prettyM a)]]]
 
 
 export FromVar (Elim d) where fromVar = B
@@ -304,47 +305,57 @@ ncloE e = Element e %search
 mutual
   ||| if the input term has any top-level closures, push them under one layer of
   ||| syntax
-  export
+  export %inline
   pushSubstsT : Term d n -> NotCloTerm d n
-  pushSubstsT s = pushSubstsT' id id s
+  pushSubstsT s = pushSubstsTWith id id s
 
   ||| if the input elimination has any top-level closures, push them under one
   ||| layer of syntax
-  export
+  export %inline
   pushSubstsE : Elim d n -> NotCloElim d n
-  pushSubstsE e = pushSubstsE' id id e
+  pushSubstsE e = pushSubstsEWith id id e
 
   private
-  pushSubstsT' : DSubst dfrom dto -> TSubst dto from to ->
-                 Term dfrom from -> NotCloTerm dto to
-  pushSubstsT' th ph (TYPE l) =
+  pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
+                    Term dfrom from -> NotCloTerm dto to
+  pushSubstsTWith th ph (TYPE l) =
     ncloT $ TYPE l
-  pushSubstsT' th ph (Pi qty qtm x a b) =
-    ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph))
-  pushSubstsT' th ph (Lam x t) =
+  pushSubstsTWith th ph (Pi qtm qty x a b) =
+    ncloT $ Pi qtm qty x (subs a th ph) (subs b th (push ph))
+  pushSubstsTWith th ph (Lam x t) =
     ncloT $ Lam x $ subs t th $ push ph
-  pushSubstsT' th ph (E e) =
-    let Element e _ = pushSubstsE' th ph e in ncloT $ E e
-  pushSubstsT' th ph (CloT  s ps) =
-    pushSubstsT' th (comp' th ps ph) s
-  pushSubstsT' th ph (DCloT s ps) =
-    pushSubstsT' (ps . th) ph s
+  pushSubstsTWith th ph (E e) =
+    let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
+  pushSubstsTWith th ph (CloT  s ps) =
+    pushSubstsTWith th (comp' th ps ph) s
+  pushSubstsTWith th ph (DCloT s ps) =
+    pushSubstsTWith (ps . th) ph s
 
   private
-  pushSubstsE' : DSubst dfrom dto -> TSubst dto from to ->
-                 Elim dfrom from -> NotCloElim dto to
-  pushSubstsE' th ph (F x) =
+  pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
+                    Elim dfrom from -> NotCloElim dto to
+  pushSubstsEWith th ph (F x) =
     ncloE $ F x
-  pushSubstsE' th ph (B i) =
+  pushSubstsEWith th ph (B i) =
     assert_total pushSubstsE $ ph !! i
-  pushSubstsE' th ph (f :@ s) =
+  pushSubstsEWith th ph (f :@ s) =
     ncloE $ subs f th ph :@ subs s th ph
-  pushSubstsE' th ph (s :# a) =
+  pushSubstsEWith th ph (s :# a) =
     ncloE $ subs s th ph :# subs a th ph
-  pushSubstsE' th ph (CloE  e ps) =
-    pushSubstsE' th (comp' th ps ph) e
-  pushSubstsE' th ph (DCloE e ps) =
-    pushSubstsE' (ps . th) ph e
+  pushSubstsEWith th ph (CloE  e ps) =
+    pushSubstsEWith th (comp' th ps ph) e
+  pushSubstsEWith th ph (DCloE e ps) =
+    pushSubstsEWith (ps . th) ph e
+
+
+public export %inline
+pushSubstsT' : Term d n -> Term d n
+pushSubstsT' s = (pushSubstsT s).fst
+
+
+public export %inline
+pushSubstsE' : Elim d n -> Elim d n
+pushSubstsE' e = (pushSubstsE e).fst
 
 
 parameters {auto _ : Alternative f}

src/Quox/Syntax/Var.idr

@@ -133,3 +133,82 @@ public export
 interface FromVar f where %inline fromVar : Var n -> f n
 
 public export FromVar Var where fromVar = id
+
+
+public export
+data LT : Var n -> Var n -> Type where
+  LTZ : VZ `LT` VS i
+  LTS : i `LT` j -> VS i `LT` VS j
+%builtin Natural Var.LT
+%name Var.LT lt
+
+public export %inline
+GT : Var n -> Var n -> Type
+i `GT` j = j `LT` i
+
+export
+Transitive (Var n) LT where
+  transitive LTZ     (LTS _) = LTZ
+  transitive (LTS p) (LTS q) = LTS $ transitive p q {rel=Var.LT}
+
+export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
+export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible
+
+export
+isLT : (i, j : Var n) -> Dec (i `LT` j)
+isLT VZ     VZ     = No uninhabited
+isLT VZ     (VS j) = Yes LTZ
+isLT (VS i) VZ     = No uninhabited
+isLT (VS i) (VS j) with (isLT i j)
+  _ | Yes prf   = Yes (LTS prf)
+  _ | No contra = No  (\case LTS p => contra p)
+
+
+public export
+data Compare : (i, j : Var n) -> Type where
+  IsLT : (lt : i `LT` j) -> Compare i j
+  IsEQ :                    Compare i i
+  IsGT : (gt : i `GT` j) -> Compare i j
+%name Compare cmp
+
+export
+compareS : Compare i j -> Compare (VS i) (VS j)
+compareS (IsLT lt) = IsLT (LTS lt)
+compareS IsEQ      = IsEQ
+compareS (IsGT gt) = IsGT (LTS gt)
+
+export
+compareP : (i, j : Var n) -> Compare i j
+compareP VZ     VZ     = IsEQ
+compareP VZ     (VS j) = IsLT LTZ
+compareP (VS i) VZ     = IsGT LTZ
+compareP (VS i) (VS j) = compareS $ compareP i j
+
+
+public export
+data LTE : Var n -> Var n -> Type where
+  LTEZ : VZ `LTE` j
+  LTES : i  `LTE` j -> VS i `LTE` VS j
+
+export
+Reflexive (Var n) LTE where
+  reflexive {x = VZ}   = LTEZ
+  reflexive {x = VS i} = LTES $ reflexive {x=i}
+
+export
+Transitive (Var n) LTE where
+  transitive LTEZ     q        = LTEZ
+  transitive (LTES p) (LTES q) = LTES $ transitive p q {rel=Var.LTE}
+
+export
+Antisymmetric (Var n) LTE where
+  antisymmetric LTEZ     LTEZ     = Refl
+  antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q {rel=Var.LTE}
+
+export
+splitLTE : {j : Var n} -> i `Var.LTE` j -> Either (i = j) (i `Var.LT` j)
+splitLTE {j = VZ}   LTEZ     = Left Refl
+splitLTE {j = VS _} LTEZ     = Right LTZ
+splitLTE            (LTES p) with (splitLTE p)
+  _ | (Left  eq) = Left $ cong VS eq
+  _ | (Right lt) = Right $ LTS lt

src/Quox/Typecheck.idr

@@ -1,152 +0,0 @@
-module Quox.Typecheck
-
-import Quox.Syntax
-import Quox.Error
-import Quox.Context
-
-import Data.Nat
-import Control.Monad.Reader
-import Control.Monad.State
-
-
-%default total
-
-public export
-DContext : Nat -> Type
-DContext = Context Dim
-
-public export
-TContext : Nat -> Nat -> Type
-TContext d = Context (Term d)
-
-public export
-QContext : Nat -> Type
-QContext = Triangle' Qty
-
-public export
-QOutput : Nat -> Type
-QOutput = Context' Qty
-
-
-namespace TContext
-  export
-  pushD : TContext d n -> TContext (S d) n
-  pushD tel = map (/// shift 1) tel
-
-
-namespace Zero
-  public export
-  data IsZero : QOutput n -> Type where
-    LinZ  : IsZero [<]
-    SnocZ : IsZero qctx -> IsZero (qctx :< Zero)
-
-  export
-  isZeroIrrel : {qctx : _} -> (0 _ : IsZero qctx) -> IsZero qctx
-  isZeroIrrel {qctx = [<]}    LinZ      = LinZ
-  isZeroIrrel {qctx = _ :< _} (SnocZ x) = SnocZ $ isZeroIrrel x
-
-  export
-  zero : Context _ n -> Subset (QOutput n) IsZero
-  zero [<]        = Element [<] LinZ
-  zero (ctx :< _) = let zeroN = zero ctx in
-                    Element (zeroN.fst :< Zero) (SnocZ zeroN.snd)
-
-
-namespace Only
-  public export
-  data IsOnly : QOutput n -> Var n -> Type where
-    Here  : IsZero qctx   -> IsOnly (qctx :< One) VZ
-    There : IsOnly qctx i -> IsOnly (qctx :< Zero) (VS i)
-
-  export
-  isOnlyIrrel : {qctx, i : _} -> (0 _ : IsOnly qctx i) -> IsOnly qctx i
-  isOnlyIrrel {i = VZ}     (Here  z) = Here  $ isZeroIrrel z
-  isOnlyIrrel {i = (VS i)} (There o) = There $ isOnlyIrrel o
-
-  export
-  only : Context _ n -> (i : Var n) ->
-         Subset (QOutput n) (\qctx => IsOnly qctx i)
-  only (ctx :< _) VZ     =
-    let zeroN = zero ctx in
-    Element (zeroN.fst :< One) (Here zeroN.snd)
-  only (ctx :< _) (VS i) =
-    let onlyN = only ctx i in
-    Element (onlyN.fst :< Zero) (There onlyN.snd)
-
-
-public export
-data LT : Universe -> Universe -> Type where
-  Fin : k `LT` l -> U k `LT` U l
-  Any : U _ `LT` UAny
-
-
-namespace Lookup
-  public export
-  data IsLookup :
-      (tctx : TContext d n) ->
-      (i    : Var n) ->
-      (ty   : Term d from) ->
-      (by   : Shift from n) -> Type
-    where
-      Here  : IsLookup {tctx=(tctx :< ty), i=VZ, ty, by=(SS SZ)}
-      There : IsLookup {tctx, i, ty, by} ->
-              IsLookup {tctx=(tctx :< ty'), i=(VS i), ty, by=(SS by)}
-
-  public export
-  record Lookup {0 d, n : Nat} (0 tctx : TContext d n) (0 i : Var n) where
-    constructor MkLookup
-    qtys : QOutput n
-    type : Term d from
-    by   : Shift from n
-    0 only : IsOnly qtys i
-    0 look : IsLookup tctx i type by
-
-export
-lookup : (ctx : TContext d n) -> (i : Var n) -> Lookup tctx i
-lookup (ctx :< x) VZ =
-  ?lookup_rhs_3
-lookup (ctx :< x) (VS i) =
-  ?lookup_rhs_4
-
-
-
-mutual
-  public export
-  data HasTypeT :
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) ->
-      (subj : Term d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-      TYPE :
-        WfCtx {dctx, tctx, qctx} ->
-        k `LT` l ->
-        (0 _ : IsZero tmout) -> (0 _ : IsZero tyout) ->
-        HasTypeT {dctx, tctx, qctx, subj=(TYPE k), ty=(TYPE l), tmout, tyout}
-
-  public export
-  data HasTypeE :
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) ->
-      (subj : Elim d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-
-  public export
-  data WfCtx :
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) ->
-      Type
-    where
-      NIL  : WfCtx [<] [<] [<]
-      BIND :
-        WfCtx    {dctx, tctx, qctx} ->
-        HasTypeT {dctx, tctx, qctx, subj=a, ty=(TYPE l), tmout, tyout} ->
-        WfCtx    {dctx, tctx=(tctx :< a), qctx=(qctx :< tmout)}

src/Quox/Typechecker.idr

@@ -0,0 +1,168 @@
+module Quox.Typechecker
+
+import public Quox.Syntax
+import public Quox.Typing
+import Quox.Error
+
+import Data.Nat
+import Data.SortedMap
+import Control.Monad.Reader
+import Control.Monad.State
+import Syntax.WithProof
+
+%default total
+
+
+public export
+data Error : Type where
+  ExpectedType : (subj, ty : Term d n) -> Error
+  UniverseInconsistency : (lo, hi : Universe) -> Error
+  GlobalNotInScope : Name -> Error
+
+public export
+record CheckResult
+  {0 d, n : Nat}
+  (0 ctx : WfContext d n)
+  (0 subj, ty : Term d n)
+where
+  constructor MkCheckResult
+  tmout, tyout : QOutput n
+  hasType : HasTypeT {ctx = ctx.ctx, subj, ty, tmout, tyout}
+
+
+public export
+record InferResult
+  {0 d, n : Nat}
+  (0 ctx : WfContext d n)
+  (0 subj : Elim d n)
+where
+  constructor MkInferResult
+  tmout, tyout : QOutput n
+  ty : Term d n
+  hasType : HasTypeE {ctx = ctx.ctx, subj, ty, tmout, tyout}
+
+
+public export
+zeroCtx : Globals -> TyContext 0 0
+zeroCtx globals = MkTyContext {globals, dctx = DNil, tctx = [<], qctx = [<]}
+
+public export
+zeroWfCtx : Globals -> WfContext 0 0
+zeroWfCtx globals = MkWfContext (zeroCtx globals) NIL
+
+public export
+Check0 : (globals : Globals) -> (subj, ty : Term 0 0) -> Type
+Check0 globals subj ty =
+  HasTypeT {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
+
+public export
+record Infer0 (globals : Globals) (subj : Elim 0 0) where
+  constructor MkInfer0
+  ty : Term 0 0
+  hasType : HasTypeE {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
+
+
+export
+0 isTypeZeroTyout : HasTypeT {ty = TYPE _, tyout, _} -> IsZero tyout
+isTypeZeroTyout (TYPE  {zty, _}) = zty
+isTypeZeroTyout (Pi    {zty, _}) = zty
+isTypeZeroTyout (PushT {})   = ?isTypeZeroTyout_PushT
+
+
+parameters {auto _ : MonadThrow Error m} mutual
+  private
+  checkUniverse : (lo, hi : Universe) -> m (lo `LT` hi)
+  checkUniverse lo hi with (lo `isLT` hi)
+    _ | Yes lt = pure lt
+    _ | No  _  = throw $ UniverseInconsistency {lo, hi}
+
+  private
+  expectType : (subj, ty : Term d n) ->
+               m (l : Universe ** ty = TYPE l)
+  expectType _    (TYPE l) = pure (l ** Refl)
+  expectType subj ty       = throw $ ExpectedType {subj, ty}
+
+  private
+  checkType : (ctx : WfContext d n) ->
+              (l : Universe) -> (ty : Term d n) ->
+              m (CheckResult ctx (TYPE l) ty)
+  checkType (MkWfContext {ctx, wf}) l ty = do
+    (l' ** eq) <- expectType (TYPE l) ty; let Refl = eq
+    lt <- checkUniverse l l'
+    let Element _ zprf = zero ctx.qctx
+    pure $ MkCheckResult {hasType = TYPE {wf, lt, ztm = zprf, zty = zprf}, _}
+
+  private
+  checkPi : (ctx : WfContext d n) ->
+            (qtm, qty : Qty) ->
+            (x : Name) ->
+            (arg : Term d n) ->
+            (res : Term d (S n)) ->
+            (ty  : Term d n) ->
+            m (CheckResult ctx (Pi qtm qty x arg res) ty)
+  checkPi (MkWfContext {ctx, wf}) qtm qty x arg res ty = do
+    let whole = Pi qtm qty x arg res
+    (l' ** eq) <- expectType whole ty; let Refl = eq
+    ?checkPi_rhs
+
+
+  private
+  inferFree : (ctx : WfContext {}) -> (x : Name) -> m (InferResult ctx (F x))
+  inferFree (MkWfContext {ctx, wf}) x =
+    case @@ lookup x ctx.globals of
+      (Just g ** eq) =>
+        let Element _ zprf = zero ctx.tctx
+            hasType = F {wf, g, eq, ztm = zprf, zty = zprf}
+        in
+        pure $ MkInferResult {hasType, _}
+      _ => throw $ GlobalNotInScope x
+
+  private
+  inferBound : (ctx : WfContext _ n) -> (i : Var n) -> m (InferResult ctx (B i))
+  inferBound (MkWfContext {ctx, wf}) i =
+    pure $ MkInferResult {hasType = B {wf, look = lookup ctx i, eq = Refl}, _}
+
+  private
+  inferAnn : (ctx : WfContext d n) -> (tm, ty : Term d n) ->
+             m (InferResult ctx (tm :# ty))
+  inferAnn ctx tm ty = do
+    ignore $ check ctx ty (TYPE UAny)
+    MkCheckResult {hasType, _} <- check ctx tm ty
+    pure $ MkInferResult {hasType = Ann hasType, _}
+
+
+  export
+  check : (ctx : WfContext d n) -> (subj, ty : Term d n) ->
+          m (CheckResult ctx subj ty)
+  check ctx subj ty = case subj of
+    TYPE l               => checkType ctx l ty
+    Pi qtm qty x arg res => checkPi ctx qtm qty x arg res ty
+    Lam x body           => ?check_rhs_3
+    E e                  => ?check_rhs_4
+    CloT  s th           => ?check_rhs_5
+    DCloT s th           => ?check_rhs_6
+
+  export
+  infer : (ctx : WfContext d n) -> (subj : Elim d n) ->
+          m (InferResult ctx subj)
+  infer ctx subj = case subj of
+    F x        => inferFree ctx x
+    B i        => inferBound ctx i
+    fun :@ arg => ?infer_rhs_3
+    tm :# ty   => inferAnn ctx tm ty
+    CloE  e th => ?infer_rhs_5
+    DCloE e th => ?infer_rhs_6
+
+
+parameters {auto _ : MonadThrow Error m} (globals : Globals)
+  public export
+  check0 : (subj, ty : Term 0 0) -> m (Check0 globals subj ty)
+  check0 subj ty = pure $
+    case !(check (zeroWfCtx globals) subj ty) of
+      MkCheckResult [<] [<] prf => prf
+
+  public export
+  infer0 : (subj : Elim 0 0) -> (ty : Term 0 0) -> m (Infer0 globals subj)
+  infer0 subj ty = pure $
+    case !(infer (zeroWfCtx globals) subj) of
+      MkInferResult [<] [<] ty prf => MkInfer0 ty prf

src/Quox/Typing.idr

@@ -0,0 +1,280 @@
+module Quox.Typing
+
+import public Quox.Syntax
+import public Quox.Context
+
+import Data.Nat
+import Data.SortedMap
+import Control.Monad.Reader
+import Control.Monad.State
+
+
+%default total
+
+public export
+data DContext : Nat -> Type where
+  DNil  : DContext 0
+  DBind : DContext d -> DContext (S d)
+  DEq   : Dim d -> Dim d -> DContext d -> DContext d
+
+public export
+TContext : Nat -> Nat -> Type
+TContext d = Context (Term d)
+
+public export
+QContext : Nat -> Type
+QContext = Triangle' Qty
+
+public export
+QOutput : Nat -> Type
+QOutput = Context' Qty
+
+
+public export
+record Global where
+  constructor MkGlobal
+  type, term : forall d, n. Term d n
+
+public export
+Globals : Type
+Globals = SortedMap Name Global
+
+
+public export
+record TyContext (d, n : Nat) where
+  constructor MkTyContext
+  globals : Globals
+  dctx : DContext d
+  tctx : TContext d n
+  qctx : QContext n
+
+%name TyContext ctx
+
+
+namespace TContext
+  export
+  pushD : TContext d n -> TContext (S d) n
+  pushD tel = map (/// shift 1) tel
+
+
+namespace TyContext
+  export
+  extendTy : Term d n -> QOutput n -> TyContext d n -> TyContext d (S n)
+  extendTy s rhos = {tctx $= (:< s), qctx $= (:< rhos)}
+
+  export
+  extendDim : TyContext d n -> TyContext (S d) n
+  extendDim = {dctx $= DBind, tctx $= pushD}
+
+  export
+  eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
+  eqDim p q = {dctx $= DEq p q}
+
+
+
+namespace QOutput
+  export
+  (+) : QOutput n -> QOutput n -> QOutput n
+  (+) = zipWith (+)
+
+  export
+  (*) : Qty -> QOutput n -> QOutput n
+  (*) pi = map (pi *)
+
+
+namespace Zero
+  public export
+  data IsZero : QOutput n -> Type where
+    LinZ  : IsZero [<]
+    SnocZ : IsZero qctx -> IsZero (qctx :< Zero)
+
+  export
+  isZeroIrrel : {qctx : _} -> (0 _ : IsZero qctx) -> IsZero qctx
+  isZeroIrrel {qctx = [<]}    LinZ      = LinZ
+  isZeroIrrel {qctx = _ :< _} (SnocZ x) = SnocZ $ isZeroIrrel x
+
+  export
+  zero : Context _ n -> Subset (QOutput n) IsZero
+  zero [<]        = Element [<] LinZ
+  zero (ctx :< _) = let zeroN = zero ctx in
+                    Element (zeroN.fst :< Zero) (SnocZ zeroN.snd)
+
+
+namespace Only
+  public export
+  data IsOnly : QOutput n -> Var n -> Type where
+    Here  : IsZero qctx   -> IsOnly (qctx :< One) VZ
+    There : IsOnly qctx i -> IsOnly (qctx :< Zero) (VS i)
+
+  export
+  isOnlyIrrel : {qctx, i : _} -> (0 _ : IsOnly qctx i) -> IsOnly qctx i
+  isOnlyIrrel {i = VZ}     (Here  z) = Here  $ isZeroIrrel z
+  isOnlyIrrel {i = (VS i)} (There o) = There $ isOnlyIrrel o
+
+  export
+  only : Context _ n -> (i : Var n) ->
+         Subset (QOutput n) (\qctx => IsOnly qctx i)
+  only (ctx :< _) VZ     =
+    let zeroN = zero ctx in
+    Element (zeroN.fst :< One) (Here zeroN.snd)
+  only (ctx :< _) (VS i) =
+    let onlyN = only ctx i in
+    Element (onlyN.fst :< Zero) (There onlyN.snd)
+
+
+namespace Universe
+  public export
+  data LT : Universe -> Universe -> Type where
+    Fin : k `LT` l -> U k `LT` U l
+    Any : U _ `LT` UAny
+
+  export
+  Uninhabited (UAny `LT` j) where
+    uninhabited _ impossible
+
+  export
+  isLT : (i, j : Universe) -> Dec (i `LT` j)
+  isLT (U i) (U j) with (i `isLT` j)
+    _ | Yes prf   = Yes $ Fin prf
+    _ | No contra = No  $ \(Fin prf) => contra prf
+  isLT (U _) UAny = Yes Any
+  isLT UAny  _    = No uninhabited
+
+
+namespace Lookup
+  public export
+  data IsLookup :
+      (tctx : TContext d n) ->
+      (i    : Var n) ->
+      (ty   : Term d from) ->
+      (by   : Shift from n) -> Type
+    where
+      Here  : IsLookup {tctx=(tctx :< ty), i=VZ, ty, by=(SS SZ)}
+      There : IsLookup {tctx, i, ty, by} ->
+              IsLookup {tctx=(tctx :< ty'), i=(VS i), ty, by=(SS by)}
+
+  public export
+  record Lookup'
+    {0 d, n : Nat}
+    (0 tctx : TContext d n)
+    (0 qctx : QContext n)
+    (0 i : Var n)
+  where
+    constructor MkLookup
+    tmout, tyout : QOutput n
+    type : Term d from
+    by   : Shift from n
+    0 only : IsOnly tmout i
+    0 look : IsLookup tctx i type by
+
+  public export
+  lookup' : (tctx : TContext d n) -> (qctx : QContext n) ->
+            (i : Var n) -> Lookup' tctx qctx i
+  lookup' tctx@(_ :< _) (_ :< tyout) VZ =
+    MkLookup {only = (only tctx VZ).snd, look = Here,
+              tyout = tyout :< Zero, _}
+  lookup' (tctx :< _) (qctx :< _) (VS i) =
+    let inner = lookup' tctx qctx i in
+    MkLookup {only = There inner.only, look = There inner.look,
+              tyout = inner.tyout :< Zero, _}
+
+
+  public export %inline
+  Lookup : TyContext d n -> Var n -> Type
+  Lookup ctx i = Lookup' ctx.tctx ctx.qctx i
+
+  public export %inline
+  lookup : (ctx : TyContext d n) -> (i : Var n) -> Lookup ctx i
+  lookup ctx = lookup' ctx.tctx ctx.qctx
+
+
+
+mutual
+  public export
+  data HasTypeT :
+      {0 d, n : Nat} ->
+      (ctx  : TyContext d n) ->
+      (subj : Term d n) ->
+      (ty   : Term d n) ->
+      (tmout, tyout : QOutput n) ->
+      Type
+    where
+      TYPE :
+        (0 wf : IsWf ctx) ->
+        (lt : k `LT` l) ->
+        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
+        HasTypeT {ctx, subj = TYPE k, ty = TYPE l, tmout, tyout}
+      Pi :
+        (tyA : HasTypeT {ctx, subj = a, ty = TYPE l, tmout = tmoutA, tyout}) ->
+        (tyB : HasTypeT {ctx = extendTy a tmoutA ctx, subj = b, ty = TYPE l,
+                         tmout = tmoutB :< qty, tyout = tyout :< Zero}) ->
+        (0 zty : IsZero tyout) ->
+        HasTypeT {ctx, subj = Pi qtm qty x a b, ty = TYPE l,
+                  tmout = tmoutA + tmoutB, tyout}
+      PushT :
+        (0 eq : ty' = pushSubstsT' ty) ->
+        (j : HasTypeT {ctx, subj, ty = ty', tmout, tyout}) ->
+        HasTypeT {ctx, subj, ty, tmout, tyout}
+
+  public export
+  data HasTypeE :
+      {0 d, n : Nat} ->
+      (ctx  : TyContext d n) ->
+      (subj : Elim d n) ->
+      (ty   : Term d n) ->
+      (tmout, tyout : QOutput n) ->
+      Type
+    where
+      F :
+        (0 wf : IsWf ctx) ->
+        (g : Global) ->
+        (0 eq : lookup x ctx.globals = Just g) ->
+        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
+        HasTypeE {ctx, subj = F x, ty = g.type, tmout, tyout}
+      B :
+        {0 ctx : TyContext d n} ->
+        (0 wf : IsWf ctx) ->
+        (look : Lookup ctx i) ->
+        (0 eq : ty = look.type // look.by) ->
+        HasTypeE {ctx, subj = B i, ty, tmout = look.tmout, tyout = look.tyout}
+      Ann :
+        HasTypeT {ctx, subj = tm,       ty, tmout, tyout} ->
+        HasTypeE {ctx, subj = tm :# ty, ty, tmout, tyout}
+      PushE :
+        (0 eq : ty' = pushSubstsT' ty) ->
+        HasTypeE {ctx, subj, ty = ty', tmout, tyout} ->
+        HasTypeE {ctx, subj, ty, tmout, tyout}
+
+  public export
+  data IsWf' :
+      (globals : Globals) ->
+      (dctx : DContext d) ->
+      (tctx : TContext d n) ->
+      (qctx : QContext n) -> Type
+    where
+      NIL  : IsWf' globals dctx [<] [<]
+      BIND :
+        IsWf' {globals, dctx, tctx, qctx} ->
+        HasTypeT {ctx = MkTyContext {globals, dctx, tctx, qctx},
+                  subj, ty = TYPE l, tmout, tyout} ->
+        IsWf' {globals, dctx, tctx = tctx :< subj, qctx = qctx :< tmout}
+
+  public export %inline
+  IsWf : TyContext d n -> Type
+  IsWf (MkTyContext {globals, dctx, tctx, qctx}) =
+    IsWf' {globals, dctx, tctx, qctx}
+
+public export
+record WfContext (d, n : Nat) where
+  constructor MkWfContext
+  ctx  : TyContext d n
+  0 wf : IsWf ctx
+
+
+public export
+record TypeTerm {0 d, n : Nat} (ctx : TyContext d n) where
+  constructor MkTypeTerm
+  term : Term d n
+  univ : Universe
+  tmout, tyout : QOutput n
+  isType : HasTypeT {ctx, subj = term, ty = TYPE univ, tmout, tyout}