diff --git a/J.red b/J.red
index 64e95a6ed..133fd5959 100644
--- a/J.red
+++ b/J.red
@@ -6,27 +6,29 @@ let J
   (x : A) (p : Path _ a x)
   : C x p
   =
-  let ty : dim → type = λ i →
-    let h : dim → A = λ j →
-      comp 0 j a [
-      | i=0 ⇒ λ _ → a
-      | i=1 ⇒ λ k → p k
-      ]
-    in
-    C (h 1) (λ k → h k)
+  let ty : dim → type =
+    λ i →
+      let h : dim → A =
+        λ j →
+          comp 0 j a [
+          | i=0 ⇒ auto
+          | i=1 ⇒ p
+          ]
+      in
+      C (h 1) h
   in
   coe 0 1 d in ty
 
 let J/eq
   (A : type) (a : A)
-  (C : (x : A) (p : Path A a x) → type) (d : C a (λ _ → a))
-  : Path (C a _) (J _ _ C d _ (λ _ → a)) d
+  (C : (x : A) (p : Path A a x) → type) (d : C a auto)
+  : Path (C a auto) (J _ _ C d _ (λ _ → a)) d
   =
   let square : dim → dim → A =
     λ i j →
       comp 0 j a [
-      | i=0 ⇒ λ _ → a
-      | i=1 ⇒ λ _ → a
+      | i=0 ⇒ auto
+      | i=1 ⇒ auto
       ]
   in
   λ k →
@@ -34,16 +36,17 @@ let J/eq
       let aux : dim → A =
         λ j →
           comp 0 j a [
-          | k=0 ⇒ λ l → square i l
-          | k=1 ⇒ λ _ → a
-          | i=0 ⇒ λ _ → a
-          | i=1 ⇒ λ _ → a
+          | k=0 ⇒ square i
+          | k=1 ⇒ auto
+          | i=0 ⇒ auto
+          | i=1 ⇒ auto
           ]
       in
-      C (aux 1) (λ l → aux l)
+      C (aux 1) aux
     with
-    | k=0 ⇒ λ i →
-      coe 0 i d in λ j →
-        C (square j 1) (λ k → square j k)
-    | k=1 ⇒ λ _ → d
+    | k=0 ⇒
+      λ i →
+        coe 0 i d in λ j →
+          C (square j 1) (square j)
+    | k=1 ⇒ auto
     end
diff --git a/README.md b/README.md
index 87e297b75..d3fd25146 100644
--- a/README.md
+++ b/README.md
@@ -31,7 +31,7 @@ and [cubicaltt](https://github.com/mortberg/cubicaltt).
   supported)  based on the [work of Evan Cavallo and Bob
   Harper](https://arxiv.org/abs/1801.01568)
 
-- experimental support for Fitch-style modal guarded recursion: □, ▷
+- experimental support for Fitch-style modal guarded recursion: ▷
 
 
 Features we intend to add in the near future:
diff --git a/bool.red b/bool.red
index 0f12fdf85..7d07e2a9f 100644
--- a/bool.red
+++ b/bool.red
@@ -15,6 +15,6 @@ let not∘not (x : bool) : _ =
 
 let not∘not/id/pt (x : bool) : Path _ (not∘not x) x =
   elim x [
-  | tt ⇒ λ _ → tt
-  | ff ⇒ λ _ → ff
+  | tt ⇒ auto
+  | ff ⇒ auto
   ]
diff --git a/connection.red b/connection.red
index 587acd881..301e73c12 100644
--- a/connection.red
+++ b/connection.red
@@ -1,10 +1,5 @@
 import path
 
-let singleton (A : type) (M : A) : type pre =
-  restrict A [
-  | 0=0 ⇒ M
-  ]
-
 let connection/or
  (A : type)
  (p : dim → A)
@@ -22,27 +17,18 @@ let connection/or
   let face : dim → dim → A =
     λ l k →
       comp 0 l (p k) [
-      | k=1 ⇒ λ _ → p 1
-      | k=0 ⇒ λ m → p m
+      | k=1 ⇒ auto
+      | k=0 ⇒ p
       ]
   in
   comp 1 0 (p 1) [
-  | i=0 ⇒ λ k → face j k
-  | i=1 ⇒ λ k → face 1 k
-  | j=0 ⇒ λ k → face i k
-  | j=1 ⇒ λ k → face 1 k
-  | i=j ⇒ λ k → face i k
+  | i=0 ⇒ face j
+  | i=1 ⇒ face 1
+  | j=0 ⇒ face i
+  | j=1 ⇒ face 1
+  | i=j ⇒ face i
   ]
 
-; an example of using the singleton type to establish an exact equality
-let connection/or/diagonal
- (A : type)
- (p : dim → A)
- : singleton _ p
- =
- λ i →
-   connection/or _ p i i
-
 let connection/and
  (A : type)
  (p : dim → A)
@@ -57,16 +43,16 @@ let connection/and
    let face : dim → dim → A =
      λ l k →
        comp 1 l (p k) [
-       | k=0 ⇒ λ _ → p 0
-       | k=1 ⇒ λ m → p m
+       | k=0 ⇒ auto
+       | k=1 ⇒ p
        ]
    in
    comp 0 1 (p 0) [
-   | i=0 ⇒ λ k → face 0 k
-   | i=1 ⇒ λ k → face j k
-   | j=0 ⇒ λ k → face 0 k
-   | j=1 ⇒ λ k → face i k
-   | i=j ⇒ λ k → face i k
+   | i=0 ⇒ face 0
+   | i=1 ⇒ face j
+   | j=0 ⇒ face 0
+   | j=1 ⇒ face i
+   | i=j ⇒ face i
    ]
 
 
diff --git a/equivalence.red b/equivalence.red
index f6ba59a1c..14a65f8b3 100644
--- a/equivalence.red
+++ b/equivalence.red
@@ -15,3 +15,8 @@ let IsEquiv (A, B : type) (f : A → B) : type =
 
 let Equiv (A, B : type) : type =
   (f : A → B) × IsEquiv _ _ f
+
+let UA (A,B : type) (E : Equiv A B) : Path^1 type A B =
+  λ i →
+    `(V i A B E)
+
diff --git a/hedberg-wip.red b/hedberg-wip.red
index aae7f93c8..222c3bd69 100644
--- a/hedberg-wip.red
+++ b/hedberg-wip.red
@@ -23,10 +23,9 @@ let or/elim
   (m0 : A → C)
   (m1 : B → C)
   : C =
-  sg/elim bool (λ b → elim b [tt ⇒ A | ff ⇒ B]) (λ _ _ → C) t
+  sg/elim bool _ (λ _ _ → C) t
     (λ b →
-      elim b in (λ b → (elim b in (λ _ → type) [tt ⇒ A | ff ⇒ B]) → C)
-      [tt ⇒ m0 | ff ⇒ m1])
+      elim b [tt ⇒ m0 | ff ⇒ m1])
 
 let neg (A : type) : type =
   A → void
diff --git a/int.red b/int.red
index 65a6522ee..614d16817 100644
--- a/int.red
+++ b/int.red
@@ -30,11 +30,11 @@ let isuc (x : int) : int =
 
 let pred-isuc (n : int) : Path int (pred (isuc n)) n =
   elim n [
-  | pos n ⇒ λ _ → pos n
+  | pos n ⇒ auto
   | negsuc n ⇒
     elim n [
-    | zero ⇒ λ _ → negsuc zero
-    | suc n ⇒ λ _ → negsuc (suc n)
+    | zero ⇒ auto
+    | suc n ⇒ auto
     ]
   ]
 
@@ -42,11 +42,11 @@ let isuc-pred (n : int) : Path int (isuc (pred n)) n =
   elim n [
   | pos n ⇒
     elim n [
-    | zero ⇒ λ _ → pos zero
-    | suc n' ⇒ λ _ → pos (suc n')
+    | zero ⇒ auto
+    | suc n' ⇒ auto
     ]
-  | negsuc n ⇒ λ _ → negsuc n
+  | negsuc n ⇒ auto
   ]
 
 let isuc-equiv : Equiv int int =
-  Iso/Equiv _ _ < isuc, < pred, < isuc-pred, pred-isuc > > >
+  Iso/Equiv _ _ <isuc, <pred, <isuc-pred, pred-isuc>>>
diff --git a/invariance.red b/invariance.red
index c5831c92d..2760806ab 100644
--- a/invariance.red
+++ b/invariance.red
@@ -27,11 +27,11 @@ let shannon (A : type) (f : bool → A) : bool → A =
 
 
 let shannon/path (A : type) (f : bool → A) : Path _ f (shannon A f) =
-  funext bool _ _ _
+  funext _ _ f (shannon A f)
     (λ b →
-      elim b in λ x → Path _ (f x) (shannon A f x) [
-      | tt ⇒ λ _ → f tt
-      | ff ⇒ λ _ → f ff
+      elim b [
+      | tt ⇒ auto
+      | ff ⇒ auto
       ])
 
 let fun-to-pair-is-equiv (A : type) : IsEquiv^1 (_ → _) _ (fun-to-pair A) =
@@ -45,8 +45,8 @@ let fun-to-pair-is-equiv (A : type) : IsEquiv^1 (_ → _) _ (fun-to-pair A) =
           >)
       in λ j →
         [i] (f : bool → A) × Path (A × A) <f tt, f ff> p [
-        | i=0 ⇒ < shannon/path A (fib.0) j, fib.1 >
-        | i=1 ⇒ < pair-to-fun A p, λ _ → p >
+        | i=0 ⇒ <shannon/path A (fib.0) j, fib.1>
+        | i=1 ⇒ <pair-to-fun A p, auto>
         ]
     >
 
diff --git a/isotoequiv.red b/isotoequiv.red
index 73922a121..b12a3b180 100644
--- a/isotoequiv.red
+++ b/isotoequiv.red
@@ -23,8 +23,8 @@ let Iso/fiber-is-prop
   let sq : (_ : Fiber _ _ (I.0) b) (i, j : dim) → A =
     λ fib i j →
       comp 0 j (g (fib.1 i)) [
-      | i=0 ⇒ λ k → β (fib.0) k
-      | i=1 ⇒ λ _ → g b
+      | i=0 ⇒ β (fib.0)
+      | i=1 ⇒ auto
       ]
   in
   λ fib0 fib1 →
@@ -36,21 +36,21 @@ let Iso/fiber-is-prop
         ]
     in
     λ i →
-     < sq2 i 0
+     < auto
      , λ j →
         let aux : A =
           comp 1 0 (sq2 i j) [
-          | i=0 ⇒ λ k → sq fib0 j k
-          | i=1 ⇒ λ k → sq fib1 j k
-          | j=0 ⇒ λ k → β (sq2 i 0) k
-          | j=1 ⇒ λ _ → g b
+          | i=0 ⇒ sq fib0 j
+          | i=1 ⇒ sq fib1 j
+          | j=0 ⇒ β (sq2 i 0)
+          | j=1 ⇒ auto
           ]
         in
         comp 0 1 (f aux) [
-        | i=0 ⇒ λ k → α (fib0.1 j) k
-        | i=1 ⇒ λ k → α (fib1.1 j) k
-        | j=0 ⇒ λ k → α (f (sq2 i 0)) k
-        | j=1 ⇒ λ k → α b k
+        | i=0 ⇒ α (fib0.1 j)
+        | i=1 ⇒ α (fib1.1 j)
+        | j=0 ⇒ α (f (sq2 i 0))
+        | j=1 ⇒ α b
         ]
      >
 
diff --git a/modal.red b/modal.red
index 94adde52e..bb771e928 100644
--- a/modal.red
+++ b/modal.red
@@ -30,57 +30,3 @@ let stream/tl (xs : stream) : ✓ → stream =
 let tts : _ =
   fix xs : stream in
     stream/cons tt xs
-
-
-; To eliminate a box, write 'b !'; this elaborates to the core term `(open b).
-let bool/constant (x : bool) : (b : □ bool) × Path _ x (b !) =
-  elim x [
-  | tt ⇒ < shut tt, λ _ → tt >
-  | ff ⇒ < shut ff, λ _ → ff >
-  ]
-
-let sequence : type = □ stream
-
-
-let Next (A : type) (x : A) ✓ : A =
-  x
-
-let sequence/cons (x : bool) (xs : sequence) : sequence =
-  shut
-    stream/cons
-      (bool/constant x .0 !)
-      (Next stream (xs !))
-      ; this is suspicious: we use this Next in order to essentially
-      ; weaken away the tick that we will not use, in order to get the right number
-      ; of locks deleted. But this is proof-theoretically very strange.
-
-; The proper solution to the problem above is to bind lock names in the syntax and in the context,
-; analogous to tick names. This will make the calculus more baroque, but it will enable a
-; deterministic version of the 'open' rule. The source term for the above would then be:
-;
-;     λ α → stream/cons (bool/constant x .0 α) (λ β → xs α)
-;
-; Above, α is a lock name and β is a tick name; opening with the lock α
-; would *delete* the tick β from the context (thinking backward), which is
-; a tick weakening. the example would typecheck because there is no need for
-; β in xs.
-;
-; For reference, the core-language term would look like the following:
-;
-;    (shut [α]
-;     (stream/cons
-;      (open α (car (bool/constant x)))
-;      (next [β] (open α xs))))
-
-
-
-let sequence/hd (xs : sequence) : bool =
-  stream/hd (xs !)
-
-let sequence/tl (xs : sequence) : sequence =
-  shut
-    stream/tl (xs !) ∙
-
-
-let law/k (A,B : type) (f : □ (A → B)) (x : □ A) : □ B =
-  shut f ! (x !)
diff --git a/nat.red b/nat.red
index 9d8416eb6..7dc57998e 100644
--- a/nat.red
+++ b/nat.red
@@ -13,7 +13,7 @@ let nat-pred (x : nat) : nat =
 
 
 let nat-pred/suc (x : nat) : Path nat x (nat-pred (suc x)) =
-  λ _ → x
+  auto
 
 let plus : nat → nat → nat =
   λ m n →
@@ -23,23 +23,23 @@ let plus : nat → nat → nat =
     ]
 
 let plus/unit/l (n : nat) : Path nat (plus zero n) n =
-  λ i → n
+  auto
 
 let plus/unit/r (n : nat) : Path nat (plus n zero) n =
   elim n [
-  | zero ⇒ λ _ → zero
+  | zero ⇒ auto
   | suc (n ⇒ path/n) ⇒ λ i → suc (path/n i)
   ]
 
 let plus/assoc (n : nat) : (m, o : nat) → Path nat (plus n (plus m o)) (plus (plus n m) o) =
   elim n [
-  | zero ⇒ λ m o i → plus m o
+  | zero ⇒ auto
   | suc (n ⇒ plus/assoc/n) ⇒ λ m o i → suc (plus/assoc/n m o i)
   ]
 
 let plus/suc/r (n : nat) : (m : nat) → Path nat (plus n (suc m)) (suc (plus n m)) =
   elim n [
-  | zero ⇒ λ m _ → suc m
+  | zero ⇒ auto
   | suc (n ⇒ plus/n/suc/r) ⇒ λ m i → suc (plus/n/suc/r m i)
   ]
 
diff --git a/omega1s1-wip.red b/omega1s1-wip.red
index 5b360c638..55fc638c0 100644
--- a/omega1s1-wip.red
+++ b/omega1s1-wip.red
@@ -16,7 +16,7 @@ let loopn (n : int) : Path s1 base base =
   elim n [
   | pos n ⇒
     elim n [
-    | zero ⇒ λ _ → base
+    | zero ⇒ auto
     | suc (n ⇒ loopn) ⇒ trans s1 (λ i → loop i) loopn
     ]
   | negsuc n ⇒
@@ -32,7 +32,7 @@ let winding (l : Path s1 base base) : int =
 let two : int = pos (suc (suc zero))
 
 let winding-loop-testing0 : Path int two (winding (loopn two)) =
-  λ _ → two
+  auto
 
 let nat/five : nat =
   suc (suc (suc (suc (suc zero))))
@@ -46,8 +46,8 @@ let int/50 : int =
 let int/5 : int = pos nat/five
 
 let winding-test/5 : Path int int/5 (winding (loopn int/5)) =
-  λ _ → int/5
+  auto
 
 let winding-test/50 : Path int int/50 (winding (loopn int/50)) =
-  λ _ → int/50
+  auto
 
diff --git a/path.red b/path.red
index 5b01be645..12a0226fe 100644
--- a/path.red
+++ b/path.red
@@ -32,7 +32,7 @@ let funext
   : Path ((x : A) → B x) f g
   =
   λ i x →
-    p x i
+    p _ i
 
 let symm/filler
   (A : type)
@@ -41,8 +41,8 @@ let symm/filler
   : A
   =
   comp 0 j (p 0) [
-  | i=0 ⇒ λ i → p i
-  | i=1 ⇒ λ _ → p 0
+  | i=0 ⇒ p
+  | i=1 ⇒ auto
   ]
 
 let symm
@@ -50,16 +50,14 @@ let symm
   (p : dim → A)
   : Path A (p 1) (p 0)
   =
-  λ i →
-    symm/filler _ p 1 i
+  symm/filler _ p 1
 
 let symm/unit
   (A : type)
   (a : A)
-  : (Path (Path _ a a) (λ _ → a) (symm _ (λ _ → a)))
+  : Path (Path _ a a) auto (symm _ (λ _ → a))
   =
-  λ i j →
-    symm/filler _ (λ _ → a) i j
+  symm/filler _ (λ _ → a)
 
 let trans/filler
   (A : type)
@@ -69,8 +67,8 @@ let trans/filler
   : A
   =
   comp 0 j (p i) [
-  | i=0 ⇒ λ _ → p 0
-  | i=1 ⇒ λ i → q i
+  | i=0 ⇒ auto
+  | i=1 ⇒ q
   ]
 
 let trans
@@ -79,28 +77,26 @@ let trans
   (q : [i] A [ i=0 ⇒ p 1 ])
   : Path _ (p 0) (q 1)
   =
-  λ i →
-    trans/filler _ p q 1 i
+  trans/filler _ p q 1
 
 let trans/unit/r
   (A : type)
   (p : dim → A)
-  : Path (Path _ (p 0) (p 1)) (λ i → p i) (trans _ p (λ _ → p 1))
+  : Path (Path _ (p 0) (p 1)) p (trans _ p (λ _ → p 1))
   =
-  λ i j →
-    trans/filler _ p (λ _ → p 1) i j
+  trans/filler _ p (λ _ → p 1)
 
 ; This proof gets simpler when dead tubes are deleted!
 let trans/sym/r
   (A : type)
   (p : dim → A)
-  : Path (Path _ (p 0) (p 0)) (λ _ → p 0) (trans _ p (symm _ p))
+  : Path (Path _ (p 0) (p 0)) auto (trans _ p (symm _ p))
   =
   λ k i →
     comp 0 1 (p i) [
-    | i=0 ⇒ λ _ → p 0
-    | i=1 ⇒ λ j → symm A p j
-    | k=0 ⇒ λ j → symm/filler A p i j
+    | i=0 ⇒ auto
+    | i=1 ⇒ symm A p
+    | k=0 ⇒ symm/filler A p i
     ;| k=1 ⇒ λ j → trans/filler A p (symm A p) j i
     ]
 
@@ -112,6 +108,6 @@ let symmd
   =
   λ i →
     comp 0 1 (p 0) in (λ j → symm/filler^1 _ A j i) [
-    | i=0 ⇒ λ j → p j
-    | i=1 ⇒ λ _ → p 0
+    | i=0 ⇒ p
+    | i=1 ⇒ auto
     ]
diff --git a/src/basis/Bwd.ml b/src/basis/Bwd.ml
index 16c846cb7..9e78f2a60 100644
--- a/src/basis/Bwd.ml
+++ b/src/basis/Bwd.ml
@@ -29,6 +29,13 @@ module Bwd =
 struct
   open BwdNotation
 
+  let rec nth xs i =
+    match xs with
+    | Emp ->
+      failwith "Bwd.nth"
+    | Snoc (_, x) when i = 0 -> x
+    | Snoc (xs, _) -> nth xs @@ i - 1
+
 
   let rec length =
     function
diff --git a/src/basis/Bwd.mli b/src/basis/Bwd.mli
index 6dff950e0..7ecd6f6d0 100644
--- a/src/basis/Bwd.mli
+++ b/src/basis/Bwd.mli
@@ -15,6 +15,7 @@ end
 
 module Bwd :
 sig
+  val nth : 'a bwd -> int -> 'a
   val rev : 'a bwd -> 'a bwd
   val length : 'a bwd -> int
   val map : ('a -> 'b) -> 'a bwd -> 'b bwd
diff --git a/src/basis/ListUtil.ml b/src/basis/ListUtil.ml
index 7c57ece1f..0e446f70d 100644
--- a/src/basis/ListUtil.ml
+++ b/src/basis/ListUtil.ml
@@ -26,3 +26,10 @@ let rec map3 f xs ys zs =
     f x y z :: map3 f xs ys zs
   | _ ->
     failwith "map3: length mismatch"
+
+let tabulate n f =
+  let rec go i =
+    if i == n then [] else
+      f i :: go (i+1)
+  in
+  go 0
diff --git a/src/basis/Monad.ml b/src/basis/Monad.ml
index 06394c044..8cfddaa13 100644
--- a/src/basis/Monad.ml
+++ b/src/basis/Monad.ml
@@ -52,8 +52,17 @@ struct
   let rec traverse f =
     function
     | [] -> M.ret []
-    | m::ms ->
-      m >>= fun x ->
-      traverse f ms >>= fun xs ->
-      M.ret @@ x :: xs
+    | x::xs ->
+      f x >>= fun y ->
+      traverse f xs >>= fun ys ->
+      M.ret @@ y :: ys
+
+  let rec fold_left f acc xs =
+    match xs with
+    | [] ->
+      M.ret acc
+    | x :: xs ->
+      f acc x >>= fun a ->
+      fold_left f a xs
+
 end
diff --git a/src/basis/Monad.mli b/src/basis/Monad.mli
index 43920fc46..563b055d6 100644
--- a/src/basis/Monad.mli
+++ b/src/basis/Monad.mli
@@ -22,6 +22,7 @@ module Notation (M : S) : Notation with type 'a m := 'a M.m
 
 module Util (M : S) :
 sig
-  val traverse : ('a -> 'b) -> 'a M.m list -> 'a list M.m
+  val traverse : ('a -> 'b M.m) -> 'a list -> 'b list M.m
+  val fold_left : ('a -> 'b -> 'a M.m) -> 'a -> 'b list -> 'a M.m
 end
 
diff --git a/src/core/Cx.ml b/src/core/Cx.ml
index 586253be1..a305fc013 100644
--- a/src/core/Cx.ml
+++ b/src/core/Cx.ml
@@ -23,8 +23,7 @@ type cx =
    env : Domain.env;
    qenv : Quote.env;
    ppenv : Pp.env;
-   rel : Restriction.t;
-   all_locks : int}
+   rel : Restriction.t}
 
 type t = cx
 
@@ -39,31 +38,7 @@ let clear_locals cx =
    qenv = Quote.Env.emp;
    hyps = [];
    ppenv = Pp.Env.emp;
-   env = Domain.Env.clear_locals cx.env;
-   all_locks = 0}
-let ext_lock cx =
-  {cx with
-   sign = GlobalEnv.ext_lock cx.sign;
-   hyps = List.map (fun hyp -> {hyp with locked = true}) cx.hyps;
-   all_locks = cx.all_locks + 1}
-
-let hyps_clear_locks hyps =
-  let rec go hyps =
-    match hyps with
-    | [] -> []
-    | hyp :: hyps ->
-      match hyp.classifier with
-      | `Tick -> hyp :: hyps (* Maybe not quite right *)
-      | _ ->
-        {hyp with locked = false} :: go hyps
-  in
-  go hyps
-
-let clear_locks cx =
-  {cx with
-   sign = GlobalEnv.clear_locks cx.sign;
-   hyps = hyps_clear_locks cx.hyps;
-   all_locks = 0}
+   env = Domain.Env.clear_locals cx.env}
 
 let kill_from_tick cx tgen =
   match tgen with
@@ -144,7 +119,6 @@ let lookup i {hyps; _} =
     hyp.classifier
 
 let lookup_constant nm tw cx =
-  (* For constants, the only locks that are relevant are the global ones. Ignore the local locks. *)
   GlobalEnv.lookup_ty cx.sign nm tw
 
 let restrict cx r r' =
@@ -205,6 +179,9 @@ let quote_ty cx ty =
   let (module Q) = quoter cx in
   Q.quote_ty cx.qenv ty
 
+let quote_dim cx r =
+  let (module Q) = quoter cx in
+  Q.quote_dim cx.qenv r
 
 let check_eq cx ~ty el0 el1 =
   let (module Q) = quoter cx in
@@ -228,5 +205,4 @@ let init globals =
    qenv = Quote.Env.emp;
    hyps = [];
    ppenv = Pp.Env.emp;
-   rel = GlobalEnv.restriction globals;
-   all_locks = 0}
+   rel = GlobalEnv.restriction globals}
diff --git a/src/core/Cx.mli b/src/core/Cx.mli
index 1785566a2..58134d4bb 100644
--- a/src/core/Cx.mli
+++ b/src/core/Cx.mli
@@ -10,10 +10,7 @@ val qenv : t -> Quote.env
 
 val clear_locals : t -> t
 
-(* Modal left adjoints *)
-val ext_lock : t -> t
-val clear_locks : t -> t
-
+(* Modal *)
 val kill_from_tick : t -> Domain.tick_gen -> t
 
 val ext_ty : t -> nm:string option -> value -> t * value
@@ -51,6 +48,7 @@ val check_eq : t -> ty:value -> value -> value -> unit
 val check_subtype : t -> value -> value -> unit
 val quote : t -> ty:value -> value -> Tm.tm
 val quote_ty : t -> value -> Tm.tm
+val quote_dim : t -> I.t -> Tm.tm
 val check_eq_ty : t -> value -> value -> unit
 
 val evaluator : t -> (module Val.S)
diff --git a/src/core/Domain.ml b/src/core/Domain.ml
index 7b186682b..c48ee9355 100644
--- a/src/core/Domain.ml
+++ b/src/core/Domain.ml
@@ -24,9 +24,9 @@ let rec pp_env_cell fmt =
   | `Tick _ ->
     Format.fprintf fmt "<tick>"
 
-and pp_env fmt =
+and pp_env fmt env =
   let pp_sep fmt () = Format.fprintf fmt ", " in
-  Format.pp_print_list ~pp_sep pp_env_cell fmt
+  Format.pp_print_list ~pp_sep pp_env_cell fmt env.cells
 
 
 and pp_con fmt : con -> unit =
@@ -93,10 +93,6 @@ and pp_con fmt : con -> unit =
     Format.fprintf fmt "<dfix>"
   | DFixLine _ ->
     Format.fprintf fmt "<dfix-line>"
-  | BoxModality _ ->
-    Format.fprintf fmt "<box-modality>"
-  | Shut _ ->
-    Format.fprintf fmt "<shut>"
   | Data lbl ->
     Uuseg_string.pp_utf_8 fmt lbl
   | Intro info ->
@@ -164,11 +160,11 @@ and pp_comp_face : type x. _ -> (x, abs) face -> unit =
 
 and pp_clo fmt (Clo clo) =
   let Tm.B (_, tm) = clo.bnd in
-  Format.fprintf fmt "<clo %a & %a>" Tm.pp0 tm pp_env clo.rho.cells
+  Format.fprintf fmt "<clo %a & %a>" Tm.pp0 tm pp_env clo.rho
 
 and pp_nclo fmt (NClo clo) =
   let Tm.NB (_, tm) = clo.nbnd in
-  Format.fprintf fmt "<clo %a & %a>" Tm.pp0 tm pp_env clo.rho.cells
+  Format.fprintf fmt "<clo %a & %a>" Tm.pp0 tm pp_env clo.rho
 
 and pp_neu fmt neu =
   match neu with
@@ -190,6 +186,10 @@ and pp_neu fmt neu =
     let r, r' = Dir.unleash info.dir in
     Format.fprintf fmt "@[<1>(ncoe %a %a@ %a@ %a)@]" I.pp r I.pp r' pp_abs info.abs pp_neu info.neu
 
+  | NCoeAtType info ->
+    let r, r' = Dir.unleash info.dir in
+    Format.fprintf fmt "@[<1>(ncoe %a %a@ %a@ %a)@]" I.pp r I.pp r' pp_abs info.abs pp_value info.el
+
   | FunApp (neu, arg) ->
     Format.fprintf fmt "@[<1>(%a@ %a)@]" pp_neu neu pp_value arg.el
 
@@ -236,9 +236,6 @@ and pp_neu fmt neu =
   | FixLine _ ->
     Format.fprintf fmt "<fix-line>"
 
-  | Open _ ->
-    Format.fprintf fmt "<open>"
-
 and pp_elim_clauses fmt clauses =
   let pp_sep fmt () = Format.fprintf fmt "@ " in
   Format.pp_print_list ~pp_sep pp_elim_clause fmt clauses
@@ -421,7 +418,6 @@ end
 module ExtAbs : IAbs.S with type el = value * val_sys =
   IAbs.M (Sort.Prod (Value) (ValSys))
 
-
 module Env :
 sig
   include Sort.S
diff --git a/src/core/Domain.mli b/src/core/Domain.mli
index 47f27985e..c0358540b 100644
--- a/src/core/Domain.mli
+++ b/src/core/Domain.mli
@@ -14,6 +14,12 @@ val pp_val_sys : Format.formatter -> ('x, value) face list -> unit
 val pp_comp_sys : Format.formatter -> comp_sys -> unit
 val pp_names : Format.formatter -> Name.t bwd -> unit
 
+val pp_clo : Format.formatter -> clo -> unit
+val pp_nclo : Format.formatter -> nclo -> unit
+
+val pp_env_cell : Format.formatter -> env_el -> unit
+val pp_env : Format.formatter -> env -> unit
+
 
 exception ProjAbs of abs
 exception ProjVal of value
diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml
index 2606b4fe6..dcbdd7921 100644
--- a/src/core/DomainData.ml
+++ b/src/core/DomainData.ml
@@ -8,7 +8,6 @@ type tick_gen =
   [`Lvl of string option * int | `Global of Name.t ]
 
 type tick =
-  | TickConst
   | TickGen of tick_gen
 
 
@@ -44,9 +43,6 @@ type con =
   | DFix of {ty : value; clo : clo}
   | DFixLine of {x : atom; ty : value; clo : clo}
 
-  | BoxModality of value
-  | Shut of value
-
   | Data of Desc.data_label
   | Intro of
       {dlbl : Desc.data_label;
@@ -65,6 +61,9 @@ and neu =
   | NHComAtCap of {dir : dir; ty : value; cap : neu; sys : comp_sys}
   | NCoe of {dir : dir; abs : abs; neu : neu}
 
+  | NCoeAtType of {dir : dir; abs : abs; el : value}
+  (** Invariant: [abs] always has a neutral interior *)
+
   | FunApp of neu * nf
   | ExtApp of neu * dim list
   | Car of neu
@@ -87,8 +86,6 @@ and neu =
   | Fix of tick_gen * value * clo
   | FixLine of atom * tick_gen * value * clo
 
-  | Open of neu
-
 and nf = {ty : value; el : value}
 
 and abs = value IAbs.abs
diff --git a/src/core/GlobalEnv.ml b/src/core/GlobalEnv.ml
index a997c47d4..93f967255 100644
--- a/src/core/GlobalEnv.ml
+++ b/src/core/GlobalEnv.ml
@@ -16,7 +16,6 @@ type t =
   {rel : Restriction.t;
    data_decls : (Tm.tm, Tm.tm Desc.Boundary.term) Desc.desc StringTable.t;
    table : (entry param * lock_info) T.t;
-   lock : int -> bool;
    killed : int -> bool;
    under_tick : int -> bool;
    len : int}
@@ -26,7 +25,6 @@ let emp () =
   {table = T.empty;
    data_decls = StringTable.empty;
    rel = Restriction.emp ();
-   lock = (fun _ -> false);
    killed = (fun _ -> false);
    under_tick = (fun _ -> false);
    len = 0}
@@ -73,15 +71,6 @@ let ext_dim (sg : t) nm : t =
   ext_ sg ~constant:false nm `I
 
 
-let ext_lock (sg : t) : t =
-  {sg with
-   lock = fun i -> if i < sg.len then true else sg.lock i}
-
-let clear_locks (sg : t) : t =
-  {sg with
-   lock = (fun i -> if sg.under_tick i then sg.lock i else false)}
-
-
 let rec index_of pred xs =
   match xs with
   | [] -> failwith "index_of"
@@ -97,9 +86,8 @@ let kill_from_tick (sg : t) nm : t =
 
 let lookup_entry sg nm tw =
   let prm, linfo = T.find nm sg.table in
-  let locked = sg.lock linfo.birth in
   let killed = sg.killed linfo.birth in
-  if not linfo.constant && (locked || killed) then
+  if not linfo.constant && killed then
     failwith "GlobalEnv.lookup_entry: not accessible (modal!!)"
   else
     match prm, tw with
@@ -130,7 +118,10 @@ let restrict tr0 tr1 sg =
     | Tm.Up (Tm.Var {name; _}, Emp) -> `Atom name
     | Tm.Dim0 -> `Dim0
     | Tm.Dim1 -> `Dim1
-    | _ -> failwith "Restrict: expected dimension"
+    | _ ->
+      Printexc.print_raw_backtrace stderr (Printexc.get_callstack 20);
+      Format.eprintf "@.";
+      failwith "Restrict: expected dimension"
   in
   let rel', _ = Restriction.equate (ev_dim tr0) (ev_dim tr1) sg.rel in
   {sg with rel = rel'}
@@ -142,7 +133,7 @@ let pp fmt sg =
     | `Tw _ ->
       Format.fprintf fmt "%a[twin]"
         Name.pp nm
-    | (`Tick | `I | `P _) ->
+    | (`Tick | `I | `P _ | `Def _) ->
       Format.fprintf fmt "%a"
         Name.pp nm
   in
diff --git a/src/core/GlobalEnv.mli b/src/core/GlobalEnv.mli
index 1f0ef8afa..d08593759 100644
--- a/src/core/GlobalEnv.mli
+++ b/src/core/GlobalEnv.mli
@@ -15,9 +15,7 @@ val ext : t -> Name.t -> entry param -> t
 val ext_meta : t -> Name.t -> entry param -> t
 val ext_dim : t -> Name.t -> t
 val ext_tick : t -> Name.t -> t
-val ext_lock : t -> t
 val restrict : Tm.tm -> Tm.tm -> t -> t
-val clear_locks : t -> t
 val kill_from_tick : t -> Name.t -> t
 
 
diff --git a/src/core/Kind.mli b/src/core/Kind.mli
new file mode 100644
index 000000000..ec906caa7
--- /dev/null
+++ b/src/core/Kind.mli
@@ -0,0 +1,4 @@
+type t = [`Reg | `Kan | `Pre]
+
+val lte : t -> t -> bool
+val pp : t Pp.t0
diff --git a/src/core/Lvl.mli b/src/core/Lvl.mli
new file mode 100644
index 000000000..49e23d8a5
--- /dev/null
+++ b/src/core/Lvl.mli
@@ -0,0 +1,6 @@
+type t = [`Omega | `Const of int]
+
+val greater : t -> t -> bool
+val lte : t -> t -> bool
+val shift : int -> t -> t
+val pp : t Pp.t0
diff --git a/src/core/Pp.ml b/src/core/Pp.ml
index 3164dcd52..6656de1f7 100644
--- a/src/core/Pp.ml
+++ b/src/core/Pp.ml
@@ -42,3 +42,8 @@ type env = Env.t
 
 type 'a t0 = Format.formatter -> 'a -> unit
 type 'a t = env -> 'a t0
+
+let pp_list pp fmt xs =
+  let pp_sep fmt () = Format.fprintf fmt ", " in
+  Format.fprintf fmt "@[<hv1>[%a]@]"
+    (Format.pp_print_list ~pp_sep pp) xs
diff --git a/src/core/Pp.mli b/src/core/Pp.mli
index 1baa561bc..1169cc84c 100644
--- a/src/core/Pp.mli
+++ b/src/core/Pp.mli
@@ -14,3 +14,5 @@ type env = Env.t
 
 type 'a t0 = Format.formatter -> 'a -> unit
 type 'a t = env -> 'a t0
+
+val pp_list : 'a t0 -> 'a list t0
diff --git a/src/core/Quote.ml b/src/core/Quote.ml
index d1cbfc415..b7bd447b2 100644
--- a/src/core/Quote.ml
+++ b/src/core/Quote.ml
@@ -70,6 +70,8 @@ sig
   val quote_ty : env -> value -> Tm.tm
   val quote_val_sys : env -> value -> val_sys -> (Tm.tm, Tm.tm) Tm.system
 
+  val quote_dim : env -> I.t -> Tm.tm
+
   val equiv : env -> ty:value -> value -> value -> unit
   val equiv_ty : env -> value -> value -> unit
   val subtype : env -> value -> value -> unit
@@ -176,12 +178,6 @@ struct
       let bdy = equate (Env.succ env) ty prev0 prev1 in
       Tm.make @@ Tm.Next (Tm.B (None, bdy))
 
-    | BoxModality ty ->
-      let open0 = modal_open el0 in
-      let open1 = modal_open el1 in
-      let t = equate env ty open0 open1 in
-      Tm.make @@ Tm.Shut t
-
     | Rst {ty; _} ->
       equate env ty el0 el1
 
@@ -256,10 +252,6 @@ struct
         let cod = equate (Env.succ env) ty vcod0 vcod1 in
         Tm.make @@ Tm.Later (Tm.B (None, cod))
 
-      | _, BoxModality ty0, BoxModality ty1 ->
-        let ty = equate env ty ty0 ty1 in
-        Tm.make @@ Tm.BoxModality ty
-
       | _, Sg sg0, Sg sg1 ->
         let dom = equate env ty sg0.dom sg1.dom in
         let var = generic env sg0.dom in
@@ -368,6 +360,9 @@ struct
         Tm.make @@ Tm.Intro (dlbl, info0.clbl, const_args @ rec_args @ trs)
 
       | _ ->
+        (* For more readable error messages *)
+        let el0 = D.make @@ V.unleash el0 in
+        let el1 = D.make @@ V.unleash el1 in
         let err = ErrEquateNf {env; ty; el0; el1} in
         raise @@ E err
 
@@ -434,6 +429,16 @@ struct
       let tm = equate_neu env info0.neu info1.neu in
       Tm.Coe {r = tr; r' = tr'; ty = bnd; tm = Tm.up tm}, Bwd.from_list stk
 
+    | NCoeAtType info0, NCoeAtType info1 ->
+      let tr, tr' = equate_dir env info0.dir info1.dir in
+      let univ = make @@ Univ {kind = `Pre; lvl = `Omega} in
+      let bnd = equate_val_abs env univ info0.abs info1.abs in
+      let r, _ = Dir.unleash info0.dir in
+      let ty_r = Abs.inst1 info0.abs r in
+      let tm = equate env ty_r info0.el info1.el in
+      Tm.Coe {r = tr; r' = tr'; ty = bnd; tm}, Bwd.from_list stk
+
+
     | Fix (tgen0, ty0, clo0), Fix (tgen1, ty1, clo1) ->
       let ty = equate_ty env ty0 ty1 in
       let ltr_ty = make_later ty0 in
@@ -484,9 +489,17 @@ struct
 
         let desc = V.Sig.lookup_datatype dlbl in
 
+        let find_clause clbl clauses =
+          try
+            snd @@ List.find (fun (clbl', _) -> clbl = clbl') clauses
+          with
+          | Not_found ->
+            failwith "Quote: elim / find_clause"
+        in
+
         let quote_clause (clbl, constr) =
-          let _, clause0 = List.find (fun (clbl', _) -> clbl = clbl') elim0.clauses in
-          let _, clause1 = List.find (fun (clbl', _) -> clbl = clbl') elim1.clauses in
+          let clause0 = find_clause clbl elim0.clauses in
+          let clause1 = find_clause clbl elim1.clauses in
           let env', vs, cvs, rvs, rs =
             let open Desc in
             let rec build_cx qenv env (vs, cvs, rvs) rs const_specs rec_specs dim_specs =
@@ -501,10 +514,12 @@ struct
                 let qenv' = Env.succ qenv in
                 let vih = generic qenv' @@ V.inst_clo elim0.mot vx in
                 build_cx (Env.succ qenv') env (vs #< vx #< vih, cvs, rvs #< vx) rs const_specs rec_specs dim_specs
-              | [], [], dims ->
-                let xs = Bwd.map (fun x -> Name.named @@ Some x) @@ Bwd.from_list dims in
-                let qenv' = Env.abs qenv xs in
-                qenv', Bwd.to_list vs, Bwd.to_list cvs, Bwd.to_list rvs, Bwd.to_list rs
+              | [], [], nm :: dim_specs ->
+                let x = Name.named @@ Some nm in
+                let qenv' = Env.abs qenv (Emp #< x) in
+                build_cx qenv' env (vs, cvs, rvs) (rs #< (`Atom x)) const_specs rec_specs dim_specs
+              | [], [], [] ->
+                qenv, Bwd.to_list vs, Bwd.to_list cvs, Bwd.to_list rvs, Bwd.to_list rs
             in
             build_cx env D.Env.emp (Emp, Emp, Emp) Emp constr.const_specs constr.rec_specs constr.dim_specs
           in
@@ -514,7 +529,8 @@ struct
           let intro = make_intro D.Env.emp ~dlbl ~clbl ~const_args:cvs ~rec_args:rvs ~rs in
           let mot_intro = inst_clo elim0.mot intro in
           let tbdy = equate env' mot_intro bdy0 bdy1 in
-          clbl, Tm.NB (Bwd.map (fun _ -> None) @@ Bwd.from_list vs, tbdy)
+          let nms = Bwd.from_list @@ ListUtil.tabulate (List.length cells) @@ fun _ -> None in
+          clbl, Tm.NB (nms, tbdy)
         in
 
         let clauses = List.map quote_clause desc.constrs in
@@ -553,9 +569,6 @@ struct
       let tick = equate_tick env tick0 tick1 in
       equate_neu_ env neu0 neu1 @@ Tm.Prev tick :: stk
 
-    | Open neu0, Open neu1 ->
-      equate_neu_ env neu0 neu1 @@ Tm.Open :: stk
-
     | _ ->
       let err = ErrEquateNeu {env; neu0; neu1} in
       raise @@ E err
@@ -690,7 +703,8 @@ struct
     | `Same ->
       quote_dim env r
     | _ ->
-      (* Printexc.print_raw_backtrace stderr (Printexc.get_callstack 20);
+      (*
+         Printexc.print_raw_backtrace stderr (Printexc.get_callstack 20);
          Format.eprintf "@.";
          Format.eprintf "Dimension mismatch: %a <> %a@." I.pp r I.pp r'; *)
       failwith "equate_dim: dimensions did not match"
@@ -701,7 +715,8 @@ struct
     | `Same, `Same ->
       quote_dim env r
     | _ ->
-      (* Printexc.print_raw_backtrace stderr (Printexc.get_callstack 20);
+      (*
+         Printexc.print_raw_backtrace stderr (Printexc.get_callstack 20);
          Format.eprintf "@.";
          Format.eprintf "Dimension mismatch: %a <> %a@." I.pp r I.pp r'; *)
       failwith "equate_dim3: dimensions did not match"
@@ -736,8 +751,6 @@ struct
 
   and quote_tick env tck =
     match tck with
-    | TickConst ->
-      Tm.make Tm.TickConst
     | TickGen (`Lvl (_, lvl)) ->
       let ix = Env.ix_of_lvl lvl env in
       Tm.up @@ Tm.ix ix
@@ -804,11 +817,6 @@ struct
       let sys1 = map_sys (fun _ _ -> prev tick) sys1 in
       fancy_subtype (Env.succ env) vcod0 sys0 vcod1 sys1
 
-    | BoxModality ty0, BoxModality ty1 ->
-      let sys0 = map_sys (fun _ _ -> modal_open) sys0 in
-      let sys1 = map_sys (fun _ _ -> modal_open) sys1 in
-      fancy_subtype env ty0 sys0 ty1 sys1
-
     | Ext abs0, Ext abs1 ->
       let xs, (ty0x, sys0x) = ExtAbs.unleash abs0 in
       let rs = Bwd.map (fun x -> `Atom x) xs in
diff --git a/src/core/Quote.mli b/src/core/Quote.mli
index b6bd70de8..2c09f5a3f 100644
--- a/src/core/Quote.mli
+++ b/src/core/Quote.mli
@@ -31,6 +31,8 @@ sig
   val quote_ty : env -> value -> Tm.tm
   val quote_val_sys : env -> value -> val_sys -> (Tm.tm, Tm.tm) Tm.system
 
+  val quote_dim : env -> I.t -> Tm.tm
+
   val equiv : env -> ty:value -> value -> value -> unit
   val equiv_ty : env -> value -> value -> unit
   val subtype : env -> value -> value -> unit
diff --git a/src/core/Tm.ml b/src/core/Tm.ml
index 2de5aed1a..5520e4201 100644
--- a/src/core/Tm.ml
+++ b/src/core/Tm.ml
@@ -4,6 +4,12 @@ open BwdNotation
 
 include TmData
 
+type tm = Tm of tm tmf
+type btm = tm Desc.Boundary.term
+type bface = (tm, btm) Desc.Boundary.face
+type bsys = (tm, btm) Desc.Boundary.sys
+type data_desc = (tm, btm) Desc.desc
+
 type 'a subst =
   | Shift of int
   | Dot of 'a * 'a subst
@@ -13,8 +19,6 @@ let shift i = Shift i
 let dot a sb = Dot (a, sb)
 
 
-type tm = Tm of tm tmf
-
 type error =
   | InvalidDeBruijnIndex of int
   | UnbindExtLengthMismatch of tm cmd list * (tm * (tm, tm) system) nbnd
@@ -56,7 +60,7 @@ struct
 
   and traverse_con =
     function
-    | (Univ _ | Dim0 | Dim1 | TickConst as con) ->
+    | (Univ _ | Dim0 | Dim1 as con) ->
       con
 
     | FHCom info ->
@@ -147,14 +151,6 @@ struct
       let bnd' = traverse_bnd traverse_tm bnd in
       Next bnd'
 
-    | BoxModality t ->
-      let t' = traverse_tm t in
-      BoxModality t'
-
-    | Shut t ->
-      let t' = traverse_tm t in
-      Shut t'
-
     | Let (cmd, bnd) ->
       let cmd' = traverse_cmd cmd in
       let bnd' = traverse_bnd traverse_tm bnd in
@@ -347,9 +343,6 @@ struct
       let tick = traverse_tm tick in
       Prev tick
 
-    | Open ->
-      Open
-
 end
 
 
@@ -452,6 +445,10 @@ let make con =
   match con with
   | Up (Ix (ix, _), _) when ix < 0 ->
     raise @@ E (InvalidDeBruijnIndex ix)
+  | Up (Down {tm = Tm (Up (hd, sp)); _}, sp') ->
+    Tm (Up (hd, sp <.> sp'))
+  | Up (Down {tm; _}, Emp) ->
+    tm
   | _ -> Tm con
 
 let unleash (Tm con) = con
@@ -651,9 +648,9 @@ let rec pp env fmt =
       begin
         match sys with
         | [] ->
-          Format.fprintf fmt "%a" (pp env) ty
+          Format.fprintf fmt "@[<hv1>(restrict %a)]" (pp env) ty
         | _ ->
-          Format.fprintf fmt "@[<hv1>(%a@ @[<hv>%a@])@]" (pp env) ty (pp_sys env) sys
+          Format.fprintf fmt "@[<hv1>(restrict %a@ @[<hv>%a@])@]" (pp env) ty (pp_sys env) sys
       end
 
     | CoR face ->
@@ -688,9 +685,6 @@ let rec pp env fmt =
     | Dim1 ->
       Format.fprintf fmt "1"
 
-    | TickConst ->
-      Uuseg_string.pp_utf_8 fmt "∙"
-
     | Univ {kind; lvl} ->
       Format.fprintf fmt "(U %a %a)" Kind.pp kind Lvl.pp lvl
 
@@ -729,12 +723,6 @@ let rec pp env fmt =
       let x, env' = Pp.Env.bind nm env in
       Format.fprintf fmt "@[<hv1>(next [%a]@ %a)@]" Uuseg_string.pp_utf_8 x (pp env') t
 
-    | BoxModality t ->
-      Format.fprintf fmt "@[<hv1>(%a@ %a)@]" Uuseg_string.pp_utf_8 "□" (pp env) t
-
-    | Shut t ->
-      Format.fprintf fmt "@[<hv1>(shut@ %a)@]" (pp env) t
-
     | Let (cmd, B (nm, t)) ->
       let x, env' = Pp.Env.bind nm env in
       Format.fprintf fmt "@[<hv1>(let@ @[<hv1>[%a %a]@]@ %a)@]" Uuseg_string.pp_utf_8 x (pp_cmd env) cmd (pp env') t
@@ -842,8 +830,6 @@ and pp_cmd env fmt (hd, sp) =
         Format.fprintf fmt "@[<hv1>(force@ %a)@]" (go `Force) sp
       | Prev tick ->
         Format.fprintf fmt "@[<hv1>(prev %a@ %a)@]" (pp env) tick (go `Prev) sp
-      | Open ->
-        Format.fprintf fmt "@[<hv1>(open@ %a)@]" (go `Open) sp
   in
   go `Start fmt sp
 
@@ -1171,8 +1157,6 @@ let map_frame f =
   | Prev tick ->
     let tick = f tick in
     Prev tick
-  | Open ->
-    Open
 
 let map_spine f =
   Bwd.map @@ map_frame f
@@ -1195,7 +1179,7 @@ let map_cmd f (hd, sp) =
 
 let map_tmf f =
   function
-  | (Univ _ | Dim0 | Dim1 | TickConst | Data _) as con ->
+  | (Univ _ | Dim0 | Dim1 | Data _) as con ->
     con
   | Cons (t0, t1) ->
     Cons (f t0, f t1)
@@ -1250,12 +1234,6 @@ let map_tmf f =
   | Next bnd ->
     let bnd = map_bnd f bnd in
     Next bnd
-  | BoxModality t ->
-    let t = f t in
-    BoxModality t
-  | Shut t ->
-    let t = f t in
-    Shut t
   | Up cmd ->
     Up (map_cmd f cmd)
   | Let (cmd, bnd) ->
@@ -1326,16 +1304,6 @@ let rec eta_contract t =
         make @@ Next (bind y tm'y)
     end
 
-  | Shut tm ->
-    let tm' = eta_contract tm in
-    begin
-      match unleash tm' with
-      | Up (hd, Snoc (sp, Open)) ->
-        up (hd, sp)
-      | _ ->
-        make @@ Shut tm'
-    end
-
   | ExtLam nbnd ->
     let ys, tmys = unbindn nbnd in
     let tm'ys = eta_contract tmys in
@@ -1391,6 +1359,13 @@ let rec shift_univ k tm =
     | tmf ->
       Tm (map_tmf (shift_univ k) tmf)
 
+let pp_bterm fmt =
+  let module B = Desc.Boundary in
+  function
+  | B.Var ix ->
+    Format.fprintf fmt "#%i" ix
+  | B.Intro intro ->
+    Format.fprintf fmt "<intro: %s>" intro.clbl
 
 let pp0 fmt tm = pp Pp.Env.emp fmt @@ eta_contract tm
 
diff --git a/src/core/Tm.mli b/src/core/Tm.mli
index 59b59df51..0ab27274c 100644
--- a/src/core/Tm.mli
+++ b/src/core/Tm.mli
@@ -1,7 +1,12 @@
 open RedBasis.Bwd
 include module type of TmData
 
+
 type tm
+type btm = tm Desc.Boundary.term
+type bsys = (tm, btm) Desc.Boundary.sys
+type bface = (tm, btm) Desc.Boundary.face
+type data_desc = (tm, btm) Desc.desc
 
 module Error :
 sig
@@ -85,6 +90,8 @@ val pp_frame : tm frame Pp.t
 val pp_spine : tm spine Pp.t
 val pp_sys : (tm, tm) system Pp.t
 
+val pp_bterm : btm Pp.t0
+
 include Occurs.S with type t := tm
 
 module Sp :
diff --git a/src/core/TmData.ml b/src/core/TmData.ml
index eb86e458f..cd0105eee 100644
--- a/src/core/TmData.ml
+++ b/src/core/TmData.ml
@@ -30,7 +30,6 @@ type 'a tmf =
 
   | Dim0
   | Dim1
-  | TickConst
 
   | Box of {r : 'a; r' : 'a; cap : 'a; sys : ('a, 'a) system}
 
@@ -41,9 +40,6 @@ type 'a tmf =
   | Later of 'a bnd
   | Next of 'a bnd
 
-  | BoxModality of 'a
-  | Shut of 'a
-
   | Up of 'a cmd
   | Let of 'a cmd * 'a bnd
 
@@ -75,7 +71,6 @@ and 'a frame =
   | LblCall
   | CoRForce
   | Prev of 'a
-  | Open
 
   | Elim of {dlbl : Desc.data_label; mot : 'a bnd; clauses : (Desc.con_label * 'a nbnd) list}
 
diff --git a/src/core/Typing.ml b/src/core/Typing.ml
index c53460db4..6ec9c60f3 100644
--- a/src/core/Typing.ml
+++ b/src/core/Typing.ml
@@ -1,6 +1,9 @@
 module Q = Quote
 module T = Tm
 module D = Domain
+module B = Desc.Boundary
+
+open Tm.Notation
 
 type value = D.value
 
@@ -70,8 +73,6 @@ and check_dim_cmd cx =
 
 let rec check_tick cx tr =
   match T.unleash tr with
-  | T.TickConst ->
-    ()
   | T.Up cmd ->
     check_tick_cmd cx cmd
   | _ ->
@@ -151,34 +152,31 @@ let check_extension_cofibration xs cofib =
   | _ ->
     check_valid_cofibration ~xs:(Some xs) cofib
 
-let rec check cx ty tm =
+let rec check_ cx ty rst tm =
   let (module V) = Cx.evaluator cx in
-  match V.unleash ty, T.unleash tm with
-  | D.Univ info0, T.Univ info1 ->
+  match rst, V.unleash ty, T.unleash tm with
+  | [], D.Univ info0, T.Univ info1 ->
     (* TODO: what about kinds? I think it's fine, since we learned from Andy Pitts how to make
        the pretype universe Kan. But I may need to add those "ecom" thingies, LOL. *)
     if Lvl.greater info0.lvl info1.lvl then () else
       failwith "Predicativity violation"
 
-  | D.Univ _, T.Pi (dom, B (nm, cod)) ->
+
+  | [], D.Univ _, T.Pi (dom, B (nm, cod)) ->
     let vdom = check_eval cx ty dom in
     let cxx', _ = Cx.ext_ty cx ~nm vdom in
     check cxx' ty cod
 
-  | D.Univ _, T.Sg (dom, B (nm, cod)) ->
+  | [], D.Univ _, T.Sg (dom, B (nm, cod)) ->
     let vdom = check_eval cx ty dom in
     let cxx, _ = Cx.ext_ty cx ~nm vdom in
     check cxx ty cod
 
-  | D.Univ _, T.Later (B (nm, cod)) ->
+  | [], D.Univ _, T.Later (B (nm, cod)) ->
     let cxx, _ = Cx.ext_tick cx ~nm in
     check cxx ty cod
 
-  | D.Univ _, T.BoxModality t ->
-    let cx' = Cx.ext_lock cx in
-    check cx' ty t
-
-  | D.Univ univ, T.Ext (NB (nms, (cod, sys))) ->
+  | [], D.Univ univ, T.Ext (NB (nms, (cod, sys))) ->
     let cxx, xs = Cx.ext_dims cx ~nms:(Bwd.to_list nms) in
     let vcod = check_eval cxx ty cod in
     if Kind.lte univ.kind `Kan then
@@ -187,12 +185,12 @@ let rec check cx ty tm =
       ();
     check_ext_sys cxx vcod sys
 
-  | D.Univ univ, T.Rst info ->
+  | [], D.Univ univ, T.Rst info ->
     if univ.kind = `Pre then () else failwith "Restriction type is not Kan";
     let ty = check_eval cx ty info.ty in
     check_ext_sys cx ty info.sys
 
-  | D.Univ univ, T.CoR (tr, tr', oty) ->
+  | [], D.Univ univ, T.CoR (tr, tr', oty) ->
     if univ.kind = `Pre then () else failwith "Co-restriction type is not known to be Kan";
     let r = check_eval_dim cx tr in
     let r' = check_eval_dim cx tr' in
@@ -207,50 +205,64 @@ let rec check cx ty tm =
         failwith "co-restriction type malformed"
     end
 
-  | D.Univ _, T.V info ->
+  | [], D.Univ _, T.V info ->
     check_dim cx info.r;
     let ty0 = check_eval cx ty info.ty0 in
     let ty1 = check_eval cx ty info.ty1 in
     check_is_equivalence cx ~ty0 ~ty1 ~equiv:info.equiv
 
-  | D.Univ univ, T.Data dlbl ->
+  | [], D.Univ univ, T.Data dlbl ->
     let desc = GlobalEnv.lookup_datatype dlbl @@ Cx.globals cx in
-    if Lvl.lte desc.lvl univ.lvl && Kind.lte desc.kind univ.kind then
-      ()
-    else
-      failwith "Universe level/kind error"
+    begin
+      if Lvl.lte desc.lvl univ.lvl && Kind.lte desc.kind univ.kind then
+        ()
+      else
+        failwith "Universe level/kind error"
+    end
 
-  | D.Data dlbl, T.Intro (dlbl', clbl, args) when dlbl = dlbl' ->
+  | [], D.Data dlbl, T.Intro (dlbl', clbl, args) when dlbl = dlbl' ->
     let desc = GlobalEnv.lookup_datatype dlbl @@ Cx.globals cx in
     let constr = Desc.lookup_constr clbl desc in
-    check_constr cx dlbl constr args
+    check_constr cx dlbl constr args;
 
 
-  | D.Pi {dom; cod}, T.Lam (T.B (nm, tm)) ->
+  | _, D.Pi {dom; cod}, T.Lam (T.B (nm, tm)) ->
     let cxx, x = Cx.ext_ty cx ~nm dom in
     let vcod = V.inst_clo cod x in
-    check cxx vcod tm
+    let rst' = List.map (Face.map (fun r r' v -> V.apply v @@ D.Value.act (I.equate r r') x)) rst in
+    check_ cxx vcod rst' tm
 
-  | D.Later tclo, T.Next (T.B (nm, tm)) ->
+  | _, D.Later tclo, T.Next (T.B (nm, tm)) ->
     let cxx, tck = Cx.ext_tick cx ~nm in
     let vty = V.inst_tick_clo tclo tck in
-    check cxx vty tm
-
-  | D.BoxModality vty, T.Shut tm ->
-    let cx' = Cx.ext_lock cx in
-    check cx' vty tm
+    let rst' = List.map (Face.map (fun _ _ -> V.prev tck)) rst in
+    check_ cxx vty rst' tm
 
-  | D.Sg {dom; cod}, T.Cons (t0, t1) ->
-    let v = check_eval cx dom t0 in
+  | _, D.Sg {dom; cod}, T.Cons (t0, t1) ->
+    let rst0 = List.map (Face.map (fun _ _ -> V.car)) rst in
+    let rst1 = List.map (Face.map (fun _ _ -> V.cdr)) rst in
+    let v = check_eval_ cx dom rst0 t0 in
     let vcod = V.inst_clo cod v in
-    check cx vcod t1
+    check_ cx vcod rst1 t1
 
-  | D.Ext ext_abs, T.ExtLam (T.NB (nms, tm)) ->
+  | _, D.Ext ext_abs, T.ExtLam (T.NB (nms, tm)) ->
     let cxx, xs = Cx.ext_dims cx ~nms:(Bwd.to_list nms) in
     let codx, sysx = Domain.ExtAbs.inst ext_abs @@ Bwd.map (fun x -> `Atom x) @@ Bwd.from_list xs in
-    check_boundary cxx codx sysx tm
-
-  | D.CoR ty_face, T.CoRThunk (tr0, tr1, otm) ->
+    let rst' = List.map (Face.map (fun _ _ el -> V.ext_apply el @@ List.map (fun x -> `Atom x) xs)) rst in
+    check_ cxx codx (rst' @ sysx) tm
+
+  | _, D.Ext ext_abs, T.Up cmd ->
+    let n = D.ExtAbs.len ext_abs in
+    let nms = ListUtil.tabulate n @@ fun _ -> None in
+    let cxx, xs = Cx.ext_dims cx ~nms in
+    let rs = List.map (fun x -> `Atom x) xs in
+    let trs = List.map (Cx.quote_dim cx) rs in
+    let codx, sysx = Domain.ExtAbs.inst ext_abs @@ Bwd.from_list rs in
+    let cmd' = T.subst_cmd (T.shift n) cmd in
+    let rst' = List.map (Face.map (fun _ _ el -> V.ext_apply el @@ List.map (fun x -> `Atom x) xs)) rst in
+    check_ cxx codx (rst' @ sysx) @@ Tm.up @@ cmd' @< Tm.ExtApp trs
+
+  | _, D.CoR ty_face, T.CoRThunk (tr0, tr1, otm) ->
     let r'0 = check_eval_dim cx tr0 in
     let r'1 = check_eval_dim cx tr1 in
     begin
@@ -261,7 +273,8 @@ let rec check cx ty tm =
         begin
           match I.compare r'0 r0, I.compare r'1 r1 with
           | `Same, `Same ->
-            check cx (Lazy.force ty) tm
+            let rst' = List.map (Face.map (fun _ _ -> V.corestriction_force)) rst in
+            check_ cx (Lazy.force ty) rst' tm
           | _ ->
             failwith "co-restriction mismatch"
         end
@@ -273,7 +286,9 @@ let rec check cx ty tm =
             begin
               try
                 let cx', phi = Cx.restrict cx r'0 r'1 in
-                check cx' (Domain.Value.act phi @@ Lazy.force ty) tm
+                (* is this right?? : *)
+                let rst' = List.map (Face.map (fun _ _ -> V.corestriction_force)) rst in
+                check_ cx' (Domain.Value.act phi @@ Lazy.force ty) rst' tm
               with
               | I.Inconsistent -> ()
             end
@@ -285,14 +300,14 @@ let rec check cx ty tm =
         failwith "Malformed element of co-restriction type"
     end
 
-  | D.Rst {ty; sys}, _ ->
-    check cx ty tm;
-    check_boundary cx ty sys tm
+  | _, D.Rst {ty; sys}, _ ->
+    check_ cx ty (sys @ rst) tm
 
-  | D.Univ _, T.FHCom info ->
+  | [], D.Univ _, T.FHCom info ->
     check_fhcom cx ty info.r info.r' info.cap info.sys
 
-  | D.Univ _, T.LblTy info ->
+
+  | [], D.Univ _, T.LblTy info ->
     check cx ty info.ty;
     let go_arg (ty, tm) =
       let vty = check_eval_ty cx ty in
@@ -300,10 +315,11 @@ let rec check cx ty tm =
     in
     List.iter go_arg info.args
 
-  | D.LblTy info, T.LblRet t ->
-    check cx info.ty t
+  | [], D.LblTy info, T.LblRet t ->
+    let rst' = List.map (Face.map (fun _ _ -> V.lbl_call)) rst in
+    check_ cx info.ty rst' t
 
-  | D.V vty, T.VIn vin ->
+  | [], D.V vty, T.VIn vin ->
     let r = check_eval_dim cx vin.r in
     begin
       match I.compare (`Atom vty.x) r with
@@ -314,22 +330,32 @@ let rec check cx ty tm =
         Cx.check_eq cx' ~ty:(D.Value.act phi vty.ty1) (V.apply (V.car vty.equiv) el0) @@ D.Value.act phi el1
       | _ ->
         failwith "v/vin dimension mismatch"
-    end
+    end;
 
-  | _, T.Up tm ->
+  | [], _, T.Up tm ->
     let ty' = infer cx tm in
     Cx.check_subtype cx ty' ty
 
-  | _, T.Let (cmd, T.B (nm, t1)) ->
+  | _, _, T.Let (cmd, T.B (nm, t1)) ->
     let ty' = infer cx cmd in
     let el = Cx.eval_cmd cx cmd in
     let cx' = Cx.def cx ~nm ~ty:ty' ~el in
-    check cx' ty t1
+    (* TODO: right?? *)
+    check_ cx' ty rst t1
 
-  | _ ->
+
+  | _ :: _, _, _ ->
+    let v = check_eval cx ty tm in
+    check_boundary cx ty rst v
+
+  | [], _, _ ->
     (* Format.eprintf "Failed to check term %a@." (Tm.pp (CxUtil.ppenv cx)) tm; *)
     failwith "Type error"
 
+and check cx ty tm =
+  check_ cx ty [] tm
+
+
 and check_constr cx dlbl constr tms =
   let vdataty = D.make @@ D.Data dlbl in
   let rec go cx' const_specs rec_specs dim_specs tms =
@@ -364,32 +390,29 @@ and check_fhcom cx ty tr tr' tcap tsys =
   check_valid_cofibration @@ cofibration_of_sys cx tsys;
   check_comp_sys cx r (cxx, x, ty) cap tsys
 
-and check_boundary cx ty sys tm =
+and check_boundary cx ty sys el =
   let rec go sys =
     match sys with
     | [] -> ()
     | face :: sys ->
-      check_boundary_face cx ty face tm;
+      check_boundary_face cx ty face el;
       go sys
   in
-  check cx ty tm;
   go sys
 
-and check_boundary_face cx ty face tm =
+and check_boundary_face cx ty face el =
   match face with
-  | Face.True (_, _, el) ->
-    Cx.check_eq cx ~ty (Lazy.force el) @@
-    Cx.eval cx tm
+  | Face.True (_, _, el') ->
+    Cx.check_eq cx ~ty (Lazy.force el') el
 
   | Face.False _ ->
     ()
 
-  | Face.Indet (p, el) ->
+  | Face.Indet (p, el') ->
     let r, r' = Eq.unleash p in
     try
       let cx', phi = Cx.restrict cx r r' in
-      Cx.check_eq cx' ~ty:(D.Value.act phi ty) (Lazy.force el) @@
-      Cx.eval cx' tm
+      Cx.check_eq cx' ~ty:(D.Value.act phi ty) (Lazy.force el') @@ D.Value.act phi el
     with
     | I.Inconsistent ->
       ()
@@ -566,7 +589,7 @@ and infer_spine cx hd =
       let used_labels = Hashtbl.create 10 in
 
 
-      let check_clause earlier_clauses lbl constr =
+      let check_clause nclos lbl constr =
         let open Desc in
         if Hashtbl.mem used_labels lbl then failwith "Duplicate case in eliminator";
         Hashtbl.add used_labels lbl ();
@@ -576,44 +599,54 @@ and infer_spine cx hd =
         (* 'cx' is local context extended with hyps;
            'env' is the environment for evaluating the types that comprise
            the constructor, and should therefore begin with the *empty* environment. *)
-        let rec build_cx cx env (nms, cvs, rvs, rs) const_specs rec_specs dim_specs =
+        let rec build_cx cx ty_env (nms, cvs, rvs, ihvs, rs) const_specs rec_specs dim_specs =
           match const_specs, rec_specs, dim_specs with
           | (plbl, pty) :: const_specs, _, _ ->
-            let vty = V.eval env pty in
+            let vty = V.eval ty_env pty in
             let cx', v = Cx.ext_ty cx ~nm:(Some plbl) vty in
-            build_cx cx' (D.Env.push (`Val v) env) (nms #< (Some plbl), cvs #< v, rvs, rs) const_specs rec_specs dim_specs
+            build_cx cx' (D.Env.push (`Val v) ty_env) (nms #< (Some plbl), cvs #< v, rvs, ihvs, rs) const_specs rec_specs dim_specs
           | [], (nm, Self) :: rec_specs, _ ->
             let cx_x, v_x = Cx.ext_ty cx ~nm:(Some nm) ih.ty in
-            let cx_ih, _ = Cx.ext_ty cx_x ~nm:None @@ V.inst_clo mot_clo v_x in
-            build_cx cx_ih env (nms #< (Some nm) #< None, cvs, rvs #< v_x, rs) const_specs rec_specs dim_specs
+            let cx_ih, v_ih = Cx.ext_ty cx_x ~nm:None @@ V.inst_clo mot_clo v_x in
+            build_cx cx_ih ty_env (nms #< (Some nm) #< None, cvs, rvs #< v_x, ihvs #< v_ih, rs) const_specs rec_specs dim_specs
           | [], [], nm :: dim_specs ->
             let cx', x = Cx.ext_dim cx ~nm:(Some nm) in
-            build_cx cx' env (nms #< (Some nm), cvs, rvs, rs #< (`Atom x)) const_specs rec_specs dim_specs
+            build_cx cx' ty_env (nms #< (Some nm), cvs, rvs, ihvs, rs #< (`Atom x)) const_specs rec_specs dim_specs
           | [], [], [] ->
-            cx, nms, Bwd.to_list cvs, Bwd.to_list rvs, Bwd.to_list rs
+            cx, nms, Bwd.to_list cvs, Bwd.to_list rvs, ihvs, Bwd.to_list rs
         in
         (* Need to extend the context once for each constr.params, and then twice for
            each constr.args (twice, because of i.h.). *)
-        let cx', nms, cvs, rvs, rs = build_cx cx D.Env.emp (Emp, Emp, Emp, Emp) constr.const_specs constr.rec_specs constr.dim_specs in
+        let cx', nms, cvs, rvs, ihvs, rs = build_cx cx D.Env.emp (Emp, Emp, Emp, Emp, Emp) constr.const_specs constr.rec_specs constr.dim_specs in
         let intro = V.make_intro (D.Env.clear_locals @@ Cx.env cx) ~dlbl:info.dlbl ~clbl:lbl ~const_args:cvs ~rec_args:rvs ~rs in
         let ty = V.inst_clo mot_clo intro in
 
-        let image_of_face face =
-          let elim_face r r' scrut =
-            let phi = I.equate r r' in
-            let mot = D.Clo.act phi mot_clo in
-            let clauses = List.map (fun (lbl, nclo) -> lbl, D.NClo.act phi nclo) earlier_clauses in
-            V.elim_data info.dlbl ~mot ~scrut ~clauses
-          in
-          Face.map elim_face @@
-          let env0 = D.Env.clear_locals (Cx.env cx) in
-          V.eval_bterm_face info.dlbl desc env0 face
-            ~const_args:cvs
-            ~rec_args:rvs
-            ~rs:rs
+        let rec image_of_bterm phi =
+          function
+          | B.Intro intro as bterm ->
+            let nclo : D.nclo = D.NClo.act phi @@ snd @@ List.find (fun (clbl, _) -> clbl = intro.clbl) nclos in
+            let rargs = List.map (fun bt -> `Val (image_of_bterm phi bt)) intro.rec_args in
+            let cargs = List.map (fun t -> `Val (D.Value.act phi @@ Cx.eval cx' t)) intro.const_args in
+            let dims = List.map (fun t -> `Dim (I.act phi @@ Cx.eval_dim cx' t)) intro.rs in (* is this right ? *)
+            let cells = cargs @ rargs @ dims in
+            V.inst_nclo nclo cells
+          | B.Var ix ->
+            (* This is so bad!! *)
+            let ix' = ix - List.length rs in
+            D.Value.act phi @@ Bwd.nth ihvs ix'
+
+        in
+
+        let image_of_bface (tr, tr', btm) =
+          let env = Cx.env cx' in
+          let r = V.eval_dim env tr in
+          let r' = V.eval_dim env tr' in
+          D.ValFace.make I.idn r r' @@ fun phi ->
+          image_of_bterm phi btm
         in
-        let boundary = List.map image_of_face constr.boundary in
-        check_boundary cx' ty boundary bdy;
+
+        let boundary = List.map image_of_bface constr.boundary in
+        check_ cx' ty boundary bdy;
         Tm.NB (nms, bdy)
       in
 
@@ -661,11 +694,6 @@ and infer_spine cx hd =
       let vtick = Cx.eval_tick cx tick in
       begin
         match vtick with
-        | D.TickConst ->
-          let cx' = Cx.ext_lock cx in
-          let ih = infer_spine cx' hd sp in
-          let tclo = V.unleash_later ih.ty in
-          D.{el = V.prev vtick ih.el; ty = V.inst_tick_clo tclo vtick}
         | D.TickGen tgen ->
           let cx' = Cx.kill_from_tick cx tgen in
           let ih = infer_spine cx' hd sp in
@@ -673,13 +701,6 @@ and infer_spine cx hd =
           D.{el = V.prev vtick ih.el; ty = V.inst_tick_clo tclo vtick}
       end
 
-    | T.Open ->
-      let cx' = Cx.clear_locks cx in
-      let ih = infer_spine cx' hd sp in
-      let ty = V.unleash_box_modality ih.ty in
-      D.{el = V.modal_open ih.el; ty}
-
-
 and infer_head cx =
   function
   | T.Var {name; twin; ushift} ->
@@ -771,6 +792,10 @@ and check_eval cx ty tm =
   check cx ty tm;
   Cx.eval cx tm
 
+and check_eval_ cx ty rst tm =
+  check_ cx ty rst tm;
+  Cx.eval cx tm
+
 and check_ty cx ty =
   let univ = D.make @@ D.Univ {kind = `Pre; lvl = `Omega} in
   check cx univ ty
diff --git a/src/core/Typing.mli b/src/core/Typing.mli
index fa9328585..961c59c4b 100644
--- a/src/core/Typing.mli
+++ b/src/core/Typing.mli
@@ -10,7 +10,6 @@ end
 
 val check : cx -> value -> Tm.tm -> unit
 val infer : cx -> Tm.tm Tm.cmd -> value
-val check_boundary : cx -> value -> Domain.val_sys -> Tm.tm -> unit
 
 val check_constr_boundary_sys
   : cx
diff --git a/src/core/Val.ml b/src/core/Val.ml
index 8c8e2b518..cd1d95136 100644
--- a/src/core/Val.ml
+++ b/src/core/Val.ml
@@ -12,6 +12,8 @@ type step =
 let ret v = Ret v
 let step v = Step v
 
+exception StrictHComEncounteredNonConstructor
+
 
 type error =
   | UnexpectedEnvCell of env_el
@@ -36,7 +38,6 @@ type error =
   | UnleashExtError of value
   | UnleashVError of value
   | UnleashLaterError of value
-  | UnleashBoxModalityError of value
   | UnleashCoRError of value
   | UnleashLblTyError of value
   | UnleashFHComError of value
@@ -94,9 +95,10 @@ struct
       Format.fprintf fmt
         "Unexpected argument to labeled type projection:@ %a."
         pp_value v
-    | UnexpectedEnvCell _ ->
+    | UnexpectedEnvCell cell ->
       Format.fprintf fmt
-        "Did not find what was expected in the environment."
+        "Did not find what was expected in the environment: %a"
+        pp_env_cell cell
     | ExpectedDimensionTerm t ->
       Format.fprintf fmt
         "Tried to evaluate non-dimension term %a as dimension."
@@ -133,10 +135,6 @@ struct
       Format.fprintf fmt
         "Tried to unleash %a as later modality."
         pp_value v
-    | UnleashBoxModalityError v ->
-      Format.fprintf fmt
-        "Tried to unleash %a as box modality."
-        pp_value v
     | UnleashExtError v ->
       Format.fprintf fmt
         "Tried to unleash %a as extension type."
@@ -219,8 +217,6 @@ struct
 
   let eval_tick rho tm =
     match Tm.unleash tm with
-    | Tm.TickConst ->
-      TickConst
     | Tm.Up (hd, Emp) ->
       begin
         match hd with
@@ -367,12 +363,6 @@ struct
       let clo = Clo.act phi info.clo in
       make_dfix_line r ty clo
 
-    | BoxModality v ->
-      make @@ BoxModality (Value.act phi v)
-
-    | Shut v ->
-      make @@ Shut (Value.act phi v)
-
     | Data lbl ->
       make @@ Data lbl
 
@@ -432,6 +422,12 @@ struct
       in
       step @@ make_coe dir abs el
 
+    | NCoeAtType info ->
+      let dir = Dir.act phi info.dir in
+      let abs = Abs.act phi info.abs in
+      let el = Value.act phi info.el in
+      step @@ make_coe dir abs el
+
 
     | VProj info ->
       let mx = I.act phi @@ `Atom info.x in
@@ -543,16 +539,6 @@ struct
           step @@ prev tick v
       end
 
-    | Open neu ->
-      begin
-        match act_neu phi neu with
-        | Ret neu ->
-          ret @@ Open neu
-        | Step v ->
-          step @@ modal_open v
-      end
-
-
     | Fix (tick, ty, clo) ->
       ret @@ Fix (tick, Value.act phi ty, Clo.act phi clo)
 
@@ -578,6 +564,14 @@ struct
       {ty; el}
 
   and unleash : value -> con =
+    let add_sys sys el=
+      match unleash el with
+      | Up up ->
+        Up {up with sys = sys @ up.sys}
+      | con ->
+        con
+    in
+
     fun (Node info) ->
       let con =
         match info.action = I.idn with
@@ -596,9 +590,9 @@ struct
             begin
               match force_val_sys rst.sys with
               | `Proj el ->
-                unleash el
-              | `Ok sys ->
-                Up {ty = rst.ty; neu = up.neu; sys}
+                add_sys up.sys el
+              | `Ok rsys ->
+                add_sys rsys @@ make @@ Up {up with ty = rst.ty}
             end
           | _ ->
             con
@@ -846,9 +840,15 @@ struct
   and rigid_coe dir abs el =
     let x, tyx = Abs.unleash1 abs in
     match unleash tyx with
-    | Pi _ | Sg _ | Ext _ | Up _ | Later _ | BoxModality _ ->
+    | Pi _ | Sg _ | Ext _ | Later _ ->
       make @@ Coe {dir; abs; el}
 
+    | Up _ ->
+      let neu = NCoeAtType {dir; abs; el} in
+      let _, r' = Dir.unleash dir in
+      let ty_r' = Abs.inst1 abs r' in
+      reflect ty_r' neu []
+
     (* TODO: what about neutral element of the universe? is this even correct? *)
     | Univ _ ->
       el
@@ -936,7 +936,8 @@ struct
       let recovery_general phi abs z_dest =
         make_gcom (Dir.make (I.act (I.cmp phi subst_r') s) z_dest) abs (naively_coerced_cap phi) @@
         force_abs_sys @@
-        let diag = AbsFace.make phi (I.act phi r) (I.act phi r') @@ fun phi ->
+        let diag =
+          AbsFace.make phi (I.act phi r) (I.act phi r') @@ fun phi ->
           Abs.make1 @@ fun y -> recovery_apart phi (Abs.act phi abs) (I.act phi r) (`Atom y) in
         let face =
           Face.map @@ fun sj s'j absj ->
@@ -951,9 +952,11 @@ struct
       let coerced_cap =
         make_hcom (Dir.act subst_r' fhcom.dir) (Value.act subst_r' fhcom.cap) (naively_coerced_cap I.idn) @@
         force_abs_sys @@
-        let diag = AbsFace.make_from_dir I.idn dir @@ fun phi ->
+        let diag =
+          AbsFace.make_from_dir I.idn dir @@ fun phi ->
           Abs.make1 @@ fun w -> origin phi (`Atom w) in
-        let face = Face.map @@ fun sj s'j absj ->
+        let face =
+          Face.map @@ fun sj s'j absj ->
           let phi = I.equate sj s'j in
           Abs.make1 @@ fun w ->
           make_coe (Dir.make (`Atom w) (I.act phi (I.act subst_r' s))) absj @@
@@ -963,7 +966,8 @@ struct
       in
       make_box (Dir.act subst_r' fhcom.dir) coerced_cap @@
       force_val_sys @@
-      let face = Face.map @@ fun sj s'j absj ->
+      let face =
+        Face.map @@ fun sj s'j absj ->
         let phi = I.equate sj s'j in
         recovery_general phi absj (I.act (I.cmp phi subst_r') s')
       in List.map (fun b -> face (AbsFace.act subst_r' b)) fhcom.sys
@@ -1010,24 +1014,29 @@ struct
            * `ext_apply (cdr fib) [`Dim1]` directly. *)
           let contr0 phi fib = apply (cdr @@ apply (cdr (Value.act phi equiv0)) (ext_apply (cdr fib) [`Dim1])) fib in
           (* The diagonal face for r=r'. *)
-          let face_diag = AbsFace.make_from_dir I.idn dir @@ fun phi ->
+          let face_diag =
+            AbsFace.make_from_dir I.idn dir @@ fun phi ->
             Abs.make1 @@ fun _ -> base phi (I.act phi r) (I.act phi r')
           in
           (* The face for r=0. *)
-          let face0 = AbsFace.make I.idn r `Dim0 @@ fun phi ->
+          let face0 =
+            AbsFace.make I.idn r `Dim0 @@ fun phi ->
             Abs.make1 @@ fun _ -> base0 phi (I.act phi r')
           in
           (* The face for r=1. This more optimized version is used
            * in [Y], [F] and [R1] but not [SVO]. *)
-          let face1 = AbsFace.make I.idn r `Dim1 @@ fun phi ->
+          let face1 =
+            AbsFace.make I.idn r `Dim1 @@ fun phi ->
             Abs.make1 @@ fun y ->
             let ty = Value.act phi @@ subst_r' info.ty1 in
             let cap = base1 phi (I.act phi r') in
             let msys = force_abs_sys @@
-              let face0 = AbsFace.make phi (I.act phi r') `Dim0 @@ fun phi ->
+              let face0 =
+                AbsFace.make phi (I.act phi r') `Dim0 @@ fun phi ->
                 Abs.make1 @@ fun z -> ext_apply (cdr (fiber0 phi cap)) [`Atom z]
               in
-              let face1 = AbsFace.make phi (I.act phi r') `Dim1 @@ fun phi ->
+              let face1 =
+                AbsFace.make phi (I.act phi r') `Dim1 @@ fun phi ->
                 Abs.make1 @@ fun _ -> Value.act phi el in
               [face0; face1]
             in
@@ -1074,10 +1083,12 @@ struct
               (* hcom whore cap is (fiber0 base), r=0 face is contr0, and r=1 face is constant *)
               make_hcom (Dir.make `Dim1 `Dim0) (fiber0_ty phi (base phi (I.act phi r) `Dim0)) (fiber0 phi (base phi (I.act phi r) `Dim0)) @@
               force_abs_sys @@
-              let face0 = AbsFace.make phi (I.act phi r) `Dim0 @@ fun phi ->
+              let face0 =
+                AbsFace.make phi (I.act phi r) `Dim0 @@ fun phi ->
                 Abs.make1 @@ fun w -> ext_apply (contr0 phi (fiber_at_face0 phi)) [`Atom w]
               in
-              let face1 = AbsFace.make phi (I.act phi r) `Dim1 @@ fun phi ->
+              let face1 =
+                AbsFace.make phi (I.act phi r) `Dim1 @@ fun phi ->
                 Abs.make1 @@ fun _ -> fiber0 phi (base1 phi `Dim0)
               in
               [face0; face1]
@@ -1149,7 +1160,10 @@ struct
         match unleash el with
         | Intro info' ->
           List.nth (info'.const_args @ info'.rec_args) k
+        | Up _ ->
+          raise StrictHComEncounteredNonConstructor
         | _ ->
+          Format.eprintf "Very bad: %a@." pp_value el;
           failwith "rigid_hcom_strict_data: peel_arg"
       in
 
@@ -1197,7 +1211,7 @@ struct
       let sys_phi = CompSys.act phi comp_sys in
       make_hcom dir_phi ty cap_phi sys_phi
     in
-    let ty = reflect univ ty [] in
+    let ty = reflect univ ty @@ ValSys.from_rigid rst_sys in
     let rst_sys = List.map (Face.map hcom_face) rst_sys in
     make @@ Up {ty; neu; sys = rst_sys}
 
@@ -1222,11 +1236,20 @@ struct
       rigid_nhcom_up_at_type dir info.ty info.neu cap ~comp_sys:sys ~rst_sys:info.sys
 
     | Data dlbl ->
-      let desc = Sig.lookup_datatype dlbl in
-      if Desc.is_strict_set desc then
-        rigid_hcom_strict_data dir ty cap sys
-      else
+      (* It's too expensive to determine in advance if the system has constructors in all faces, so we just disable strict composition for now. *)
+      make @@ FHCom {dir; cap; sys}
+
+    (* Note, that the following code looks like it would work, but it doesn't. The problem is that the exception gets thrown in a recursive call that is underneath a thunk,
+       so it is never caught. Generally, backtracking is not something we would support during evaluation. *)
+
+    (* let desc = Sig.lookup_datatype dlbl in
+       if Desc.is_strict_set desc then
+       try rigid_hcom_strict_data dir ty cap sys
+       with
+       | StrictHComEncounteredNonConstructor ->
         make @@ FHCom {dir; cap; sys}
+       else
+       make @@ FHCom {dir; cap; sys} *)
 
     | Univ _ ->
       rigid_fhcom dir cap sys
@@ -1265,7 +1288,8 @@ struct
       let new_cap =
         rigid_hcom dir fhcom.cap (cap_aux I.idn cap) @@
         let ri_faces =
-          let face = Face.map @@ fun ri r'i abs ->
+          let face =
+            Face.map @@ fun ri r'i abs ->
             let y, el = Abs.unleash1 abs in
             Abs.bind1 y @@ cap_aux (I.equate ri r'i) el
           in
@@ -1360,7 +1384,8 @@ struct
             | `Ok rest0 ->
               let r'i = I.act phi r'i in
               let ghcom00 = AbsFace.make phi r'i dim0 @@ fun phi -> Abs.act phi @@ Lazy.force absi in
-              let ghcom01 = AbsFace.make phi r'i dim1 @@ fun phi ->
+              let ghcom01 =
+                AbsFace.make phi r'i dim1 @@ fun phi ->
                 Abs.make1 @@ fun y ->
                 (* TODO this can be optimized further by expanding
                  * `make_ghcom` because `ty` is not changed and
@@ -1466,7 +1491,9 @@ struct
     let rho' =
       Env.push_many
         begin
-          (* This is not backwards, FYI. *)
+          List.rev @@
+          (* ~~This is not backwards, FYI.~~ *)
+          (* NARRATOR VOICE: it was backwards. *)
           List.map (fun x -> `Val x) const_args
           @ List.map (fun x -> `Val x) rec_args
           @ List.map (fun x -> `Dim x) rs
@@ -1562,9 +1589,6 @@ struct
     | (Tm.Dim0 | Tm.Dim1) ->
       raise @@ E (UnexpectedDimensionTerm tm)
 
-    | Tm.TickConst ->
-      raise @@ E (UnexpectedTickTerm tm)
-
     | Tm.Up cmd ->
       eval_cmd rho cmd
 
@@ -1588,14 +1612,6 @@ struct
       let tclo = TickClo {bnd; rho} in
       make @@ Next tclo
 
-    | Tm.BoxModality ty ->
-      let vty = eval rho ty in
-      make @@ BoxModality vty
-
-    | Tm.Shut t ->
-      let v = eval rho t in
-      make @@ Shut v
-
     | Tm.Data lbl ->
       make @@ Data lbl
 
@@ -1662,8 +1678,6 @@ struct
     | Tm.Prev tick ->
       let vtick = eval_tick rho tick in
       prev vtick vhd
-    | Tm.Open ->
-      modal_open vhd
     | Tm.Elim info ->
       let mot = clo info.mot rho in
       let clauses = List.map (fun (lbl, nbnd) -> lbl, nclo nbnd rho) info.clauses in
@@ -1855,13 +1869,6 @@ struct
     | _ ->
       raise @@ E (UnleashLaterError v)
 
-  and unleash_box_modality v =
-    match unleash v with
-    | BoxModality ty -> ty
-    | Rst rst -> unleash_box_modality rst.ty
-    | _ ->
-      raise @@ E (UnleashBoxModalityError v)
-
   and unleash_sg v =
     match unleash v with
     | Sg {dom; cod} -> dom, cod
@@ -2099,8 +2106,6 @@ struct
     | DFix dfix ->
       begin
         match tick with
-        | TickConst ->
-          inst_clo dfix.clo el
         | TickGen gen ->
           let neu = Fix (gen, dfix.ty, dfix.clo) in
           make @@ Up {ty = dfix.ty; neu; sys = []}
@@ -2108,8 +2113,6 @@ struct
     | DFixLine dfix ->
       begin
         match tick with
-        | TickConst ->
-          inst_clo dfix.clo el
         | TickGen gen ->
           let neu = FixLine (dfix.x, gen, dfix.ty, dfix.clo) in
           make @@ Up {ty = dfix.ty; neu; sys = []}
@@ -2164,53 +2167,6 @@ struct
       failwith "prev"
 
 
-  and modal_open el =
-    match unleash el with
-    | Shut el ->
-      el
-
-    | Up info ->
-      let ty = unleash_box_modality info.ty in
-      let open_face = Face.map @@ fun _ _ a -> modal_open a in
-      let open_sys = List.map open_face info.sys in
-      make @@ Up {ty; neu = Open info.neu; sys = open_sys}
-
-    | Coe info ->
-      (* EXPERIMENTAL !!! *)
-      let x, boxtyx = Abs.unleash1 info.abs in
-      let tyx = unleash_box_modality boxtyx in
-      let abs = Abs.bind1 x tyx in
-      let el = modal_open info.el in
-      rigid_coe info.dir abs el
-
-    | HCom info ->
-      (* EXPERIMENTAL !!! *)
-      let ty = unleash_box_modality info.ty in
-      let cap = modal_open info.cap in
-      let open_face =
-        Face.map @@ fun _ _ abs ->
-        let x, v = Abs.unleash1 abs in
-        Abs.bind1 x @@ modal_open v
-      in
-      let sys = List.map open_face info.sys in
-      rigid_hcom info.dir ty cap sys
-
-    | GHCom info ->
-      (* EXPERIMENTAL !!! *)
-      let ty = unleash_box_modality info.ty in
-      let cap = modal_open info.cap in
-      let open_face =
-        Face.map @@ fun _ _ abs ->
-        let x, v = Abs.unleash1 abs in
-        Abs.bind1 x @@ modal_open v
-      in
-      let sys = List.map open_face info.sys in
-      rigid_ghcom info.dir ty cap sys
-
-    | _ ->
-      failwith "modal_open"
-
-
   (* the equation oracle `phi` is for continuations `ty0` and `equiv`
    * waiting for an updated oracle. *)
   and vproj phi mgen ~ty0 ~ty1 ~equiv ~el : value =
@@ -2242,9 +2198,17 @@ struct
       raise @@ E err
 
   and elim_data dlbl ~mot ~scrut ~clauses =
+    let find_clause clbl =
+      try
+        snd @@ List.find (fun (clbl', _) -> clbl = clbl') clauses
+      with
+      | Not_found ->
+        raise @@ MissingElimClause clbl
+    in
+
     match unleash scrut with
     | Intro info ->
-      let _, nclo = List.find (fun (clbl', _) -> info.clbl = clbl') clauses in
+      let nclo = find_clause info.clbl in
 
       (* Clean this up with some kind of a state type for the traversal maybe. Barf! *)
       let rec go cvs rvs rs =
diff --git a/src/core/ValSig.ml b/src/core/ValSig.ml
index e40083dd8..ec4500e25 100644
--- a/src/core/ValSig.ml
+++ b/src/core/ValSig.ml
@@ -11,9 +11,11 @@ sig
   (** Return the type and boundary of a global variable *)
   val lookup : Name.t -> Tm.twin -> Tm.tm * (Tm.tm, Tm.tm) Tm.system
 
-  val lookup_datatype : Desc.data_label -> (Tm.tm, Tm.tm B.term) Desc.desc
+  val lookup_datatype : Desc.data_label -> Tm.data_desc
 end
 
+exception MissingElimClause of Desc.con_label
+
 module type S =
 sig
   val unleash : value -> con
@@ -30,29 +32,29 @@ sig
 
   val eval_bterm
     : Desc.data_label
-    -> (Tm.tm, Tm.tm B.term) Desc.desc
+    -> Tm.data_desc
     -> env
-    -> Tm.tm B.term
+    -> Tm.btm
     -> value
 
   val eval_bterm_boundary
     : Desc.data_label
-    -> (Tm.tm, Tm.tm B.term) Desc.desc
+    -> Tm.data_desc
     -> env
     -> const_args:value list
     -> rec_args:value list
     -> rs:I.t list
-    -> (Tm.tm, Tm.tm B.term) B.sys
+    -> Tm.bsys
     -> val_sys
 
   val eval_bterm_face
     : Desc.data_label
-    -> (Tm.tm, Tm.tm B.term) Desc.desc
+    -> Tm.data_desc
     -> env
     -> const_args:value list
     -> rec_args:value list
     -> rs:I.t list
-    -> (Tm.tm, Tm.tm B.term) B.face
+    -> Tm.bface
     -> val_face
 
   val make_closure : env -> Tm.tm Tm.bnd -> clo
@@ -60,7 +62,6 @@ sig
   val apply : value -> value -> value
   val ext_apply : value -> dim list -> value
   val prev : tick -> value -> value
-  val modal_open : value -> value
 
   val elim_data : Desc.data_label -> mot:clo -> scrut:value -> clauses:(string * nclo) list -> value
 
@@ -79,7 +80,6 @@ sig
   val unleash_sg : value -> value * clo
   val unleash_v : value -> atom * value * value * value
   val unleash_later : value -> tick_clo
-  val unleash_box_modality : value -> value
   val unleash_fhcom : value -> dir * value * comp_sys
   val unleash_ext_with : value -> dim list -> value * val_sys
   val unleash_ext : value -> ext_abs
diff --git a/src/core/dune b/src/core/dune
index 84e452310..a5000a7ee 100644
--- a/src/core/dune
+++ b/src/core/dune
@@ -1,6 +1,6 @@
 (library
  (name RedTT_Core)
  (flags
-  (:standard -w -32-37))
+  (:standard -w -32-26-27-37))
  (public_name redtt_core)
  (libraries redbasis uuseg uuseg.string uutf))
diff --git a/src/frontend/Contextual.ml b/src/frontend/Contextual.ml
index d30592e90..6a2ec539d 100644
--- a/src/frontend/Contextual.ml
+++ b/src/frontend/Contextual.ml
@@ -175,10 +175,6 @@ let get_global_env =
       GlobalEnv.ext_dim (go_params psi) x
     | Snoc (psi, (x, `Tick)) ->
       GlobalEnv.ext_tick (go_params psi) x
-    | Snoc (psi, (_, `Lock)) ->
-      GlobalEnv.ext_lock @@ go_params psi
-    | Snoc (psi, (_, `ClearLocks)) ->
-      GlobalEnv.clear_locks @@ go_params psi
     | Snoc (psi, (_, `KillFromTick tck)) ->
       begin
         match Tm.unleash tck with
@@ -189,6 +185,8 @@ let get_global_env =
       end
     | Snoc (psi, (x, `P ty)) ->
       GlobalEnv.ext (go_params psi) x @@ `P {ty; sys = []}
+    | Snoc (psi, (x, `Def (ty, tm))) ->
+      GlobalEnv.define (go_params psi) x ~ty ~tm
     | Snoc (psi, (x, `Tw (ty0, ty1))) ->
       GlobalEnv.ext (go_params psi) x @@ `Tw ({ty = ty0; sys = []}, {ty = ty1; sys = []})
     | Snoc (psi, (_, `R (r0, r1))) ->
@@ -251,6 +249,8 @@ let lookup_var x w =
     match w, gm with
     | `Only, Snoc (gm, (y, `P ty)) ->
       if x = y then M.ret ty else go gm
+    | `Only, Snoc (gm, (y, `Def (ty, _))) ->
+      if x = y then M.ret ty else go gm
     | `TwinL, Snoc (gm, (y, `Tw (ty0, _))) ->
       if x = y then M.ret ty0 else go gm
     | `TwinR, Snoc (gm, (y, `Tw (_, ty1))) ->
diff --git a/src/frontend/Dev.ml b/src/frontend/Dev.ml
index 18b86de94..eae3ca466 100644
--- a/src/frontend/Dev.ml
+++ b/src/frontend/Dev.ml
@@ -25,10 +25,9 @@ type ('a, 'b) equation =
 type 'a param =
   [ `I
   | `Tick
-  | `Lock
-  | `ClearLocks
   | `KillFromTick of 'a
   | `P of 'a
+  | `Def of 'a * 'a
   | `Tw of 'a * 'a
   | `R of 'a * 'a
   | `SelfArg of 'a Desc.rec_spec
@@ -75,11 +74,13 @@ let rec eqn_close_var x tw k q =
 
 let param_open_var k x =
   function
-  | (`I | `Tick | `Lock | `ClearLocks) as p -> p
+  | (`I | `Tick ) as p -> p
   | `KillFromTick tck ->
     `KillFromTick (Tm.open_var k (fun twin -> Tm.var x ~twin) tck)
   | `P ty ->
     `P (Tm.open_var k (fun twin -> Tm.var x ~twin) ty)
+  | `Def (ty, tm) ->
+    `Def (Tm.open_var k (fun twin -> Tm.var x ~twin) ty, Tm.open_var k (fun twin -> Tm.var x ~twin) tm)
   | `Tw (ty0, ty1) ->
     `Tw (Tm.open_var k (fun twin -> Tm.var x ~twin) ty0, Tm.open_var k (fun twin -> Tm.var x ~twin) ty1)
   | `R (r0, r1) ->
@@ -90,11 +91,13 @@ let param_open_var k x =
 
 let param_close_var x k =
   function
-  | (`I | `Tick | `Lock | `ClearLocks) as p -> p
+  | (`I | `Tick) as p -> p
   | `KillFromTick tck ->
     `KillFromTick (Tm.close_var x ~twin:(fun tw -> tw) k tck)
   | `P ty ->
     `P (Tm.close_var x ~twin:(fun tw -> tw) k ty)
+  | `Def (ty, tm) ->
+    `Def (Tm.close_var x ~twin:(fun tw -> tw) k ty, Tm.close_var x ~twin:(fun tw -> tw) k tm)
   | `Tw (ty0, ty1) ->
     `Tw (Tm.close_var x ~twin:(fun tw -> tw) k ty0, Tm.close_var x ~twin:(fun tw -> tw) k ty1)
   | `R (r0, r1) ->
@@ -177,14 +180,12 @@ let pp_param fmt =
     Format.fprintf fmt "dim"
   | `Tick ->
     Uuseg_string.pp_utf_8 fmt "✓"
-  | `Lock ->
-    Uuseg_string.pp_utf_8 fmt "🔓"
-  | `ClearLocks ->
-    Format.fprintf fmt "<clear-locks>"
   | `KillFromTick _ ->
     Format.fprintf fmt "<kill-after-tick>"
   | `P ty ->
     Tm.pp0 fmt ty
+  | `Def (ty, _) -> (* TODO *)
+    Tm.pp0 fmt ty
   | `Tw (ty0, ty1) ->
     Format.fprintf fmt "%a %a %a"
       Tm.pp0 ty0
@@ -205,6 +206,12 @@ let pp_param_cell fmt (x, param) =
       Name.pp x
       Tm.pp0 ty
 
+  | `Def (ty, tm) ->
+    Format.fprintf fmt "@[<1>%a : %a = %a@]"
+      Name.pp x
+      Tm.pp0 ty
+      Tm.pp0 tm
+
   | `Tw (ty0, ty1) ->
     Format.fprintf fmt "@[<1>%a : %a %a %a@]"
       Name.pp x
@@ -222,12 +229,6 @@ let pp_param_cell fmt (x, param) =
       Uuseg_string.pp_utf_8
       "✓"
 
-  | `Lock ->
-    Uuseg_string.pp_utf_8 fmt "🔓"
-
-  | `ClearLocks ->
-    Format.fprintf fmt "<clear-locks>"
-
   | `KillFromTick tck ->
     Format.fprintf fmt "<clear-after-tick: %a>"
       Tm.pp0 tck
@@ -360,12 +361,14 @@ let subst_equation sub q =
 let subst_param sub =
   let univ = Tm.univ ~kind:`Pre ~lvl:`Omega in
   function
-  | (`I | `Tick | `Lock | `ClearLocks | `SelfArg Desc.Self) as p ->
+  | (`I | `Tick | `SelfArg Desc.Self) as p ->
     p, sub
   | `KillFromTick tck ->
     `KillFromTick (subst_tm sub ~ty:univ tck), sub
   | `P ty ->
     `P (subst_tm sub ~ty:univ ty), sub
+  | `Def (ty, tm) ->
+    `Def (subst_tm sub ~ty:univ ty, subst_tm sub ~ty tm), sub
   | `Tw (ty0, ty1) ->
     `Tw (subst_tm sub ~ty:univ ty0, subst_tm sub ~ty:univ ty1), sub
   | `R (r0, r1) ->
@@ -391,12 +394,18 @@ let rec subst_problem sub =
         let probx' = subst_problem sub'' probx in
         let prob' = bind x param' probx' in
         All (param', prob')
+      | `Def (ty, tm) ->
+        let sys = [Tm.make Dim0, Tm.make Dim0, Some tm] in
+        let sub'' = GlobalEnv.ext sub' x @@ `P {ty; sys}  in
+        let probx' = subst_problem sub'' probx in
+        let prob' = bind x param' probx' in
+        All (param', prob')
       | `Tw (ty0, ty1) ->
         let sub'' = GlobalEnv.ext sub' x @@ `Tw ({ty = ty0; sys = []}, {ty = ty1; sys = []}) in
         let probx' = subst_problem sub'' probx in
         let prob' = bind x param' probx' in
         All (param', prob')
-      | (`I | `Tick | `Lock | `ClearLocks | `KillFromTick _ | `SelfArg Desc.Self) ->
+      | (`I | `Tick | `KillFromTick _ | `SelfArg Desc.Self) ->
         let probx' = subst_problem sub' probx in
         let prob' = bind x param' probx' in
         All (param', prob')
@@ -424,9 +433,11 @@ struct
 
   let free fl =
     function
-    | (`I | `Tick | `Lock | `ClearLocks | `SelfArg Desc.Self) -> Occurs.Set.empty
+    | (`I | `Tick | `SelfArg Desc.Self) -> Occurs.Set.empty
     | `KillFromTick tck -> Tm.free fl tck
     | `P ty -> Tm.free fl ty
+    | `Def (ty, tm) ->
+      Occurs.Set.union (Tm.free fl ty) (Tm.free fl tm)
     | `Tw (ty0, ty1) ->
       Occurs.Set.union (Tm.free fl ty0) (Tm.free fl ty1)
     | `R (r0, r1) ->
diff --git a/src/frontend/Dev.mli b/src/frontend/Dev.mli
index 73c099585..bc2f235bf 100644
--- a/src/frontend/Dev.mli
+++ b/src/frontend/Dev.mli
@@ -22,10 +22,9 @@ type ('a, 'b) equation =
 type 'a param =
   [ `I
   | `Tick
-  | `Lock
-  | `ClearLocks
   | `KillFromTick of 'a
   | `P of 'a
+  | `Def of 'a * 'a
   | `Tw of 'a * 'a
   | `R of 'a * 'a
   | `SelfArg of 'a Desc.rec_spec
diff --git a/src/frontend/ESig.ml b/src/frontend/ESig.ml
index 04ac52e2d..b417ab045 100644
--- a/src/frontend/ESig.ml
+++ b/src/frontend/ESig.ml
@@ -9,6 +9,7 @@ type edecl =
   | Define of string * [ `Opaque | `Transparent ] * escheme * eterm
   | Data of string * (eterm, eterm) Desc.desc
   | Debug of [ `All | `Constraints | `Unsolved ]
+  | Normalize of eterm
   | Import of string
   | Quit
 
@@ -19,7 +20,6 @@ and ecell =
   [ `Ty of string * eterm
   | `Tick of string
   | `I of string
-  | `Lock
   ]
 
 and etele = ecell list
@@ -39,7 +39,6 @@ and econ =
   | Pi of etele * eterm
   | Sg of etele * eterm
   | Ext of string list * eterm * esys
-  | Rst of eterm * esys
 
   | Coe of {r : eterm; r' : eterm; fam : eterm; tm : eterm}
   | HCom of {r : eterm; r' : eterm; cap : eterm; sys : esys}
@@ -47,12 +46,13 @@ and econ =
 
   | Shut of eterm
 
-  | TickConst
   | DFixLine of {r : eterm; name : string; ty : eterm; bdy : eterm}
   | FixLine of {r : eterm; name : string; ty : eterm; bdy : eterm}
 
   | Cut of eterm * frame bwd
 
+  | Auto
+
   | Var of string * int
   | Num of int
 
diff --git a/src/frontend/ElabMonad.ml b/src/frontend/ElabMonad.ml
index 84717cd93..f0bf57c2e 100644
--- a/src/frontend/ElabMonad.ml
+++ b/src/frontend/ElabMonad.ml
@@ -12,6 +12,9 @@ type diagnostic =
        tele : U.telescope;
        ty : Tm.tm;
        tm : Tm.tm}
+  | PrintTerm of
+      {ty : Tm.tm;
+       tm : Tm.tm}
 
 type 'a m = ('a * (location * diagnostic) bwd) C.m
 
@@ -46,9 +49,15 @@ let normalize_param p =
   match p with
   | `P ty ->
     C.ret @@ `P (normalize_ty ty)
+  | `Def (ty, tm) ->
+    let vty = Cx.eval cx ty in
+    let ty' = Cx.quote_ty cx vty in
+    let el = Cx.eval cx tm in
+    let tm' = Cx.quote cx ~ty:vty el in
+    C.ret @@ `Def (ty', tm')
   | `Tw (ty0, ty1) ->
     C.ret @@ `Tw (normalize_ty ty0, normalize_ty ty1)
-  | (`I | `Tick | `Lock | `ClearLocks | `KillFromTick _ | `SelfArg Desc.Self) as p ->
+  | (`I | `Tick | `KillFromTick _ | `SelfArg Desc.Self) as p ->
     C.ret p
   | `R (r0, r1) ->
     C.ret @@ `R (r0, r1)
@@ -65,6 +74,13 @@ let rec normalize_tele =
 
 let print_diagnostic =
   function
+  | (loc, PrintTerm {tm; ty}) ->
+    let pp fmt () =
+      Format.fprintf fmt "@[<v>%a@,@,has type@,@,%a@]" Tm.pp0 tm Tm.pp0 ty
+    in
+    Log.pp_message ~loc ~lvl:`Info pp Format.std_formatter ();
+    C.ret ()
+
   | (loc, UserHole {name; tele; ty; _}) ->
     C.local (fun _ -> tele) @@
     begin
@@ -72,12 +88,45 @@ let print_diagnostic =
       C.bind (normalize_tele @@ Bwd.to_list tele) @@ fun tele ->
       let vty = Cx.eval cx ty in
       let ty = Cx.quote_ty cx vty in
+
+      let pp_restriction fmt =
+        let pp_bdy fmt =
+          function
+          | None -> Format.fprintf fmt "-"
+          | Some tm -> Tm.pp0 fmt tm
+        in
+        let pp_face fmt (r, r', otm) =
+          Format.fprintf fmt "%a = %a %a @[%a@]"
+            Tm.pp0 r
+            Tm.pp0 r'
+            Uuseg_string.pp_utf_8 "⇒"
+            pp_bdy otm
+        in
+        Format.pp_print_list ~pp_sep:Format.pp_print_cut pp_face fmt
+      in
+
+      let pp_restricted_ty fmt (ty, sys) =
+        match sys with
+        | [] -> Tm.pp0 fmt ty
+        | _ ->
+          Format.fprintf fmt "%a@,@,with the following faces:@,@,   @[<v>%a@]"
+            Tm.pp0 ty
+            pp_restriction sys
+      in
+
+      let ty, sys =
+        match Tm.unleash ty with
+        | Tm.Rst rst ->
+          rst.ty, rst.sys
+        | _ ->
+          ty, []
+      in
       let pp fmt () =
-        Format.fprintf fmt "@[<v>?%s:@; @[<v>%a@]@,%a %a@]"
+        Format.fprintf fmt "@[<v>?%s:@; @[<v>%a@]@,@[<v>%a %a@]@]"
           (match name with Some name -> name | None -> "Hole")
           Dev.pp_params (Bwd.from_list tele)
           Uuseg_string.pp_utf_8 "⊢"
-          Tm.pp0 ty
+          pp_restricted_ty (ty, sys)
       in
       Log.pp_message ~loc ~lvl:`Info pp Format.std_formatter ();
       C.ret ()
diff --git a/src/frontend/ElabMonad.mli b/src/frontend/ElabMonad.mli
index ca9b86458..9cfa33339 100644
--- a/src/frontend/ElabMonad.mli
+++ b/src/frontend/ElabMonad.mli
@@ -23,6 +23,9 @@ type diagnostic =
        tele : Unify.telescope;
        ty : Tm.tm;
        tm : Tm.tm}
+  | PrintTerm of
+      {ty : Tm.tm;
+       tm : Tm.tm}
 
 val emit : location -> diagnostic -> unit m
 val report : 'a m -> 'a m
diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml
index 992fda248..bd6b16bc8 100644
--- a/src/frontend/Elaborator.ml
+++ b/src/frontend/Elaborator.ml
@@ -14,20 +14,19 @@ struct
   module C = Contextual
   module U = Unify
 
-  open Dev open Unify
+  open Dev
 
   module M = ElabMonad
+  module MonadUtil = Monad.Util (M)
   module Notation = Monad.Notation (M)
   open Notation
 
   open Tm.Notation
 
-  let rec traverse f xs =
-    match xs with
-    | [] ->
-      M.ret []
-    | x :: xs ->
-      (fun y ys -> y :: ys) <@>> f x <*> traverse f xs
+
+  let traverse = MonadUtil.traverse
+
+  let flip f x y = f y x
 
   module E = ESig
   module T = Map.Make (String)
@@ -73,8 +72,6 @@ struct
 
   let kind_of_frame env =
     function
-    | E.App ({con = E.TickConst} as e) ->
-      M.ret @@ `Prev e
     | E.App ({con = E.Num (0 | 1)} as e) ->
       M.ret @@ `ExtApp e
     | E.App ({con = E.Var (nm, _)} as e) ->
@@ -87,8 +84,7 @@ struct
               M.lift C.get_global_env >>= fun env ->
               begin
                 match GlobalEnv.lookup_kind env alpha with
-                | `P _ -> M.ret @@ `FunApp e
-                | `Tw _ -> M.ret @@ `FunApp e
+                | (`P _ | `Tw _) -> M.ret @@ `FunApp e
                 | `I -> M.ret @@ `ExtApp e
                 | `Tick -> M.ret @@ `Prev e
               end
@@ -128,7 +124,7 @@ struct
       let now0 = Unix.gettimeofday () in
       elab_scheme env scheme @@ fun cod ->
       M.unify >>
-      elab_chk env cod e >>= fun tm ->
+      elab_chk env e {ty = cod; sys = []} >>= fun tm ->
       let alpha = Name.named @@ Some name in
 
       M.lift C.ask >>= fun psi ->
@@ -154,6 +150,16 @@ struct
       M.lift @@ C.dump_state Format.std_formatter title filter >>
       M.ret env
 
+    | E.Normalize e ->
+      elab_inf env e >>= fun (ty, cmd) ->
+      M.lift C.base_cx >>= fun cx ->
+      let vty = Cx.eval cx ty in
+      let el = Cx.eval_cmd cx cmd in
+      let tm = Cx.quote cx ~ty:vty el in
+      M.emit e.span @@ M.PrintTerm {ty = ty; tm} >>
+      M.ret env
+
+
     | E.Import file_name ->
       begin
         match I.import file_name with
@@ -221,7 +227,7 @@ struct
       | (lbl, ety) :: const_specs ->
         (* TODO: support higher universes *)
         let univ = Tm.univ ~kind:desc.kind ~lvl:desc.lvl in
-        elab_chk env univ ety >>= bind_in_scope >>= fun pty ->
+        elab_chk env ety {ty = univ; sys = []} >>= bind_in_scope >>= fun pty ->
         let x = Name.named @@ Some lbl in
         M.in_scope x (`P pty) @@
         go (acc #< (lbl, x, pty)) const_specs
@@ -234,34 +240,36 @@ struct
     let (module V) = Cx.evaluator cx in
     let module D = Domain in
 
-    let rec build_cx cx env (nms, cvs, rvs, rs) const_specs rec_specs dim_specs =
+    let rec build_cx cx env const_specs rec_specs dim_specs =
       match const_specs, rec_specs, dim_specs with
       | (plbl, pty) :: const_specs, _, _ ->
         let vty = V.eval env pty in
         let cx', v = Cx.ext_ty cx ~nm:(Some plbl) vty in
-        build_cx cx' (D.Env.push (`Val v) env) (nms #< (Some plbl), cvs #< v, rvs, rs) const_specs rec_specs dim_specs
+        build_cx cx' (D.Env.push (`Val v) env)  const_specs rec_specs dim_specs
       | [], (nm, Desc.Self) :: rec_specs, _ ->
-        let cx_x, v_x = Cx.ext_ty cx ~nm:(Some nm) @@ D.make @@ D.Data dlbl in
-        build_cx cx_x env (nms #< (Some nm), cvs, rvs #< v_x, rs) const_specs rec_specs dim_specs
+        let cx_x, _ = Cx.ext_ty cx ~nm:(Some nm) @@ D.make @@ D.Data dlbl in
+        build_cx cx_x env  const_specs rec_specs dim_specs
       | [], [], nm :: dim_specs ->
-        let cx', x = Cx.ext_dim cx ~nm:(Some nm) in
-        build_cx cx' env (nms #< (Some nm), cvs, rvs, rs #< (`Atom x)) const_specs rec_specs dim_specs
+        let cx', _ = Cx.ext_dim cx ~nm:(Some nm) in
+        build_cx cx' env  const_specs rec_specs dim_specs
       | [], [], [] ->
         cx
     in
 
-    let cx' = build_cx cx D.Env.emp (Emp, Emp, Emp, Emp) const_specs rec_specs dim_specs in
+    let cx' = build_cx cx D.Env.emp const_specs rec_specs dim_specs in
     traverse (elab_constr_face env dlbl desc) sys >>= fun bdry ->
     Typing.check_constr_boundary_sys cx' dlbl desc bdry;
     M.ret bdry
 
   and elab_constr_face env dlbl desc (er0, er1, e) =
-    elab_dim env er0 >>= bind_in_scope >>= fun r0 ->
-    elab_dim env er1 >>= bind_in_scope >>= fun r1 ->
+    elab_dim env er0 >>= fun r0 ->
+    bind_in_scope r0 >>= fun r0' ->
+    elab_dim env er1 >>= fun r1 ->
+    bind_in_scope r1 >>= fun r1' ->
     M.in_scope (Name.fresh ()) (`R (r0, r1)) @@
     begin
       elab_boundary_term env dlbl desc e <<@> fun bt ->
-        r0, r1, bt
+        r0', r1', bt
     end
 
   and elab_boundary_term env dlbl desc e =
@@ -280,8 +288,18 @@ struct
       match ResEnv.get name renv with
       | `Var x ->
         M.lift C.ask >>= fun psi ->
-        (* backwards? *)
-        let ix = ListUtil.index_of (fun (y, _) -> x = y) @@ Bwd.to_list psi in
+        let go (x, param) =
+          match param with
+          | `P _ -> [x]
+          | `Def _ -> [x]
+          | `I -> [x]
+          | `SelfArg _ -> [x]
+          | `Tick -> [x]
+          | `Tw _ -> []
+          | _ -> []
+        in
+        let xs = Bwd.flat_map go psi in
+        let ix = Bwd.length xs - 1 - (ListUtil.index_of (fun y -> x = y) @@ Bwd.to_list xs) in
         M.ret @@ `Ix ix
       | `Ix _ ->
         failwith "impossible"
@@ -312,7 +330,7 @@ struct
           (* TODO: might be backwards *)
           let sub = List.fold_right (fun (ty,tm) sub -> Tm.dot (Tm.ann ~ty ~tm) sub) acc @@ Tm.shift 0 in
           let pty' = Tm.subst sub pty in
-          elab_chk env pty' e >>= bind_in_scope >>= fun t ->
+          elab_chk env e {ty = pty'; sys = []} >>= bind_in_scope >>= fun t ->
           go_const_specs ((pty', t) :: acc) ps frms
         | _ ->
           failwith "elab_intro: malformed parameters"
@@ -346,31 +364,16 @@ struct
       M.ret @@ Desc.Boundary.Intro {clbl; const_args; rec_args; rs}
 
 
-  and bind_in_scope tm =
-    M.lift C.ask <<@> fun psi ->
-      let go (x, param) =
-        match param with
-        | `P _ -> [x]
-        | `I -> [x]
-        | `SelfArg _ -> [x]
-        | `Tick -> [x]
-        | `Tw _ -> []
-        | _ -> []
-      in
-      let xs = Bwd.rev @@ Bwd.flat_map go psi in
-      let Tm.NB (_, tm) = Tm.bindn xs tm in
-      tm
-
 
 
   and elab_scheme env (cells, ecod) kont =
     let rec go =
       function
       | [] ->
-        elab_chk env univ ecod >>=
+        elab_chk env ecod {ty = univ; sys = []} >>=
         kont
       | `Ty (name, edom) :: cells ->
-        elab_chk env univ edom >>= normalize_ty >>= fun dom ->
+        elab_chk env edom {ty = univ; sys = []} >>= normalize_ty >>= fun dom ->
         let x = Name.named @@ Some name in
         M.in_scope x (`P dom) @@
         go cells
@@ -382,208 +385,186 @@ struct
         let x = Name.named @@ Some name in
         M.in_scope x `I @@
         go cells
-      | `Lock :: cells ->
-        let x = Name.fresh () in
-        M.in_scope x `Lock @@
-        go cells
       | _ -> failwith "TODO: elab_scheme"
     in
     go cells
 
 
 
-
-
   (* TODO: we will be disentangling all the elaboration of concrete expressions from tactics which produce redtt proofs.
      As an example, see what we have done with tac_lambda, tac_if, etc. *)
-  and elab_chk env ty e : tm M.m =
-    normalize_ty ty >>= fun ty ->
-    match Tm.unleash ty, e.con with
-    | Tm.Rst rst, E.Guess e ->
-      elab_chk env rst.ty e >>= fun tm ->
-      M.lift C.ask >>= fun psi ->
-      M.lift @@ U.push_guess psi ~ty0:ty ~ty1:rst.ty tm
-
-    | Tm.BoxModality ty, E.Shut e ->
-      M.in_scope (Name.fresh ()) `Lock begin
-        elab_chk env ty e
-      end <<@> fun tm ->
-        Tm.make @@ Tm.Shut tm
+  and elab_chk env e : chk_tac =
+    fun goal ->
+      (* TODO speed up elaboration by not normalizing, but raising ChkMatch if we don't know what to do.
+         Then wrap the whole thing in tac_wrap_nf. *)
+      normalize_ty goal.ty >>= fun ty ->
+      let goal = {goal with ty} in
+      match goal.sys, Tm.unleash ty, e.con with
+      | _, _, E.Guess e ->
+        tac_guess (elab_chk env e) goal
+
+      | _, _, E.Hole name ->
+        tac_hole ~loc:e.span ~name goal
+
+      | _, _, E.Hope ->
+        tac_hope goal
+
+      | _, _, E.Auto ->
+        tac_auto goal
+
+      | _, _, E.Let info ->
+        let itac =
+          match info.ty with
+          | None ->
+            elab_inf env info.tm <<@> fun (let_ty, let_tm) ->
+              let_ty, Tm.up let_tm
+          | Some ety ->
+            elab_chk env ety {ty = univ; sys = []} >>= fun let_ty ->
+            elab_chk env info.tm {ty = let_ty; sys = []} <<@> fun let_tm ->
+              let_ty, let_tm
+        in
+        let ctac goal = elab_chk env info.body goal in
+        tac_let info.name itac ctac goal
 
-    | _, E.Hole name ->
-      M.lift C.ask >>= fun psi ->
-      M.lift @@ U.push_hole `Rigid psi ty >>= fun tm ->
-      begin
-        if name = Some "_" then M.ret () else
-          M.emit e.span @@ M.UserHole {name; ty; tele = psi; tm = Tm.up tm}
-      end >>
-      M.ret @@ Tm.up tm
+      | _, Tm.Rst rst, _ ->
+        elab_chk env e {ty = rst.ty; sys = rst.sys @ goal.sys}
 
-    | _, E.Hope ->
-      M.lift C.ask >>= fun psi ->
-      M.lift @@ U.push_hole `Flex psi ty <<@> Tm.up
-
-
-    | _, E.Let info ->
-      let itac =
-        match info.ty with
-        | None ->
-          elab_inf env info.tm <<@> fun (let_ty, let_tm) ->
-            let_ty, Tm.up let_tm
-        | Some ety ->
-          elab_chk env univ ety >>= fun let_ty ->
-          elab_chk env let_ty info.tm <<@> fun let_tm ->
-            let_ty, let_tm
-      in
-      let ctac ty = elab_chk env ty info.body in
-      tac_let info.name itac ctac ty
+      | _, _, E.Lam (names, e) ->
+        let tac = elab_chk env e in
+        tac_wrap_nf (tac_lambda names tac) goal
 
-    | Tm.Rst _, _ ->
-      tac_rst (fun ty -> elab_chk env ty e) ty
+      | [], _, E.Quo tmfam ->
+        get_resolver env >>= fun renv ->
+        let tm = tmfam renv in
+        begin
+          match Tm.unleash tm with
+          | Tm.Up _ ->
+            elab_up env ty {e with con = E.Quo tmfam}
+          | _ ->
+            M.ret @@ tmfam renv
+        end
 
-    | _, E.Lam (names, e) ->
-      let tac ty = elab_chk env ty e in
-      tac_wrap_nf (tac_lambda names tac) ty
 
-    | _, E.Quo tmfam ->
-      get_resolver env >>= fun renv ->
-      let tm = tmfam renv in
-      begin
-        match Tm.unleash tm with
-        | Tm.Up _ ->
-          elab_up env ty {e with con = E.Quo tmfam }
-        | _ ->
-          M.ret @@ tmfam renv
-      end
+      | [], _, E.Elim {mot; scrut; clauses} ->
+        let tac_mot = Option.map (elab_chk env) mot in
+        let tac_scrut = elab_inf env scrut <<@> fun (ty, cmd) -> ty, Tm.up cmd in
+        let used = Hashtbl.create 10 in
+        let elab_clause (lbl, pbinds, bdy) =
+          if Hashtbl.mem used lbl then failwith "Duplicate clause in elimination" else
+            begin
+              Hashtbl.add used lbl ();
+              lbl, pbinds, elab_chk env bdy
+            end
+        in
+        let clauses = List.map elab_clause clauses in
+        tac_elim ~loc:e.span ~tac_mot ~tac_scrut ~clauses goal
+
+      | [], Tm.Univ _, E.Ext (names, ety, esys) ->
+        let univ = ty in
+        let xs = List.map (fun x -> Name.named (Some x)) names in
+        let ps = List.map (fun x -> (x, `I)) xs in
+        M.in_scopes ps begin
+          elab_chk env ety {ty = univ; sys = []} >>= fun tyxs ->
+          elab_tm_sys env tyxs esys <<@> fun sysxs ->
+            let ebnd = Tm.bind_ext (Bwd.from_list xs) tyxs sysxs in
+            let ext_ty = Tm.make @@ Tm.Ext ebnd in
+            ext_ty
+        end
 
+      | [], Tm.Univ _, E.Pi ([], e) ->
+        elab_chk env e goal
 
-    | _, E.Elim {mot; scrut; clauses} ->
-      let tac_mot = Option.map (fun emot ty -> elab_chk env ty emot) mot in
-      let tac_scrut = elab_inf env scrut <<@> fun (ty, cmd) -> ty, Tm.up cmd in
-      let used = Hashtbl.create 10 in
-      let elab_clause (lbl, pbinds, bdy) =
-        if Hashtbl.mem used lbl then failwith "Duplicate clause in elimination" else
-          begin
-            Hashtbl.add used lbl ();
-            lbl, pbinds, fun ty -> elab_chk env ty bdy
-          end
-      in
-      let clauses = List.map elab_clause clauses in
-      tac_elim ~loc:e.span ~tac_mot ~tac_scrut ~clauses ty
-
-    | Tm.Univ _, E.Ext (names, ety, esys) ->
-      let univ = ty in
-      let xs = List.map (fun x -> Name.named (Some x)) names in
-      let ps = List.map (fun x -> (x, `I)) xs in
-      M.in_scopes ps begin
-        elab_chk env univ ety >>= fun tyxs ->
-        elab_tm_sys env tyxs esys <<@> fun sysxs ->
-          let ebnd = Tm.bind_ext (Bwd.from_list xs) tyxs sysxs in
-          let ext_ty = Tm.make @@ Tm.Ext ebnd in
-          ext_ty
-      end
+      | [], Tm.Univ _, E.Pi (`Ty (name, edom) :: etele, ecod) ->
+        elab_chk env edom {ty; sys = []} >>= fun dom ->
+        let x = Name.named @@ Some name in
+        M.in_scope x (`P dom) begin
+          elab_chk env {e with con = E.Pi (etele, ecod)} {ty; sys = []}
+          <<@> Tm.bind x
+          <<@> fun cod -> Tm.make @@ Tm.Pi (dom, cod)
+        end
 
-    | Tm.Univ _, E.Rst (ety, esys) ->
-      let univ = ty in
-      elab_chk env univ ety >>= fun ty ->
-      elab_tm_sys env ty esys <<@> fun sys ->
-        Tm.make @@ Tm.Rst {ty; sys}
+      | [], Tm.Univ _, E.Pi (`I name :: etele, ecod) ->
+        let x = Name.named @@ Some name in
+        M.in_scope x `I begin
+          elab_chk env { e with con = E.Pi (etele, ecod)} {ty; sys = []}
+          <<@> fun codx ->
+            let ebnd = Tm.bind_ext (Emp #< x) codx [] in
+            Tm.make @@ Tm.Ext ebnd
+        end
 
-    | Tm.Univ _, E.Pi ([], e) ->
-      elab_chk env ty e
+      | [], Tm.Univ _, E.Pi (`Tick name :: etele, ecod) ->
+        let x = Name.named @@ Some name in
+        M.in_scope x `Tick begin
+          elab_chk env {e with con = E.Pi (etele, ecod)} {ty; sys = []}
+          <<@> Tm.bind x
+          <<@> fun bnd -> Tm.make @@ Tm.Later bnd
+        end
 
-    | Tm.Univ _, E.Pi (`Ty (name, edom) :: etele, ecod) ->
-      elab_chk env ty edom >>= fun dom ->
-      let x = Name.named @@ Some name in
-      M.in_scope x (`P dom) begin
-        elab_chk env ty {e with con = E.Pi (etele, ecod)}
-        <<@> Tm.bind x
-        <<@> fun cod -> Tm.make @@ Tm.Pi (dom, cod)
-      end
+      | [], Tm.Univ _, E.Sg ([], e) ->
+        elab_chk env e {ty; sys = []}
 
-    | Tm.Univ _, E.Pi (`I name :: etele, ecod) ->
-      let x = Name.named @@ Some name in
-      M.in_scope x `I begin
-        elab_chk env ty { e with con = E.Pi (etele, ecod)}
-        <<@> fun codx ->
-          let ebnd = Tm.bind_ext (Emp #< x) codx [] in
-          Tm.make @@ Tm.Ext ebnd
-      end
+      | [], Tm.Univ _, E.Sg (`Ty (name, edom) :: etele, ecod) ->
+        elab_chk env edom {ty; sys = []} >>= fun dom ->
+        let x = Name.named @@ Some name in
+        M.in_scope x (`P dom) begin
+          elab_chk env {e with con = E.Sg (etele, ecod)} {ty; sys = []}
+          <<@> Tm.bind x
+          <<@> fun cod -> Tm.make @@ Tm.Sg (dom, cod)
+        end
 
-    | Tm.Univ _, E.Pi (`Tick name :: etele, ecod) ->
-      let x = Name.named @@ Some name in
-      M.in_scope x `Tick begin
-        elab_chk env ty {e with con = E.Pi (etele, ecod)}
-        <<@> Tm.bind x
-        <<@> fun bnd -> Tm.make @@ Tm.Later bnd
-      end
 
-    | Tm.Univ _, E.Pi (`Lock :: etele, ecod) ->
-      let x = Name.fresh () in
-      M.in_scope x `Lock begin
-        elab_chk env ty {e with con = E.Pi (etele, ecod)}
-        <<@> fun ty -> Tm.make @@ Tm.BoxModality ty
-      end
+      | _, _, Tuple [] ->
+        failwith "empty tuple"
 
-    | Tm.Univ _, E.Sg ([], e) ->
-      elab_chk env ty e
+      | _, _, Tuple [e] ->
+        elab_chk env e goal
 
-    | Tm.Univ _, E.Sg (`Ty (name, edom) :: etele, ecod) ->
-      elab_chk env ty edom >>= fun dom ->
-      let x = Name.named @@ Some name in
-      M.in_scope x (`P dom) begin
-        elab_chk env ty {e with con = E.Sg (etele, ecod)}
-        <<@> Tm.bind x
-        <<@> fun cod -> Tm.make @@ Tm.Sg (dom, cod)
-      end
+      | _, Tm.Sg (dom, cod), Tuple (e0 :: es) as etuple ->
+        let tac0 = elab_chk env e0 in
+        let tac1 = elab_chk env @@ {e with con = Tuple es} in
+        tac_pair tac0 tac1 goal
 
+      | [], Tm.Univ info, Type (kind, lvl) ->
+        begin
+          if Lvl.greater info.lvl lvl then
+            match Tm.unleash ty with
+            | Tm.Univ _ ->
+              M.ret @@ Tm.univ ~kind ~lvl
+            | _ ->
+              failwith "Type"
+          else
+            failwith "Elaborator: universe level error"
+        end
 
-    | _, Tuple [] ->
-      failwith "empty tuple"
-    | _, Tuple [e] ->
-      elab_chk env ty e
-    | Tm.Sg (dom, cod), Tuple (e :: es) ->
-      elab_chk env dom e >>= fun tm0 ->
-      let cmd0 = Tm.ann ~ty:dom ~tm:tm0 in
-      let cod' = Tm.make @@ Tm.Let (cmd0, cod) in
-      elab_chk env cod' {e with con = E.Tuple es} <<@> Tm.cons tm0
+      | [], _, E.Cut (e, fs) ->
+        elab_chk_cut env e fs ty
 
-    | Tm.Univ info, Type (kind, lvl) ->
-      begin
-        if Lvl.greater info.lvl lvl then
-          match Tm.unleash ty with
-          | Tm.Univ _ ->
-            M.ret @@ Tm.univ ~kind ~lvl
-          | _ ->
-            failwith "Type"
-        else
-          failwith "Elaborator: universe level error"
-      end
+      | [], _, E.HCom info ->
+        elab_dim env info.r >>= fun r ->
+        elab_dim env info.r' >>= fun r' ->
+        let kan_univ = Tm.univ ~lvl:`Omega ~kind:`Kan in
+        begin
+          M.lift @@ C.check ~ty:kan_univ ty >>= function
+          | `Ok ->
+            elab_chk env info.cap {ty; sys = []} >>= fun cap ->
+            elab_hcom_sys env r ty cap info.sys <<@> fun sys ->
+              let hcom = Tm.HCom {r; r'; ty; cap; sys} in
+              Tm.up (hcom, Emp)
+
+          | `Exn exn ->
+            raise exn
+        end
 
-    | _, E.Cut (e, fs) ->
-      elab_chk_cut env e fs ty
+      | [], _, E.Var _ ->
+        elab_chk_cut env e Emp ty
 
-    | _, E.HCom info ->
-      elab_dim env info.r >>= fun r ->
-      elab_dim env info.r' >>= fun r' ->
-      let kan_univ = Tm.univ ~lvl:`Omega ~kind:`Kan in
-      begin
-        M.lift @@ C.check ~ty:kan_univ ty >>= function
-        | `Ok ->
-          elab_chk env ty info.cap >>= fun cap ->
-          elab_hcom_sys env r ty cap info.sys <<@> fun sys ->
-            let hcom = Tm.HCom {r; r'; ty; cap; sys} in
-            Tm.up (hcom, Emp)
-
-        | `Exn exn ->
-          raise exn
-      end
+      | [], _, _ ->
+        elab_up env ty e
 
-    | _, E.Var _ ->
-      elab_chk_cut env e Emp ty
+      | _, _, _ ->
+        elab_chk env e {goal with sys = []} >>= fun tm ->
+        guess_restricted tm goal
 
-    | _, _ ->
-      elab_up env ty e
 
   and elab_tm_sys env ty =
     let rec go acc =
@@ -592,12 +573,11 @@ struct
         M.ret @@ Bwd.to_list acc
 
       | (e_r, e_r', e) :: esys ->
-        let rst_ty = Tm.make @@ Tm.Rst {ty; sys = Bwd.to_list acc} in
         elab_dim env e_r >>= fun r ->
         elab_dim env e_r' >>= fun r' ->
         begin
           M.under_restriction r r' begin
-            elab_chk env rst_ty e
+            elab_chk env e {ty; sys = Bwd.to_list acc}
           end
         end >>= fun obnd ->
         let face = r, r', obnd in
@@ -605,6 +585,8 @@ struct
     in
     go Emp
 
+
+
   and elab_hcom_sys env s ty cap =
     let rec go acc =
       function
@@ -629,8 +611,8 @@ struct
         elab_dim env e_r' >>= fun r' ->
         begin
           M.under_restriction r r' begin
-            elab_chk env ext_ty e >>= fun line ->
-            M.in_scope x `I (M.lift @@ (ext_ty, line) %% Tm.ExtApp [varx]) >>= fun (_, tmx) ->
+            elab_chk env e {ty = ext_ty; sys = []} >>= fun line ->
+            let tmx = Tm.up @@ Tm.ann ~ty:ext_ty ~tm:line @< Tm.ExtApp [varx] in
             M.ret @@ Tm.bind x tmx
           end
         end >>= fun obnd ->
@@ -664,8 +646,8 @@ struct
         elab_dim env e_r' >>= fun r' ->
         begin
           M.under_restriction r r' begin
-            elab_chk env ext_ty e >>= fun line ->
-            M.in_scope x `I (M.lift @@ (ext_ty, line) %% Tm.ExtApp [varx]) >>= fun (_, tmx) ->
+            elab_chk env e {ty = ext_ty; sys = []} >>= fun line ->
+            let tmx = Tm.up @@ Tm.ann ~ty:ext_ty ~tm:line @< Tm.ExtApp [varx] in
             M.ret @@ Tm.bind x tmx
           end
         end >>= fun obnd ->
@@ -676,13 +658,14 @@ struct
 
   and elab_up env ty inf =
     elab_inf env inf >>= fun (ty', cmd) ->
-    M.lift (C.check_subtype ty' ty) >>= function
+    M.lift (C.check ~ty @@ Tm.up cmd) >>= function
     | `Ok -> M.ret @@ Tm.up cmd
-    | _ ->
+    | `Exn exn ->
       M.lift @@ C.active @@ Dev.Subtype {ty0 = ty'; ty1 = ty} >>
       M.unify >>
-      M.lift (C.check_subtype ty' ty) >>= function
-      | `Ok -> M.ret @@ Tm.up cmd
+      M.lift (C.check ~ty @@ Tm.up cmd) >>= function
+      | `Ok ->
+        M.ret @@ Tm.up cmd
       | `Exn exn ->
         raise exn
 
@@ -735,13 +718,12 @@ struct
       let x = Name.fresh () in
       let kan_univ = Tm.univ ~lvl:`Omega ~kind:`Kan in
       let univ_fam = Tm.make @@ Tm.Ext (Tm.bind_ext (Emp #< x) kan_univ []) in
-      elab_chk env univ_fam info.fam >>= fun fam ->
-      begin
-        (M.lift @@ (univ_fam, fam) %% Tm.ExtApp [tr] <<@> snd)
-        <&>
-        (M.lift @@ (univ_fam, fam) %% Tm.ExtApp [tr'] <<@> snd)
-      end >>= fun (fam_r, fam_r') ->
-      elab_chk env fam_r info.tm <<@> fun tm ->
+      elab_chk env info.fam {ty = univ_fam; sys = []} >>= fun fam ->
+
+      let fam_cmd = Tm.ann ~ty:univ_fam ~tm:fam in
+      let fam_r = Tm.up @@ fam_cmd @< Tm.ExtApp [tr] in
+      let fam_r' = Tm.up @@ fam_cmd @< Tm.ExtApp [tr'] in
+      elab_chk env info.tm {ty = fam_r; sys = []} <<@> fun tm ->
         let varx = Tm.up @@ Tm.var x in
         let tyx = Tm.up @@ Tm.ann ~ty:univ_fam ~tm:fam @< Tm.ExtApp [varx] in
         let coe = Tm.Coe {r = tr; r' = tr'; ty = Tm.bind x tyx; tm} in
@@ -753,40 +735,42 @@ struct
       let x = Name.fresh () in
       let kan_univ = Tm.univ ~lvl:`Omega ~kind:`Kan in
       let univ_fam = Tm.make @@ Tm.Ext (Tm.bind_ext (Emp #< x) kan_univ []) in
-      elab_chk env univ_fam info.fam >>= fun fam ->
-      M.lift @@ (univ_fam, fam) %% Tm.ExtApp [tr] >>= fun (_, fam_r) ->
-      M.lift @@ (univ_fam, fam) %% Tm.ExtApp [tr'] >>= fun (_, fam_r') ->
-      elab_chk env fam_r info.cap >>= fun cap ->
-      M.in_scope x `I begin
-        let varx = Tm.up @@ Tm.var x in
-        M.lift @@ (univ_fam, fam) %% Tm.ExtApp [varx]
-      end >>= fun (_, fam_x) ->
+      elab_chk env info.fam {ty = univ_fam; sys = []} >>= fun fam ->
+
+      let fam_cmd = Tm.ann ~ty:univ_fam ~tm:fam in
+      let fam_r = Tm.up @@ fam_cmd @< Tm.ExtApp [tr] in
+      let fam_r' = Tm.up @@ fam_cmd @< Tm.ExtApp [tr'] in
+
+      elab_chk env info.cap {ty = fam_r; sys = []} >>= fun cap ->
+
+      let varx = Tm.up @@ Tm.var x in
+      let fam_x = Tm.up @@ fam_cmd @< Tm.ExtApp [varx] in
       let tybnd = Tm.bind x fam_x in
       elab_com_sys env tr tybnd cap info.sys <<@> fun sys ->
         let com = Tm.Com {r = tr; r' = tr'; ty = tybnd; cap; sys} in
         fam_r', (com, Emp)
 
     | E.DFixLine info ->
-      elab_chk env univ info.ty >>= fun ty ->
+      elab_chk env info.ty {ty = univ; sys = []} >>= fun ty ->
       elab_dim env info.r >>= fun r ->
       let wk_ty = Tm.subst (Tm.shift 1) ty in
       let ltr_ty = Tm.make @@ Tm.Later (Tm.B (None, wk_ty)) in
       let x = Name.named @@ Some info.name in
       M.in_scope x (`P ltr_ty) begin
-        elab_chk env ty info.bdy
+        elab_chk env info.bdy {ty; sys = []}
         <<@> Tm.bind x
         <<@> fun bdy ->
           ltr_ty, (Tm.DFix {r; ty; bdy}, Emp)
       end
 
     | E.FixLine info ->
-      elab_chk env univ info.ty >>= fun ty ->
+      elab_chk env info.ty {ty = univ; sys = []} >>= fun ty ->
       elab_dim env info.r >>= fun r ->
       let wk_ty = Tm.subst (Tm.shift 1) ty in
       let ltr_ty = Tm.make @@ Tm.Later (Tm.B (None, wk_ty)) in
       let x = Name.named @@ Some info.name in
       M.in_scope x (`P ltr_ty) begin
-        elab_chk env ty info.bdy
+        elab_chk env info.bdy {ty; sys = []}
         <<@> Tm.bind x
         <<@> fun bdy ->
           let dfix = Tm.DFix {r; ty; bdy}, Emp in
@@ -887,7 +871,7 @@ struct
         (* TODO: might be backwards *)
         let sub = List.fold_right (fun (ty,tm) sub -> Tm.dot (Tm.ann ~ty ~tm) sub) acc @@ Tm.shift 0 in
         let ty' = Tm.subst sub ty in
-        elab_chk env ty' e >>= fun t ->
+        elab_chk env e {ty = ty'; sys = []} >>= fun t ->
         go_const_args ((ty', t) :: acc) const_specs frms
       | _ ->
         failwith "elab_intro: malformed parameters"
@@ -900,7 +884,7 @@ struct
         (fun x xs -> x :: xs) <@>> elab_dim env r <*> go_rec_args rec_specs dims frms
       | (_, Desc.Self) :: rec_specs, dims, E.App e :: frms ->
         let self_ty = Tm.make @@ Tm.Data dlbl in
-        (fun x xs -> x :: xs) <@>> elab_chk env self_ty e <*> go_rec_args rec_specs dims frms
+        (fun x xs -> x :: xs) <@>> elab_chk env e {ty = self_ty; sys = []} <*> go_rec_args rec_specs dims frms
       | _ ->
         failwith "todo: go_args"
     in
@@ -910,13 +894,17 @@ struct
 
   and elab_mode_switch_cut env exp frms ty =
     elab_cut env exp frms >>= fun (ty', cmd) ->
-    M.lift @@ C.active @@ Dev.Subtype {ty0 = ty'; ty1 = ty} >>
-    M.unify >>
-    M.lift (C.check_subtype ty' ty) >>= function
+    M.lift (C.check ~ty @@ Tm.up cmd) >>= function
     | `Ok ->
       M.ret @@ Tm.up cmd
     | `Exn exn ->
-      raise exn
+      M.lift @@ C.active @@ Dev.Subtype {ty0 = ty'; ty1 = ty} >>
+      M.unify >>
+      M.lift (C.check ~ty @@ Tm.up cmd) >>= function
+      | `Ok ->
+        M.ret @@ Tm.up cmd
+      | `Exn exn ->
+        raise exn
 
   and elab_cut env exp frms =
     elab_cut_ env exp frms >>= fun (ty, cmd) ->
@@ -967,7 +955,7 @@ struct
       begin
         match unleash ty with
         | Tm.Pi (dom, cod) ->
-          elab_chk env dom e <<@> fun arg ->
+          elab_chk env e {ty = dom; sys = []} <<@> fun arg ->
             Tm.unbind_with (Tm.ann ~ty:dom ~tm:arg) cod, cmd @< Tm.FunApp arg
         | _ ->
           raise ChkMatch
@@ -997,21 +985,6 @@ struct
           raise ChkMatch
       end
 
-    | spine, `Prev {con = E.TickConst} ->
-      M.in_scope (Name.fresh ()) `Lock begin
-        elab_cut env exp spine
-      end >>= fun (ty, cmd) ->
-      try_nf ty @@ fun ty ->
-      begin
-        match unleash ty with
-        | Later ltr ->
-          let tick = Tm.make Tm.TickConst in
-          let ty' = Tm.unbind_with (Tm.DownX tick, Emp) ltr in
-          M.ret (ty', cmd @< Tm.Prev tick)
-        | _ ->
-          raise ChkMatch
-      end
-
     | spine, `Prev {con = E.Var (name, _)} ->
       elab_var env name 0 >>= fun (_, tick) ->
       M.in_scope (Name.fresh ()) (`KillFromTick (Tm.up tick)) begin
@@ -1027,19 +1000,6 @@ struct
           raise ChkMatch
       end
 
-    | spine, `Open ->
-      M.in_scope (Name.fresh ()) `ClearLocks begin
-        elab_cut env exp spine
-      end >>= fun (ty, cmd) ->
-      try_nf ty @@ fun ty ->
-      begin
-        match unleash ty with
-        | Tm.BoxModality ty' ->
-          M.ret (ty', cmd @< Tm.Open)
-        | _ ->
-          raise ChkMatch
-      end
-
     | _ ->
       failwith "elab_cut"
 
diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly
index 06a785b23..f74ee1261 100644
--- a/src/frontend/Grammar.mly
+++ b/src/frontend/Grammar.mly
@@ -15,13 +15,13 @@
 %token <string> ATOM
 %token <string option> HOLE_NAME
 %token LSQ RSQ LPR RPR LGL RGL LBR RBR
-%token COLON TRIANGLE_RIGHT COMMA DOT PIPE CARET BANG
+%token COLON TRIANGLE_RIGHT COMMA DOT PIPE CARET
 %token EQUALS
-%token RIGHT_ARROW RRIGHT_ARROW BULLET
+%token RIGHT_ARROW RRIGHT_ARROW
 %token TIMES HASH AT BACKTICK IN WITH WHERE END DATA INTRO
-%token DIM TICK LOCK
-%token ELIM UNIV LAM PAIR FST SND COMP HCOM COM COE LET DEBUG CALL RESTRICT V VPROJ VIN NEXT PREV FIX DFIX BOX_MODALITY OPEN SHUT
-%token IMPORT OPAQUE QUIT
+%token DIM TICK
+%token ELIM UNIV LAM PAIR FST SND COMP HCOM COM COE LET CALL V VPROJ VIN NEXT PREV FIX DFIX AUTO
+%token IMPORT OPAQUE QUIT DEBUG NORMALIZE
 %token TYPE PRE KAN
 %token EOF
 
@@ -36,6 +36,8 @@ edecl:
     { E.Define (a, `Opaque, sch, tm) }
   | DEBUG; f = debug_filter
     { E.Debug f }
+  | NORMALIZE; e = eterm
+    { E.Normalize e }
 
   | DATA; dlbl = ATOM;
     univ_spec = option(preceded(COLON, univ_spec));
@@ -86,10 +88,10 @@ atomic_econ:
     { E.Var (a, k) }
   | a = ATOM;
     { if a = "_" then E.Hope else E.Var (a, 0) }
+  | AUTO
+    { E.Auto }
   | n = NUMERAL;
     { E.Num n }
-  | BULLET
-    { E.TickConst }
 
 atomic_eterm:
   | e = atomic_econ
@@ -98,8 +100,6 @@ atomic_eterm:
 eframe:
   | e = atomic_eterm
     { E.App e }
-  | BANG
-    { E.Open }
   | DOT FST
     { E.Car }
   | DOT SND
@@ -169,21 +169,12 @@ econ:
   | LSQ; dims = nonempty_list(ATOM); RSQ; ty = eterm; sys = pipe_block(eface)
     { E.Ext (dims, ty, sys)}
 
-  | RESTRICT; ty = eterm; sys = pipe_block(eface)
-    { E.Rst (ty, sys)}
-
   | dom = atomic_eterm; RIGHT_ARROW; cod = eterm
     { E.Pi ([`Ty ("_", dom)], cod) }
 
   | dom = atomic_eterm; TIMES; cod = eterm
     { E.Sg ([`Ty ("_", dom)], cod) }
 
-  | BOX_MODALITY; ty = eterm
-    { E.Pi ([`Lock], ty)}
-
-  | SHUT; tm = eterm
-    { E.Shut tm }
-
 eterm:
   | e = econ
     { eterm $startpos $endpos e }
@@ -218,9 +209,6 @@ etele_cell:
     { [`I "_"] }
   | TICK
     { [`Tick "_"] }
-  | LOCK
-    { [`Lock] }
-
 
 
 desc_constr:
@@ -338,9 +326,6 @@ kind:
   | { `Kan }
 
 tm:
-  | BULLET
-    { fun _env ->
-      make_node $startpos $endpos Tm.TickConst }
 
   | i = NUMERAL
     { fun _env ->
@@ -379,17 +364,6 @@ tm:
       make_node $startpos $endpos @@
       Tm.Later (ty env) }
 
-  | LPR; BOX_MODALITY; ty = tm; RPR
-    { fun env ->
-      make_node $startpos $endpos @@
-      Tm.BoxModality (ty env) }
-
-  | LPR; rst = constrained; RPR
-    { fun env ->
-      let ty, sys = rst env in
-      make_node $startpos $endpos @@
-      Tm.Rst {ty; sys} }
-
   | LPR; LAM; mb = multibind(tm); RPR
     { fun env ->
       lam_from_multibind (Some ($startpos, $endpos)) @@ mb env }
@@ -399,11 +373,6 @@ tm:
       make_node $startpos $endpos @@
       Tm.Next (bnd env) }
 
-  | LPR; SHUT; tm = tm; RPR
-    { fun env ->
-      make_node $startpos $endpos @@
-      Tm.Shut (tm env) }
-
   | LPR; PAIR; e0 = tm; e1 = tm; RPR
     { fun env ->
       make_node $startpos $endpos @@
@@ -492,11 +461,6 @@ cut:
       let hd, fs = e env in
       hd, fs #< (Tm.Prev (t env)) }
 
-  | LPR; OPEN; e = cut; RPR
-    { fun env ->
-      let hd, fs = e env in
-      hd, fs #< Tm.Open }
-
   | LPR; e = cut; arg0 = tm; rest = elist(tm); RPR
     { fun env ->
       let hd, fs = e env in
diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll
index c7dbc5473..5023d10c7 100644
--- a/src/frontend/Lex.mll
+++ b/src/frontend/Lex.mll
@@ -32,14 +32,10 @@ module Make (R : SOURCE) : LEXER = struct
       ("where", WHERE);
       ("data", DATA);
       ("end", END);
-      ("[]", BOX_MODALITY);
-      ("□", BOX_MODALITY);
       ("tick", TICK);
       ("✓", TICK);
       ("dim", DIM);
       ("𝕀", DIM);
-      ("lock", LOCK);
-      ("🔓", LOCK);
       ("elim", ELIM);
       ("fst", FST);
       ("snd", SND);
@@ -50,20 +46,19 @@ module Make (R : SOURCE) : LEXER = struct
       ("comp", COMP);
       ("vproj", VPROJ);
       ("vin", VIN);
-      ("restrict", RESTRICT);
       ("let", LET);
       ("lam", LAM);
       ("next", NEXT);
       ("prev", PREV);
       ("dfix", DFIX);
       ("fix", FIX);
-      ("open", OPEN);
-      ("shut", SHUT);
       ("call", CALL);
+      ("auto", AUTO);
       ("pre", PRE);
       ("kan", KAN);
       ("U", UNIV);
       ("debug", DEBUG);
+      ("normalize", NORMALIZE);
       ("type", TYPE);
       ("import", IMPORT);
     ]
@@ -89,8 +84,6 @@ rule token = parse
     { Lwt.return (NUMERAL (int_of_string (Lexing.lexeme lexbuf))) }
   | ';'
     {comment lexbuf}
-  | '!'
-    { Lwt.return BANG }
   | '('
     { Lwt.return LPR }
   | ')'
@@ -137,10 +130,6 @@ rule token = parse
     { Lwt.return RRIGHT_ARROW }
   | "→"
     { Lwt.return RIGHT_ARROW }
-  | "<>"
-    { Lwt.return BULLET}
-  | "∙"
-    { Lwt.return BULLET }
   | "<"
     { Lwt.return LGL }
   | ">"
diff --git a/src/frontend/Refiner.ml b/src/frontend/Refiner.ml
index 71cdcd2ef..363d4891f 100644
--- a/src/frontend/Refiner.ml
+++ b/src/frontend/Refiner.ml
@@ -3,13 +3,22 @@ open RedTT_Core
 open Dev open Bwd open BwdNotation
 
 module D = Domain
-module M = ElabMonad
+module B = Desc.Boundary
+
+module M =
+struct
+  include ElabMonad
+  module Util = Monad.Util(ElabMonad)
+end
+
 module C = Contextual
 module U = Unify
 module Notation = Monad.Notation (M)
 open Notation
 
-type chk_tac = ty -> tm M.m
+type sys = (tm, tm) Tm.system
+type goal = {ty : ty; sys : sys}
+type chk_tac = goal -> tm M.m
 type inf_tac = (ty * tm) M.m
 
 open Tm.Notation
@@ -30,8 +39,21 @@ let normalize_ty ty =
   normalization_clock := !normalization_clock +. (now1 -. now0);
   M.ret ty
 
+let normalizing_goal tac goal =
+  normalize_ty goal.ty >>= fun ty ->
+  tac {goal with ty}
+
+let rec tac_fix ftac goal =
+  ftac (tac_fix ftac) goal
 
-let guess_restricted ty sys tm =
+let match_goal tac =
+  fun goal ->
+    tac goal goal
+
+
+let guess_restricted tm goal =
+  let ty = goal.ty in
+  let sys = goal.sys in
   let rty = Tm.make @@ Tm.Rst {ty; sys} in
   M.lift @@ C.check ~ty:rty tm >>= function
   | `Ok -> M.ret tm
@@ -58,105 +80,56 @@ let guess_restricted ty sys tm =
 
 exception ChkMatch
 
-(* The idea of this function is to push a restriction downward into a negative type.
-   It is perhaps a bit too ambitious to fully unleash, until we have developed the Immortal
-   subtyping and definitional equivalence theory that really gets down with eta laws of
-   restriction types. *)
-let rec push_restriction sys ty =
-  normalize_ty ty >>= fun ty ->
-  let on_sys f =
-    List.map @@ fun (r, r', otm) ->
-    r, r', Option.map f otm
-  in
-  match Tm.unleash ty with
-  | Tm.Rst rst ->
-    push_restriction (rst.sys @ sys) rst.ty
-  | Tm.Pi (dom, cod) ->
-    let x, codx = Tm.unbind cod in
-    let app_tm tm =
-      let var = Tm.up @@ Tm.var x in
-      Tm.up @@ Tm.ann ~ty ~tm @< Tm.FunApp var
-    in
-    let app_sys = on_sys app_tm sys in
-    let rcodx = Tm.make @@ Tm.Rst {ty = codx; sys = app_sys} in
-    let rty = Tm.make @@ Tm.Pi (dom, Tm.bind x rcodx) in
-    M.ret @@ `Negative rty
-
-  | Tm.Ext ebnd ->
-    let xs, tyxs, sysxs = Tm.unbind_ext ebnd in
-    let app_tm tm =
-      let vars = List.map (fun x -> Tm.up @@ Tm.var x) @@ Bwd.to_list xs in
-      Tm.up @@ Tm.ann ~ty ~tm @< Tm.ExtApp vars
+let bind_in_scope tm =
+  M.lift C.ask <<@> fun psi ->
+    let go (x, param) =
+      match param with
+      | `P _ -> [x]
+      | `Def _ -> [x]
+      | `I -> [x]
+      | `SelfArg _ -> [x]
+      | `Tick -> [x]
+      | `Tw _ -> []
+      | _ -> []
     in
-    let ebnd' = Tm.bind_ext xs tyxs @@ sysxs @ on_sys app_tm sys in
-    let rty = Tm.make @@ Tm.Ext ebnd' in
-    M.ret @@ `Negative rty
+    let xs = Bwd.flat_map go psi in
+    let Tm.NB (_, tm) = Tm.bindn xs tm in
+    tm
 
-  (* | Tm.Sg (dom, cod) ->
-     let car tm = Tm.up (Tm.Down {ty; tm}, Emp #< Tm.Car) in
-     let cdr tm = Tm.up (Tm.Down {ty; tm}, Emp #< Tm.Cdr) in
-     let x, codx = Tm.unbind cod in
-     let rdom = Tm.make @@ Tm.Rst {ty = dom; sys = on_sys car sys} in
-     let rcodx = Tm.make @@ Tm.Rst {ty = codx; sys = on_sys cdr sys} in
-     let rty = Tm.make @@ Tm.Sg (rdom, Tm.bind x rcodx) in
-     M.ret @@ `Negative rty *)
-
-
-  | _ ->
-    M.ret `Positive
-
-let rec tac_rst tac ty =
-  let rec go sys ty =
-    normalize_ty ty >>= fun ty ->
-    match Tm.unleash ty with
-    | Tm.Rst rst ->
-      go (rst.sys @ sys) rst.ty
-    | _ ->
-      begin
-        match sys with
-        | [] -> tac ty
-        | _ ->
-          normalize_ty ty >>= fun ty ->
-          push_restriction sys ty >>= function
-          | `Positive ->
-            tac_wrap_nf tac ty >>=
-            guess_restricted ty sys
-          | `Negative rty ->
-            tac_wrap_nf tac rty
-      end
-  in go [] ty
-
-
-and tac_wrap_nf tac ty =
-  try tac ty
+let tac_wrap_nf tac goal =
+  try tac goal
   with
   | ChkMatch ->
-    normalize_ty ty >>= tac_rst tac
+    normalize_ty goal.ty >>= fun ty ->
+    tac {ty; sys = goal.sys}
 
 
 let tac_let name itac ctac =
-  fun ty ->
+  fun goal ->
     itac >>= fun (let_ty, let_tm) ->
-    let singleton_ty =
-      let face = Tm.make Tm.Dim0, Tm.make Tm.Dim0, Some let_tm in
-      Tm.make @@ Tm.Rst {ty = let_ty; sys = [face]}
-    in
     let x = Name.named @@ Some name in
-    M.in_scope x (`P singleton_ty) (ctac ty) >>= fun bdyx ->
+    M.in_scope x (`Def (let_ty, let_tm)) (ctac goal) >>= fun bdyx ->
     M.ret @@ Tm.make @@ Tm.Let (Tm.ann ~ty:let_ty ~tm:let_tm, Tm.bind x bdyx)
 
 
-let rec tac_lambda names tac ty =
-  match Tm.unleash ty with
+let flip f x y = f y x
+
+let rec tac_lambda names tac goal =
+  match Tm.unleash goal.ty with
   | Tm.Pi (dom, cod) ->
     begin
       match names with
-      | [] -> tac ty
+      | [] -> tac goal
       | name :: names ->
         let x = Name.named @@ Some name in
         let codx = Tm.unbind_with (Tm.var x) cod in
+        let sysx =
+          flip List.map goal.sys @@ fun (r, r', otm) ->
+          r, r', flip Option.map otm @@ fun tm ->
+          Tm.up @@ Tm.ann ~ty:goal.ty ~tm @< Tm.FunApp (Tm.up @@ Tm.var x)
+        in
         M.in_scope x (`P dom) begin
-          tac_wrap_nf (tac_lambda names tac) codx
+          tac_wrap_nf (tac_lambda names tac) {ty = codx; sys = sysx}
         end >>= fun bdyx ->
         M.ret @@ Tm.make @@ Tm.Lam (Tm.bind x bdyx)
     end
@@ -164,12 +137,17 @@ let rec tac_lambda names tac ty =
   | Tm.Later cod ->
     begin
       match names with
-      | [] -> tac ty
+      | [] -> tac goal
       | name :: names ->
         let x = Name.named @@ Some name in
         let codx = Tm.unbind_with (Tm.var x) cod in
+        let sysx =
+          flip List.map goal.sys @@ fun (r, r', otm) ->
+          r, r', flip Option.map otm @@ fun tm ->
+          Tm.up @@ Tm.ann ~ty:goal.ty ~tm @< Tm.Prev (Tm.up @@ Tm.var x)
+        in
         M.in_scope x `Tick begin
-          tac_wrap_nf (tac_lambda names tac) codx
+          tac_wrap_nf (tac_lambda names tac) {ty = codx; sys = sysx}
         end >>= fun bdyx ->
         M.ret @@ Tm.make @@ Tm.Next (Tm.bind x bdyx)
     end
@@ -177,7 +155,7 @@ let rec tac_lambda names tac ty =
   | Tm.Ext (Tm.NB (nms, _) as ebnd) ->
     begin
       match names with
-      | [] -> tac ty
+      | [] -> tac goal
       | _ ->
         let rec bite nms lnames rnames =
           match nms, rnames with
@@ -188,11 +166,17 @@ let rec tac_lambda names tac ty =
           | _ -> failwith "Elab: incorrect number of binders when refining extension type"
         in
         let xs, tac' = bite nms Emp names in
-        let ty, sys = Tm.unbind_ext_with (Bwd.to_list @@ Bwd.map (fun x -> Tm.var x) xs) ebnd in
-        let rty = Tm.make @@ Tm.Rst {ty; sys} in
-        let ps = List.map (fun x -> (x, `I)) @@ Bwd.to_list xs in
+        let xs_fwd = Bwd.to_list xs in
+        let xs_tms = List.map (fun x -> Tm.var x) xs_fwd in
+        let tyxs, sysxs = Tm.unbind_ext_with xs_tms ebnd in
+        let ps = List.map (fun x -> (x, `I)) xs_fwd in
+        let sys'xs =
+          flip List.map goal.sys @@ fun (r, r', otm) ->
+          r, r', flip Option.map otm @@ fun tm ->
+          Tm.up @@ Tm.ann ~ty:goal.ty ~tm @< Tm.ExtApp (List.map Tm.up xs_tms)
+        in
         M.in_scopes ps begin
-          tac' rty
+          tac' {ty = tyxs; sys = sysxs @ sys'xs}
         end >>= fun bdyxs ->
         let lam = Tm.make @@ Tm.ExtLam (Tm.bindn xs bdyxs) in
         M.ret lam
@@ -201,12 +185,33 @@ let rec tac_lambda names tac ty =
   | _ ->
     begin
       match names with
-      | [] -> tac ty
+      | [] -> tac goal
       | _ ->
         raise ChkMatch
     end
 
-(* TODO factor out the motive inference algorithm *)
+let tac_pair tac0 tac1 : chk_tac =
+  fun goal ->
+    match Tm.unleash goal.ty with
+    | Tm.Sg (dom, cod) ->
+      let sys0 =
+        flip List.map goal.sys @@ fun (r, r', otm) ->
+        r, r', flip Option.map otm @@ fun tm ->
+        Tm.up @@ Tm.ann ~ty:goal.ty ~tm @< Tm.Car
+      in
+      let sys1 =
+        flip List.map goal.sys @@ fun (r, r', otm) ->
+        r, r', flip Option.map otm @@ fun tm ->
+        Tm.up @@ Tm.ann ~ty:goal.ty ~tm @< Tm.Cdr
+      in
+      tac0 {ty = dom; sys = sys0} >>= fun tm0 ->
+      let cmd0 = Tm.ann ~ty:dom ~tm:tm0 in
+      let cod' = Tm.make @@ Tm.Let (cmd0, cod) in
+      tac1 {ty = cod'; sys = sys1} >>= fun tm1 ->
+      M.ret @@ Tm.cons tm0 tm1
+
+    | _ ->
+      raise ChkMatch
 
 let unleash_data ty =
   match Tm.unleash ty with
@@ -229,7 +234,7 @@ let make_motive ~data_ty ~tac_mot ~scrut ~ty =
   | Some tac_mot ->
     let univ = Tm.univ ~lvl:`Omega ~kind:`Pre in
     let mot_ty = Tm.pi None data_ty univ in
-    tac_mot mot_ty >>= fun mot ->
+    tac_mot {ty = mot_ty; sys = []} >>= fun mot ->
     let motx =
       Tm.ann ~ty:(Tm.subst (Tm.shift 1) mot_ty) ~tm:(Tm.subst (Tm.shift 1) mot)
       @< Tm.FunApp (Tm.up @@ Tm.ix 0)
@@ -237,11 +242,11 @@ let make_motive ~data_ty ~tac_mot ~scrut ~ty =
     M.ret @@ Tm.B (None, Tm.up @@ motx)
 
 let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
-  fun ty ->
+  fun goal ->
     tac_scrut >>= fun (data_ty, scrut) ->
     normalize_ty data_ty >>= fun data_ty ->
 
-    make_motive ~data_ty ~scrut ~tac_mot ~ty >>= fun bmot ->
+    make_motive ~data_ty ~scrut ~tac_mot ~ty:goal.ty >>= fun bmot ->
 
     let mot arg =
       let Tm.B (_, motx) = bmot in
@@ -258,7 +263,7 @@ let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
     end >>= fun desc ->
 
     (* Add holes for any missing clauses *)
-    let clauses =
+    let eclauses =
       let find_clause lbl =
         try
           List.find (fun (lbl', _, _) -> lbl = lbl') clauses
@@ -270,10 +275,11 @@ let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
             @ List.mapi (fun i _ -> let x = "x" ^ string_of_int i in ESig.PIndVar (x, x ^ "/ih")) constr.rec_specs
             @ List.map (fun x -> ESig.PVar x) constr.dim_specs
           in
-          lbl, pbinds, fun ty ->
+          lbl, pbinds, fun goal ->
             M.lift C.ask >>= fun psi ->
-            M.lift @@ U.push_hole `Rigid psi ty >>= fun tm ->
-            M.emit loc @@ M.UserHole {name = Some lbl; ty; tele = psi; tm = Tm.up tm} >>
+            let rty = Tm.make @@ Tm.Rst {ty = goal.ty; sys = goal.sys} in
+            M.lift @@ U.push_hole `Rigid psi rty  >>= fun tm ->
+            M.emit loc @@ M.UserHole {name = Some lbl; ty = rty; tele = psi; tm = Tm.up tm} >>
             M.ret @@ Tm.up tm
       in
       List.map (fun (lbl, _) -> find_clause lbl) desc.constrs
@@ -289,7 +295,7 @@ let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
     let refine_clause earlier_clauses (clbl, pbinds, (clause_tac : chk_tac)) =
       let open Desc in
       let constr = lookup_constr clbl desc in
-      let rec go psi env (tms, cargs, rargs, rs) pbinds const_specs rec_specs dims =
+      let rec go psi env (tms, cargs, rargs, ihs, rs) pbinds const_specs rec_specs dims =
         match pbinds, const_specs, rec_specs, dims with
         | ESig.PVar nm :: pbinds, (_plbl, pty) :: const_specs, _, _->
           let x = Name.named @@ Some nm in
@@ -298,7 +304,7 @@ let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
           let x_el = V.reflect vty (D.Var {name = x; twin = `Only; ushift = 0}) [] in
           let x_tm = Tm.up @@ Tm.var x in
           let env' = D.Env.push (`Val x_el) env in
-          go (psi #< (x, `P tty)) env' (tms #< x_tm, cargs #< x_el, rargs, rs) pbinds const_specs rec_specs dims
+          go (psi #< (x, `P tty)) env' (tms #< x_tm, cargs #< x_el, rargs, ihs, rs) pbinds const_specs rec_specs dims
 
         | ESig.PVar nm :: pbinds, [], (_, Self) :: rec_specs, _ ->
           let x = Name.named @@ Some nm in
@@ -306,7 +312,7 @@ let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
           let x_tm = Tm.up @@ Tm.var x in
           let x_el = V.reflect data_vty (D.Var {name = x; twin = `Only; ushift = 0}) [] in
           let ih_ty = mot x_tm in
-          go (psi #< (x, `P data_ty) #< (x_ih, `P ih_ty)) env (tms #< x_tm, cargs, rargs #< x_el, rs) pbinds const_specs rec_specs dims
+          go (psi #< (x, `P data_ty) #< (x_ih, `P ih_ty)) env (tms #< x_tm, cargs, rargs #< x_el, ihs #< x_ih, rs) pbinds const_specs rec_specs dims
 
         | ESig.PIndVar (nm, nm_ih) :: pbinds, [], (_, Self) :: rec_specs, _ ->
           let x = Name.named @@ Some nm in
@@ -314,24 +320,24 @@ let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
           let x_tm = Tm.up @@ Tm.var x in
           let ih_ty = mot x_tm in
           let x_el = V.reflect data_vty (D.Var {name = x; twin = `Only; ushift = 0}) [] in
-          go (psi #< (x, `P data_ty) #< (x_ih, `P ih_ty)) env (tms #< x_tm, cargs, rargs #< x_el, rs) pbinds const_specs rec_specs dims
+          go (psi #< (x, `P data_ty) #< (x_ih, `P ih_ty)) env (tms #< x_tm, cargs, rargs #< x_el, ihs #< x_ih, rs) pbinds const_specs rec_specs dims
 
         | ESig.PVar nm :: pbinds, [], [], _ :: dims ->
           let x = Name.named @@ Some nm in
           let x_tm = Tm.up @@ Tm.var x in
           let r = `Atom x in
           let env' = D.Env.push (`Dim r) env in
-          go (psi #< (x, `I)) env' (tms #< x_tm, cargs, rargs, rs #< r) pbinds [] [] dims
+          go (psi #< (x, `I)) env' (tms #< x_tm, cargs, rargs, ihs, rs #< r) pbinds [] [] dims
 
         | _, [], [], [] ->
-          psi, Bwd.to_list tms, Bwd.to_list cargs, Bwd.to_list rargs, Bwd.to_list rs
+          psi, Bwd.to_list tms, Bwd.to_list cargs, Bwd.to_list rargs, ihs, Bwd.to_list rs
 
         | _ ->
           failwith "refine_clause"
       in
-      let psi, tms, const_args, rec_args, rs =
-        go Emp D.Env.emp (Emp, Emp, Emp, Emp) pbinds constr.const_specs constr.rec_specs constr.dim_specs
-      in
+
+      let psi, tms, const_args, rec_args, ihs, rs = go Emp D.Env.emp (Emp, Emp, Emp, Emp, Emp) pbinds constr.const_specs constr.rec_specs constr.dim_specs in
+      let sub = List.fold_left (fun sub (x,_) -> Tm.dot (Tm.var x) sub) (Tm.shift 0) (Bwd.to_list psi) in
       let intro = Tm.make @@ Tm.Intro (dlbl, clbl, tms) in
       let clause_ty = mot intro in
 
@@ -341,56 +347,100 @@ let tac_elim ~loc ~tac_mot ~tac_scrut ~clauses : chk_tac =
             cx, Cx.evaluator cx, Cx.quoter cx
         end >>= fun (cx, (module V), (module Q)) ->
 
-        let image_of_face face =
-          let elim_face r r' scrut =
-            let phi = I.equate r r' in
-            let rho = D.Env.act phi @@ Cx.env cx in
-            let mot = V.make_closure rho bmot in
-            let clauses = List.map (fun (clbl, nbnd) -> clbl, D.NClo {nbnd; rho}) earlier_clauses in
-            V.elim_data dlbl ~mot:mot ~scrut:scrut ~clauses
-          in
-          Face.map elim_face @@
-          let env0 = D.Env.clear_locals @@ Cx.env cx in
-          V.eval_bterm_face dlbl desc env0 face
-            ~const_args
-            ~rec_args
-            ~rs
+        let rec image_of_bterm phi =
+          function
+          | B.Intro intro as bterm ->
+            let nbnd : ty Tm.nbnd = snd @@ List.find (fun (clbl, _) -> clbl = intro.clbl) earlier_clauses in
+            let nclo = D.NClo {nbnd; rho = Cx.env cx} in
+            let cargs = List.map (fun t -> `Val (Cx.eval cx @@ Tm.subst sub t)) intro.const_args in
+            let rargs = List.map (fun bt -> `Val (image_of_bterm phi bt)) intro.rec_args in
+            let dims = List.map (fun t -> `Dim (Cx.eval_dim cx @@ Tm.subst sub t)) intro.rs in
+            let cells = cargs @ rargs @ dims in
+            V.inst_nclo nclo cells
+          | B.Var ix ->
+            let ix' = ix - List.length rs in
+            Cx.eval_cmd cx @@ Tm.var @@ Bwd.nth ihs ix'
+        in
+
+        let image_of_bface (tr, tr', btm) =
+          let env = Cx.env cx in
+          let r = V.eval_dim env @@ Tm.subst sub tr in
+          let r' = V.eval_dim env @@ Tm.subst sub tr' in
+          D.ValFace.make I.idn r r' @@ fun phi ->
+          image_of_bterm phi btm
         in
 
         (* What is the image of the boundary in the current fiber of the motive? *)
         let tsys =
-          let val_sys = List.map image_of_face constr.boundary in
+          let val_sys = List.map image_of_bface constr.boundary in
           let vty = Cx.eval cx clause_ty in
           Q.quote_val_sys (Cx.qenv cx) vty val_sys
         in
 
         (* We run the clause tactic with the goal type restricted by the boundary above *)
-        let clause_rty =
-          match tsys with
-          | [] -> clause_ty
-          | _ -> Tm.make @@ Tm.Rst {ty = clause_ty; sys = tsys}
-        in
-
-        clause_tac clause_rty <<@> fun bdy ->
+        clause_tac {ty = clause_ty; sys = tsys} <<@> fun bdy ->
           clbl, Tm.bindn (Bwd.map fst psi) bdy
       end
     in
 
-    let rec refine_clauses acc =
-      function
-      | [] ->
-        M.ret acc
-      | clause :: clauses ->
-        refine_clause acc clause >>= fun tclause ->
-        refine_clauses (tclause :: acc) clauses
-    in
-
-    refine_clauses [] clauses >>= fun tclauses ->
+    M.Util.fold_left (fun acc clause -> refine_clause acc clause <<@> fun cl -> cl :: acc) [] eclauses >>= fun clauses ->
+    M.ret @@ Tm.up @@ Tm.ann ~ty:data_ty ~tm:scrut @< Tm.Elim {dlbl; mot = bmot; clauses}
+
+let rec tac_hope goal =
+  let rst = Tm.make @@ Tm.Rst {ty = goal.ty; sys = goal.sys} in
+  let rec try_system sys =
+    match sys with
+    | [] ->
+      M.lift C.ask >>= fun psi ->
+      let rty = Tm.make @@ Tm.Rst {ty = goal.ty; sys = goal.sys} in
+      M.lift @@ U.push_hole `Flex psi rty <<@> Tm.up
+    | (r, r', Some tm) :: sys ->
+      begin
+        M.lift @@ C.check ~ty:rst tm >>=
+        function
+        | `Ok ->
+          M.ret tm
+        | _ ->
+          try_system sys
+      end
+    | _ :: sys ->
+      try_system sys
+  in
+  try_system goal.sys
+
+let tac_hole ~loc ~name : chk_tac =
+  fun goal ->
+    M.lift C.ask >>= fun psi ->
+    let rty = Tm.make @@ Tm.Rst {ty = goal.ty; sys = goal.sys} in
+    M.lift @@ U.push_hole `Rigid psi rty >>= fun cmd ->
+    let tm = Tm.up cmd in
+    begin
+      if name = Some "_" then M.ret () else
+        M.emit loc @@ M.UserHole {name; ty = rty; tele = psi; tm}
+    end >>
+    M.ret tm
+
+let tac_guess tac : chk_tac =
+  fun goal ->
+    tac {goal with sys = []} >>= fun tm ->
+    let rty = Tm.make @@ Tm.Rst {ty = goal.ty; sys = goal.sys} in
+    M.lift C.ask >>= fun psi ->
+    M.lift @@ U.push_guess psi ~ty0:rty ~ty1:goal.ty tm
+
+let tac_auto =
+  tac_fix @@ fun tac_auto ->
+  normalizing_goal @@ match_goal @@ fun goal ->
+  match Tm.unleash goal.ty with
+  | Tm.Ext (Tm.NB (nms, _)) ->
+    let nms' = Bwd.to_list @@ Bwd.map (function Some nm -> nm | None -> "_") nms in
+    tac_lambda nms' tac_auto
+
+  | Tm.Pi (dom, Tm.B (nm, _)) ->
+    let nms = [match nm with Some nm -> nm | None -> "_"] in
+    tac_lambda nms tac_auto
+
+  | Tm.Sg (_, _) ->
+    tac_pair tac_auto tac_auto
 
-    let bmot =
-      let x = Name.fresh () in
-      Tm.bind x @@ mot @@ Tm.up @@ Tm.var x
-    in
-    M.ret @@ Tm.up @@
-    Tm.ann ~ty:data_ty ~tm:scrut
-    @< Tm.Elim {dlbl; mot = bmot; clauses = tclauses}
+  | _ ->
+    tac_hope
diff --git a/src/frontend/Refiner.mli b/src/frontend/Refiner.mli
index 96e55ed1f..396a2bfee 100644
--- a/src/frontend/Refiner.mli
+++ b/src/frontend/Refiner.mli
@@ -2,25 +2,54 @@ open Dev
 open RedTT_Core
 open ElabMonad
 
-type chk_tac = ty -> tm m
+type sys = (tm, tm) Tm.system
+type goal = {ty : ty; sys : sys}
+type chk_tac = goal -> tm m
 type inf_tac = (ty * tm) m
 
 exception ChkMatch
 
+(** Decompose the current goal and try to solve it automatically. *)
+val tac_auto : chk_tac
+
+(** Try to solve the current goal using the current restriction, and/or unification. *)
+val tac_hope : chk_tac
+
+(** Unleash a hole named [name]. *)
+val tac_hole : loc:location -> name:string option -> chk_tac
+
+(** Run the input tactic without the restriction, and then store the result
+    as a guess for the current hole in the proof state. *)
+val tac_guess : chk_tac -> chk_tac
+
+
+val tac_fix : (chk_tac -> chk_tac) -> chk_tac
+val match_goal : (goal -> chk_tac) -> chk_tac
+
+
 (** Try to run a tactic against the current type, but if it raises [ChkMatch], re-run it after normalizing the type. *)
 val tac_wrap_nf : chk_tac -> chk_tac
 
-
 (** Multi-introduction tactic *)
 val tac_lambda : string list -> chk_tac -> chk_tac
 
-val tac_elim : loc:location -> tac_mot:chk_tac option -> tac_scrut:inf_tac -> clauses:(Desc.con_label * ESig.epatbind list * chk_tac) list -> chk_tac
+(** Introduce a sigma type *)
+val tac_pair : chk_tac -> chk_tac -> chk_tac
 
+(** Call a data elimination rule. *)
+val tac_elim
+  : loc:location
+  -> tac_mot:chk_tac option
+  -> tac_scrut:inf_tac
+  -> clauses:(Desc.con_label * ESig.epatbind list * chk_tac) list
+  -> chk_tac
+
+(** Introduce a let-binding. *)
 val tac_let : string -> inf_tac -> chk_tac -> chk_tac
 
+(** Try to solve a goal with a term, unifying it against the ambient restriction. *)
+val guess_restricted : tm -> chk_tac
 
-(** A tactical which adds support for restriction *)
-val tac_rst : chk_tac -> chk_tac
 
 val normalize_ty : ty -> ty m
-
+val bind_in_scope : tm -> tm m
diff --git a/src/frontend/Unify.ml b/src/frontend/Unify.ml
index 8d47df5f6..9f2f8947e 100644
--- a/src/frontend/Unify.ml
+++ b/src/frontend/Unify.ml
@@ -28,10 +28,6 @@ let rec telescope ty : telescope * ty =
     let x, codx = Tm.unbind cod in
     let tel, ty = telescope codx in
     (Emp #< (x, `Tick)) <.> tel, ty
-  | Tm.BoxModality ty ->
-    let x = Name.fresh () in
-    let tel, ty = telescope ty in
-    (Emp #< (x, `Lock)) <.> tel, ty
   | _ ->
     Emp, ty
 
@@ -40,17 +36,15 @@ let rec abstract_tm xs tm =
   | Emp -> tm
   | Snoc (xs, (x, `P _)) ->
     abstract_tm xs @@ Tm.make @@ Tm.Lam (Tm.bind x tm)
+  | Snoc (xs, (x, `Def (ty, def))) ->
+    abstract_tm xs @@ Tm.unbind_with (Tm.ann ~ty ~tm:def) @@ Tm.bind x tm
   | Snoc (xs, (x, `Tick)) ->
     abstract_tm xs @@ Tm.make @@ Tm.Next (Tm.bind x tm)
   | Snoc (xs, (x, `I)) ->
     let bnd = Tm.NB (Emp #< None, Tm.close_var x 0 tm) in
     abstract_tm xs @@ Tm.make @@ Tm.ExtLam bnd
-  | Snoc (xs, (_, `Lock)) ->
-    abstract_tm xs @@ Tm.make @@ Tm.Shut tm
   | Snoc (xs, (_, `R (r, r'))) ->
     abstract_tm xs @@ Tm.make @@ Tm.CoRThunk (r, r', Some tm)
-  | Snoc (xs, (_, `ClearLocks)) ->
-    abstract_tm xs tm
   | Snoc (xs, (_, `KillFromTick _)) ->
     abstract_tm xs tm
   | _ ->
@@ -61,6 +55,8 @@ let rec abstract_ty (gm : telescope) cod =
   | Emp -> cod
   | Snoc (gm, (x, `P dom)) ->
     abstract_ty gm @@ Tm.make @@ Tm.Pi (dom, Tm.bind x cod)
+  | Snoc (gm, (x, `Def (dom, def))) ->
+    abstract_ty gm @@ Tm.unbind_with (Tm.ann ~ty:dom ~tm:def) @@ Tm.bind x cod
   | Snoc (gm, (_, `R (r, r'))) ->
     abstract_ty gm @@ Tm.make @@ Tm.CoR (r, r', Some cod)
   | Snoc (gm, (x, `I)) ->
@@ -68,10 +64,6 @@ let rec abstract_ty (gm : telescope) cod =
     abstract_ty gm @@ Tm.make @@ Tm.Ext (Tm.NB (Emp #< (Name.name x), (cod', [])))
   | Snoc (gm, (x, `Tick)) ->
     abstract_ty gm @@ Tm.make @@ Tm.Later (Tm.bind x cod)
-  | Snoc (gm, (_, `Lock)) ->
-    abstract_ty gm @@ Tm.make @@ Tm.BoxModality cod
-  | Snoc (gm, (_, `ClearLocks)) ->
-    abstract_ty gm cod
   | Snoc (gm, (_, `KillFromTick _)) ->
     abstract_ty gm cod
   | _ ->
@@ -84,6 +76,8 @@ let telescope_to_spine : telescope -> tm Tm.spine =
     [Tm.ExtApp [Tm.up @@ Tm.var x]]
   | `P _ ->
     [Tm.FunApp (Tm.up @@ Tm.var x)]
+  | `Def _ ->
+    []
   | `SelfArg _ ->
     (* ??? *)
     [Tm.FunApp (Tm.up @@ Tm.var x)]
@@ -93,10 +87,6 @@ let telescope_to_spine : telescope -> tm Tm.spine =
     [Tm.CoRForce]
   | `Tick ->
     [Tm.Prev (Tm.up @@ Tm.var x)]
-  | `Lock ->
-    [Tm.Open]
-  | `ClearLocks ->
-    []
   | `KillFromTick _ ->
     []
 
@@ -397,8 +387,8 @@ let plug (ty, tm) frame =
   let (module V) = Cx.evaluator cx in
 
   match Tm.unleash tm, frame with
-  | Tm.Up (hd, sp), _ ->
-    ret @@ Tm.up (hd, sp #< frame)
+  | Tm.Up cmd, _ ->
+    ret @@ Tm.up @@ cmd @< frame
   | Tm.Lam bnd, Tm.FunApp arg ->
     let dom, cod = V.unleash_pi ty in
     inst_bnd (cod, bnd) (dom, arg)
@@ -888,7 +878,7 @@ let rec solver prob =
     else
       begin
         match param with
-        | `I | `Tick | `Lock | `ClearLocks | `KillFromTick _ | `SelfArg _ as p ->
+        | `I | `Tick | `KillFromTick _ | `SelfArg _ as p ->
           in_scope x p @@
           solver probx
 
@@ -904,6 +894,18 @@ let rec solver prob =
               solver probx
           end
 
+        | `Def (ty, tm) ->
+          begin
+            (* match split_sigma Emp x ty with
+               | Some (y, ty0, z, ty1, s, _) ->
+               (in_scopes [(y, `P ty0); (z, `P ty1)] get_global_env) >>= fun env ->
+               solver @@ Problem.all y ty0 @@ Problem.all z ty1 @@
+               Problem.subst (GlobalEnv.define env x ~ty ~tm:s) probx
+               | None -> *)
+            in_scope x (`Def (ty, tm)) @@
+            solver probx
+          end
+
         | `Tw (ty0, ty1) ->
           let univ = Tm.univ ~lvl:`Omega ~kind:`Pre in
           begin
diff --git a/src/frontend/dune b/src/frontend/dune
index c98920d82..1cbf08153 100644
--- a/src/frontend/dune
+++ b/src/frontend/dune
@@ -9,9 +9,9 @@
  (public_name redtt)
  ; for warning numbers (the part after "-w") see "ocamlc -warn-help"
  (flags
-  (:standard -w +a-3-4-6-9-22-30-32-39-40-41-42-44-48-60 -safe-string -short-paths -strict-formats -strict-sequence))
+  (:standard -w +a-3-4-6-9-22-26-27-30-32-39-40-41-42-44-48-60 -safe-string -short-paths -strict-formats -strict-sequence))
  (ocamlopt_flags
-  (:standard -w +a-3-4-6-9-22-30-32-39-40-41-42-44-48-60 -safe-string -short-paths -strict-formats -strict-sequence -O3 -bin-annot -unbox-closures -inlining-report))
+  (:standard -w +a-3-4-6-9-22-26-27-30-32-39-40-41-42-44-48-60 -safe-string -short-paths -strict-formats -strict-sequence -O3 -bin-annot -unbox-closures -inlining-report))
  (libraries
   lwt.unix
   redbasis
diff --git a/torus.red b/torus.red
index 79f0acc63..b12e595e0 100644
--- a/torus.red
+++ b/torus.red
@@ -1,5 +1,9 @@
 import path
 import s1
+import isotoequiv
+
+; cubicaltt version: https://github.com/mortberg/cubicaltt/blob/master/examples/torus.ctt
+; cubical agda version: https://github.com/Saizan/cubical-demo/blob/hits-transp/examples/Cubical/Examples/Torus.agda
 
 data torus where
 | pt
@@ -17,7 +21,74 @@ let t2c (t : torus) : s1 × s1 =
   | pt ⇒ <base, base>
   | p/one i ⇒ <loop i, base>
   | p/two i ⇒ <base, loop i>
-  | square i j ⇒ <loop j, loop i>
+  | square i j ⇒ auto
+  ]
+
+let c2t/base (c : s1) : torus =
+  elim c [
+  | base ⇒ pt
+  | loop i ⇒ p/two i
+  ]
+
+let c2t/transpose (c : s1) : s1 → torus =
+  elim c [
+  | base ⇒ λ c' →
+    elim c' [
+    | base ⇒ pt
+    | loop j ⇒ p/two j
+    ]
+
+  | loop i ⇒ λ c' →
+    elim c' [
+    | base ⇒ p/one i
+    | loop j ⇒ square j i
+    ]
+  ]
+
+
+
+let c2t (cs : s1 × s1) : torus =
+  c2t/transpose (cs.0) (cs.1)
+
+let t2c2t (t : torus) : Path torus (c2t (t2c t)) t =
+  elim t [
+  | pt ⇒ auto
+  | p/one i ⇒ auto
+  | p/two i ⇒ auto
+  | square i j ⇒ auto
+  ]
+
+
+let c2t2c/transpose (c0 : s1) : (c1 : s1) → Path (s1 × s1) (t2c (c2t/transpose c0 c1)) <c0, c1> =
+  elim c0
+  [ base ⇒ λ c1 →
+    elim c1
+    [ base ⇒ auto
+    | loop j ⇒ auto
+    ]
+
+  | loop i ⇒ λ c1 →
+    elim c1
+    [ base ⇒ auto
+    | loop j ⇒ auto
+    ]
   ]
 
-debug
+
+let c2t2c (cs : s1 × s1) : Path (s1 × s1) (t2c (c2t cs)) cs =
+  c2t2c/transpose (cs.0) (cs.1)
+
+
+let torus/s1s1/iso : Iso (s1 × s1) torus =
+  < c2t
+  , t2c
+  , t2c2t
+  , c2t2c
+  >
+
+
+let torus/s1s1/equiv : Equiv (s1 × s1) torus =
+  Iso/Equiv (s1 × s1) torus torus/s1s1/iso
+
+let torus/s1s1/path : Path^1 type (s1 × s1) torus =
+  UA (s1 × s1) torus torus/s1s1/equiv
diff --git a/univalence.red b/univalence.red
index bb55bd3c7..73cf62b71 100644
--- a/univalence.red
+++ b/univalence.red
@@ -29,23 +29,23 @@ let RetIsContr
     λ a i →
       comp 0 1 (g (c.1 (f a) i)) [
       | i=0 ⇒ h a
-      | i=1 ⇒ λ _ → g (c.0)
+      | i=1 ⇒ auto
       ]
   >
 
 let IdEquiv (A : type) : Equiv A A =
   < λ a → a
   , λ a →
-    < <a, λ _ → a>
+    < <a, auto>
     , λ p i →
       let aux : dim → A =
         λ j →
         comp 1 j a [
-        | i=0 ⇒ λ k → p.1 k
-        | i=1 ⇒ λ _ → a
+        | i=0 ⇒ p.1
+        | i=1 ⇒ auto
         ]
       in
-      <aux 0, λ j → aux j>
+      <aux 0, aux>
     >
   >
 
@@ -69,10 +69,10 @@ let PropSet
   =
   λ a b p q i j →
     comp 0 1 a [
-    | j=0 ⇒ λ k → A/prop a a k
-    | j=1 ⇒ λ k → A/prop a b k
-    | i=0 ⇒ λ k → A/prop a (p j) k
-    | i=1 ⇒ λ k → A/prop a (q j) k
+    | j=0 ⇒ A/prop a a
+    | j=1 ⇒ A/prop a b
+    | i=0 ⇒ A/prop a (p j)
+    | i=1 ⇒ A/prop a (q j)
     ]
 
 let LemSig
@@ -87,7 +87,7 @@ let LemSig
     , let coe0 = coe 0 i (u.1) in λ j → B (P j) in
       let coe1 = coe 1 i (v.1) in λ j → B (P j) in
       B/prop (P i) coe0 coe1 i
-     >
+    >
 
 
 let PropSig
@@ -97,8 +97,7 @@ let PropSig
   : IsProp ((a : A) × B a)
   =
   λ u v →
-    LemSig _ _ B/prop _ _ (A/prop (u.0) (v.0))
-
+    LemSig A B B/prop u v (A/prop (u.0) (v.0))
 
 opaque
 let PropIsContr (A : type) : IsProp (IsContr A) =
@@ -106,13 +105,13 @@ let PropIsContr (A : type) : IsProp (IsContr A) =
     let A/prop : IsProp A =
       λ a b i →
         comp 1 0 (contr.1 a i) [
-        | i=0 ⇒ λ _ → a
-        | i=1 ⇒ λ j → contr.1 b j
+        | i=0 ⇒ auto
+        | i=1 ⇒ contr.1 b
         ]
     in
 
     let contr/A/prop =
-      PropSig A (λ a → (b : A) → Path A b a) A/prop
+      PropSig _ (λ a → (b : A) → Path A b a) A/prop
         (λ a → PropPi A (λ b → Path A b a) (λ b → PropSet A A/prop b a))
     in
 
@@ -134,16 +133,12 @@ let EquivLemma
 ; per Dan Licata, UA and UABeta suffice for full univalence:
 ; https://groups.google.com/forum/#!topic/homotopytypetheory/j2KBIvDw53s
 
-let UA (A,B : type) (E : Equiv A B) : Path^1 type A B =
-  λ i →
-    `(V i A B E)
-
 let UA/beta
   (A,B : type) (E : Equiv A B) (a : A)
   : Path _ (coe 0 1 a in UA _ _ E) (E.0 a)
   =
   λ i →
-    coe i 1 (E.0 a) in λ _ → B
+    coe i 1 (E.0 a) in auto
 
 let SigEquivToPath
   (A : type)
@@ -187,12 +182,12 @@ let IsContrPath (A : type) : IsContr^1 ((B : _) × Path^1 type A B) =
   , λ X i →
     < comp 0 1 A [
       | i=0 ⇒ X.1
-      | i=1 ⇒ λ _ → A
+      | i=1 ⇒ auto
       ]
     , λ j →
       comp 0 j A [
       | i=0 ⇒ X.1
-      | i=1 ⇒ λ _ → A
+      | i=1 ⇒ auto
       ]
     >
   >
@@ -214,7 +209,7 @@ let univalence (A : type) : IsContr^1 ((B : type) × Equiv A B) =
 let IdEquiv/connection (B : type) : Equiv B B =
   < λ b → b
   , λ b →
-    < <b, λ _ → b>
+    < <b, auto>
     , λ v i → <v.1 i, λ j → connection/or B (v.1) i j>
     >
   >
@@ -222,37 +217,37 @@ let IdEquiv/connection (B : type) : Equiv B B =
 let univalence/alt (B : type) : IsContr^1 ((A : type) × Equiv A B) =
   < <B, IdEquiv/connection B>
   , λ w i →
-       let VB : type = `(V i (fst w) B (snd w)) in
-       let proj/B : VB → B = λ g → `(vproj i g (fst w) B (snd w)) in
-       < VB
-       , proj/B
-       , λ b →
-            let ctr/B : dim → B =
-              λ j →
-                comp 1 j b [
-                | i=0 ⇒ λ k → w .1 .1 b .0 .1 k
-                | i=1 ⇒ λ _ → b
-                ]
-            in
-            let ctr : Fiber VB B proj/B b =
-              < `(vin i (fst (fst ((snd (snd w)) b))) (@ ctr/B 0)), λ l → ctr/B l >
-            in
-            < ctr
-            , λ v j →
-                let filler : dim → B =
-                  λ l →
-                    comp 1 l b [
-                    | i=0 ⇒ λ k → w .1 .1 b .1 v j .1 k
-                    | i=1 ⇒ λ k → connection/or B (v .1) j k
-                    | j=0 ⇒ λ k → v .1 k
-                    | j=1 ⇒ λ k → ctr/B k
-                    ]
-                in
-                < `(vin i (fst (@ ((snd ((snd (snd w)) b)) v) j)) (@ filler 0))
-                , λ j → filler j
-                >
-            >
-       >
+      let VB : type = `(V i (fst w) B (snd w)) in
+      let proj/B : VB → B = λ g → `(vproj i g (fst w) B (snd w)) in
+      < _
+      , proj/B
+      , λ b →
+           let ctr/B : dim → B =
+             λ j →
+               comp 1 j b [
+               | i=0 ⇒ w .1 .1 b .0 .1
+               | i=1 ⇒ auto
+               ]
+           in
+           let ctr : Fiber VB B proj/B b =
+             < `(vin i (fst (fst ((snd (snd w)) b))) (@ ctr/B 0)), ctr/B >
+           in
+           < ctr
+           , λ v j →
+               let filler : dim → B =
+                 λ l →
+                   comp 1 l b [
+                   | i=0 ⇒ w .1 .1 b .1 v j .1
+                   | i=1 ⇒ λ k → connection/or B (v .1) j k
+                   | j=0 ⇒ v .1
+                   | j=1 ⇒ ctr/B
+                   ]
+               in
+               < `(vin i (fst (@ ((snd ((snd (snd w)) b)) v) j)) (@ filler 0))
+               , filler
+               >
+           >
+      >
   >
 
 
diff --git a/vim/syntax/redtt.vim b/vim/syntax/redtt.vim
index a692c1dab..02b1f738b 100644
--- a/vim/syntax/redtt.vim
+++ b/vim/syntax/redtt.vim
@@ -29,7 +29,7 @@ syn keyword redttKeyw pre kan U type then else
 syn keyword redttKeyw open shut tick dim prev next dfix fix
 
 
-syn keyword redttDecl opaque let debug import quit
+syn keyword redttDecl opaque let debug normalize import quit
 
 syn match   redttSymb '[#@`|\[\]^*×:,.∙✓□▷=⇒→<>λ]\|->'