From bba4c5705d6c8063e028165c0303f5a60a07cdf2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Tue, 4 May 2021 00:35:11 -0300
Subject: [PATCH] Some fixes to prove univalence

---
 intro.tt                      | 294 ++++++++++++++++++++++++++++------
 src/Elab.hs                   |  64 ++++----
 src/Elab/Eval.hs              | 192 +++++++++++++---------
 src/Elab/Eval/Formula.hs      |   6 +-
 src/Elab/Eval/Formula.hs-boot |  18 +++
 src/Elab/WiredIn.hs           |  21 +--
 src/Main.hs                   |  37 +++--
 src/Syntax.hs                 |   9 +-
 src/Syntax/Pretty.hs          |  13 +-
 9 files changed, 469 insertions(+), 185 deletions(-)
 create mode 100644 src/Elab/Eval/Formula.hs-boot

diff --git a/intro.tt b/intro.tt
index ecd0e79..7d2c035 100644
--- a/intro.tt
+++ b/intro.tt
@@ -115,23 +115,23 @@ singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))
 
 -- Some more operations on paths. By rearranging parentheses we get a
 -- proof that the images of equal elements are themselves equal.
-cong : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)
-cong f p i = f (p i)
+ap : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)
+ap f p i = f (p i)
 
--- These satisfy definitional equalities, like congComp and congId, which are
+-- These satisfy definitional equalities, like apComp and apId, which are
 -- propositional in vanilla MLTT.
-congComp : {A : Type} {B : Type} {C : Type}
+apComp : {A : Type} {B : Type} {C : Type}
            {f : A -> B} {g : B -> C} {x : A} {y : A}
            (p : Path x y)
-        -> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)
-congComp p = refl
+        -> Path (ap g (ap f p)) (ap (\x -> g (f x)) p)
+apComp p = refl
 
-congId : {A : Type} {x : A} {y : A}
+apId : {A : Type} {x : A} {y : A}
          (p : Path x y)
-     -> Path (cong (id {A}) p) p
-congId p = refl
+     -> Path (ap (id {A}) p) p
+apId p = refl
 
--- Just like rearranging parentheses gives us cong, swapping the value
+-- Just like rearranging parentheses gives us ap, swapping the value
 -- and interval binders gives us function extensionality.
 funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
          (h : (x : A) -> Path (f x) (g x))
@@ -270,14 +270,20 @@ trans {A} {x} p q i =
 transp : (A : I -> Type) (x : A i0) -> A i1
 transp A x = comp A {i0} (\i [ ]) (inS x)
 
+subst : {A : Type} (P : A -> Type) {x : A} {y : A} -> Path x y -> P x -> P y
+subst P p x = transp (\i -> P (p i)) x
+
 -- Since we have the iand operator, we can also derive the *filler* of a cube,
 -- which connects the given face and the output of composition.
 
-fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) (a0 : Sub (A i0) phi (u i0)) -> PathP A (outS a0) (comp A {phi} u a0)
+fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) (a0 : Sub (A i0) phi (u i0))
+    -> PathP A (outS a0) (comp A {phi} u a0)
 fill A {phi} u a0 i =
     comp (\j -> A (iand i j))
          {ior phi (inot i)}
-         (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])
+         (\j [ (phi = i1) -> u (iand i j) itIs1
+             , (i = i0)   -> outS a0
+             ])
          (inS (outS a0))
 
 hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A
@@ -467,6 +473,9 @@ lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)
 idToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
 idToEquiv p = lineToEquiv (\i -> p i)
 
+isEquivTransport : (A : I -> Type) -> isEquiv (transp A)
+isEquivTransport A = (lineToEquiv A).2
+
 -- The fact that this diagram has 2 filled-in B sides explains the
 -- complication in the proof below.
 --
@@ -503,6 +512,12 @@ J : {A : Type} {x : A}
  -> P y p
 J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d
 
+JRefl : {A : Type} {x : A}
+        (P : (y : A) -> Path x y -> Type)
+        (d : P x (\i -> x))
+     -> Path (J {A} {x} P d {x} (\i -> x)) d
+JRefl P d i = transpFill {\i -> P x (\j -> x)} d (inot i)
+
 Jay : {A : Type} {x : A}
       (P : ((y : A) * Path x y) -> Type)
       (d : P (x, refl))
@@ -793,35 +808,34 @@ predZ = \case
 
 -- And prove that the successor function is an isomorphism, and thus, an
 -- equivalence.
+sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
+sucPredZ = \case
+  pos n ->
+    let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
+        k = \case
+          zero -> refl
+          succ n -> refl
+     in k n
+  neg n -> refl
+
+predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
+predSucZ = \case
+  pos n -> refl
+  neg n ->
+    let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
+        k = \case
+          zero -> refl
+          succ n -> refl
+     in k n
 
-sucEquiv : isIso sucZ
-sucEquiv = 
-  let
-    sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
-    sucPredZ = \case
-      pos n ->
-        let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
-            k = \case
-              zero -> refl
-              succ n -> refl
-         in k n
-      neg n -> refl
-    predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
-    predSucZ = \case
-      pos n -> refl
-      neg n ->
-        let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
-            k = \case
-              zero -> refl
-              succ n -> refl
-         in k n
-   in (predZ, sucPredZ, predSucZ)
+sucEquiv : Equiv Int Int
+sucEquiv = IsoToEquiv (sucZ, (predZ, sucPredZ, predSucZ))
 
 -- Univalence gives us a path between integers such that transp intPath
 -- x = suc x, transp (sym intPath) x = pred x
 
 intPath : Path Int Int
-intPath = univalence (IsoToEquiv (sucZ, sucEquiv))
+intPath = univalence sucEquiv
 
 -- Higher inductive types
 -------------------------
@@ -906,12 +920,37 @@ goAround =
     forwards : Nat -> Path base base
     forwards = \case
       zero -> refl
-      succ n -> trans (forwards n) (\i -> loop i)
+      succ n -> trans (goAround (pos n)) (\i -> loop i)
     backwards : Nat -> Path base base
     backwards = \case
       zero -> \i -> loop (inot i)
-      succ n -> trans (backwards n) (\i -> loop (inot i))
-    
+      succ n -> trans (goAround (neg n)) (\i -> loop (inot i))
+
+windingGoAround : (n : Int) -> Path (winding (goAround n)) n
+windingGoAround =
+  \case
+    pos n -> posCase n
+    neg n -> negCase n
+  where
+    posCase : (n : Nat) -> Path (winding (goAround (pos n))) (pos n)
+    posCase = \case
+      zero -> refl
+      succ n -> ap sucZ (posCase n)
+    negCase : (n : Nat) -> Path (winding (goAround (neg n))) (neg n)
+    negCase = \case
+      zero -> refl
+      succ n -> ap predZ (negCase n)
+
+decodeSquare : (n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n)
+decodeSquare = \case
+    pos n -> posCase n
+    neg n -> \i j -> hfill (\k [ (j = i1) -> loop (inot k), (j = i0) -> base ]) (inS (goAround (neg n) j)) (inot i)
+  where
+    posCase : (n : Nat) -> PathP (\i -> Path base (loop i)) (goAround (predZ (pos n))) (goAround (pos n))
+    posCase = \case
+      zero -> \i j -> loop (ior i (inot j))
+      succ n -> \i j -> hfill (\k [ (j = i1) -> loop k, (j = i0) -> base ]) (inS (goAround (pos n) j)) i
+
 -- One particularly general higher inductive type is the homotopy pushout,
 -- which can be seen as a kind of sum B + C with the extra condition that
 -- whenever x and y are in the image of f (resp. g), inl x ≡ inr y.
@@ -963,8 +1002,8 @@ Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp
 
   poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x
   poSusp_to_Susp_to_poSusp {A} = \case
-    inl x -> cong inl (sym (unitEta x))
-    inr x -> cong inr (sym (unitEta x))
+    inl x -> ap inl (sym (unitEta x))
+    inr x -> ap inr (sym (unitEta x))
     push x i -> refl
 
 data T2 : Type where
@@ -1104,6 +1143,19 @@ isProp_isSet h a b p q j i =
 isProp_isProp : {A : Type} -> isProp (isProp A)
 isProp_isProp f g i a b = isProp_isSet f a b (f a b) (g a b) i
 
+isProp_isContr : {A : Type} -> isProp (isContr A)
+isProp_isContr {A} z0 z1 j =
+  ( z0.2 z1.1 j
+  , \x i -> hcomp {A} (\k [ (i = i0) -> z0.2 z1.1 j
+                          , (i = i1) -> z0.2 x (ior j k)
+                          , (j = i0) -> z0.2 x (iand i k)
+                          , (j = i1) -> z1.2 x i ])
+                      (inS (z0.2 (z1.2 x i) j))
+  )
+
+isContr_isProp : {A : Type} -> isContr A -> isProp A
+isContr_isProp x a b i = hcomp (\k [ (i = i0) -> x.2 a k, (i = i1) -> x.2 b k ]) (inS x.1)
+
 sigmaPath : {A : Type} {B : A -> Type} {s1 : (x : A) * B x} {s2 : (x : A) * B x}
          -> (p : Path s1.1 s2.1)
          -> PathP (\i -> B (p i)) s1.2 s2.2
@@ -1155,7 +1207,7 @@ S2IsSuspS1 = univalence (IsoToEquiv iso) where
   suspSurf i j = hfill {Susp S1} (\k [ (i = i0) -> north
                                      , (i = i1) -> merid base (inot k)
                                      , (j = i0) -> merid base (iand (inot k) i)
-                                     , (j = i1) -> merid base (iand (inot k) i)
+                                     , (j = i1) -> merid {S1} base (iand (inot k) i)
                                      ])
                                  (inS (merid (loop j) i))
 
@@ -1191,9 +1243,9 @@ S3IsSuspS2 = univalence (IsoToEquiv iso) where
   suspSurf i j k = hfill {Susp S2} (\l [ (i = i0) -> north
                                        , (i = i1) -> merid base2 (inot l)
                                        , (j = i0) -> merid base2 (iand (inot l) i)
-                                       , (j = i1) -> merid base2 (iand (inot l) i)
+                                       , (j = i1) -> merid {S2} base2 (iand (inot l) i)
                                        , (k = i0) -> merid base2 (iand (inot l) i)
-                                       , (k = i1) -> merid base2 (iand (inot l) i)
+                                       , (k = i1) -> merid {S2} base2 (iand (inot l) i)
                                        ])
                                    (inS (merid (surf2 j k) i))
 
@@ -1429,11 +1481,8 @@ Sq_equiv_to_isProp eqv = transp (\i -> isProp (univalence eqv (inot i))) (\x y i
 exercise_3_21 : {P : Type} -> Equiv (isProp P) (Equiv P (Sq P))
 exercise_3_21 {P} = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp
 
-uaBeta : {A : Type} {B : Type} (e : Equiv A B) -> Path (idToEquiv (univalence e)).1 e.1
-uaBeta {A} {B} e i a = univalenceBeta e i a
-
 uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (univalence {A} {B}) (idToEquiv {A} {B})
-uaret eqv = equivLemma (uaBeta eqv)
+uaret eqv = equivLemma (univalenceBeta eqv)
 
 f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B
 f1 {A} p = (p.1, univalence p.2)
@@ -1452,4 +1501,153 @@ retContr {A} {B} f g h v = (g b, p) where
   b = v.1
 
   p : (x : A) -> Path (g b) x
-  p x i = comp (\i -> A) (\j [ (i = i0) -> g b, (i = i1) -> h x j ]) (inS (g (v.2 (f x) i)))
\ No newline at end of file
+  p x i = comp (\i -> A) (\j [ (i = i0) -> g b, (i = i1) -> h x j ]) (inS (g (v.2 (f x) i)))
+
+curry : {A : Type} {B : A -> Type} {C : (x : A) -> B x -> Type}
+     -> Path ((x : A) (y : B x) -> C x y) ((p : (x : A) * B x) -> C p.1 p.2)
+curry {A} {B} {C} = IsoToId (to, from, \f -> refl, \g -> refl) where
+  to : ((x : A) (y : B x) -> C x y) -> (p : (x : A) * B x) -> C p.1 p.2
+  to f p = f p.1 p.2
+
+  from : ((p : (x : A) * B x) -> C p.1 p.2) -> (x : A) (y : B x) -> C x y
+  from f x y = f (x, y)
+
+ft2 : {A : Type} -> Path (T2 -> A) (S1 -> S1 -> A)
+ft2 {A} = transp (\i -> Path (T2 -> A) (curry {S1} {\x -> S1} {\x y -> A} (inot i))) p where
+  p : Path (T2 -> A) ((S1 * S1) -> A)
+  p i = TorusIsTwoCircles i -> A
+
+data coeq {A : Type} {B : Type} (f : B -> A) (g : B -> A) : Type where
+  c   : A -> coeq {A} {B} f g
+  p i : (b : B) -> coeq {A} {B} f g [ (i = i0) -> c (f b), (i = i1) -> c (g b) ]
+
+coeq_S1 : Type
+coeq_S1 = coeq {Unit} {Unit} id id
+
+coeq_base : coeq_S1
+coeq_base = c tt
+
+coeq_loop : Path coeq_base coeq_base
+coeq_loop i = p tt i
+
+coeq_S1_elim : (P : coeq_S1 -> Type) (base : P coeq_base)
+            -> PathP (\i -> P (coeq_loop i)) base base
+            -> (x : coeq_S1)
+            -> P x
+coeq_S1_elim P base loop =
+  \case
+    c x -> baseCase x
+    p x i -> loopCase x i
+  where
+    baseCase : (x : Unit) -> P (c x)
+    baseCase = \case
+      tt -> base
+
+    loopCase : (x : Unit) -> PathP (\i -> P (p x i)) (baseCase x) (baseCase x)
+    loopCase = \case
+      tt -> loop
+
+ContractibleIfInhabited : {A : Type} -> Path (A -> isContr A) (isProp A)
+ContractibleIfInhabited {A} = IsoToId (to, from, toFrom, fromTo) where
+  to : (A -> isContr A) -> isProp A
+  to cont x y = trans (sym (p.2 x)) (p.2 y) where
+    p = cont x
+
+  from : isProp A -> A -> isContr A
+  from prop x = (x, prop x)
+
+  toFrom : (y : isProp A) -> Path (to (from y)) y
+  toFrom y = isProp_isProp {A} (to (from y)) y
+
+  fromTo : (y : A -> isContr A) -> Path (from (to y)) y
+  fromTo y i a = isProp_isContr {A} (from (to y) a) (y a) i
+
+data cone (A : Type) : Type where
+  point  : cone A
+  base   : A -> cone A
+  side i : (x : A) -> cone A [ (i = i0) -> point, (i = i1) -> base x ]
+
+ConeA_contr : {A : Type} -> isContr (cone A)
+ConeA_contr {A} = (point, contr) where
+  contr : (y : cone A) -> Path point y
+  contr = \case
+    point  -> refl
+    base x -> \i -> side x i
+    side x i -> \j -> side x (iand i j)
+
+contrSinglEquiv : {B : Type} -> isContr ((A : Type) * Equiv A B)
+contrSinglEquiv {B} = (center, contract) where
+  center : (A : Type) * Equiv A B
+  center = (B, the B, idEquiv {B})
+
+  contract : (p : (A : Type) * Equiv A B) -> Path center p
+  contract w i =
+    let
+      sys : Partial (ior (inot i) i) ((A : Type) * Equiv A B)
+      sys = \ [ (i = i0) -> center, (i = i1) -> w ]
+
+      GlueB = Glue B sys
+
+      unglueB : GlueB -> B
+      unglueB x = unglue {B} (ior (inot i) i) {sys} x 
+
+      unglueEquiv : isEquiv {GlueB} {B} unglueB
+      unglueEquiv b =
+        let
+          ctr : fiber unglueB b
+          ctr = ( glue {B} {ior (inot i) i} {sys} (\[ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.1 ])
+                    (primComp (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))
+                , fill (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))
+
+          contr : (v : fiber unglueB b) -> Path ctr v
+          contr v j = ( glue {B} {ior (inot i) i} {sys}
+                          (\[ (i = i0) -> v.2 j, (i = i1) -> ((w.2.2 b).2 v j).1 ])
+                          (inS (comp (\i -> B)
+                                  (\k [ (i = i0) -> v.2 (iand j k)
+                                      , (i = i1) -> ((w.2.2 b).2 v j).2 k
+                                      , (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k
+                                      , (j = i1) -> v.2 k
+                                      ])
+                                  (inS b)))
+                      , fill (\j -> B) (\k [ (i = i0) -> v.2 (iand j k)
+                                           , (i = i1) -> ((w.2.2 b).2 v j).2 k
+                                           , (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k
+                                           , (j = i1) -> v.2 k
+                                           ])
+                                       (inS b)
+                      )
+        in (ctr, contr)
+    in (GlueB, unglueB, unglueEquiv)
+
+uaIdEquiv : {A : Type} -> Path (univalence (the A, idEquiv {A})) (\i -> A)
+uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, the A, idEquiv {A}))
+
+EquivJ : {X : Type}
+         (P : (Y : Type) -> Equiv Y X -> Type)
+         (d : P X (the X, idEquiv {X}))
+         {Y : Type} (E : Equiv Y X)
+      -> P Y E
+EquivJ {X} P d {Y} e = subst {(Y : Type) * Equiv Y X} (\x -> P x.1 x.2) path d where
+  path : Path {(Y : Type) * Equiv Y X} (X, the X, idEquiv {X}) (Y, e)
+  path = isContr_isProp {(Y : Type) * Equiv Y X} contrSinglEquiv (X, the X, idEquiv {X}) (Y, e)
+
+uaIso : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B)
+uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where
+  pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
+  pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A})
+
+  pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) (the A, idEquiv {A})
+  pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A})
+
+  univalence_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (univalence (pathToEquiv p)) p
+  univalence_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (univalence {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where
+    lemma : Path (univalence (pathToEquiv (\i -> A))) (\i -> A)
+    lemma = transp (\i -> Path (univalence (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv
+
+  pathToEquiv_univalence : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (univalence p)) p
+  pathToEquiv_univalence {A} {B} p = EquivJ {B} (\A e -> Path (pathToEquiv (univalence e)) e) lemma p where
+    lemma : Path (pathToEquiv (univalence (the B, idEquiv {B}))) (the B, idEquiv {B})
+    lemma = transp (\i -> Path (pathToEquiv (uaIdEquiv {B} (inot i))) (the B, idEquiv {B})) pathToEquiv_refl
+
+uaEquiv : {A : Type} {B : Type} -> isEquiv (pathToEquiv {A} {B})
+uaEquiv {A} {B} = (IsoToEquiv (uaIso {A} {B})).2
\ No newline at end of file
diff --git a/src/Elab.hs b/src/Elab.hs
index 2f35a8f..e9f0277 100644
--- a/src/Elab.hs
+++ b/src/Elab.hs
@@ -145,7 +145,7 @@ check (P.Let items body) ty = do
 
 check (P.LamSystem bs) ty = do
   (extent, dom) <- isPartialType ty
-  let dom_q = quote dom
+  let dom_q x = quote (dom x)
   eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
     phi <- checkFormula (P.condF formula)
     rhses <-
@@ -155,13 +155,14 @@ check (P.LamSystem bs) ty = do
           for (truthAssignments phi (getEnv env)) $ \e -> do
             let env' = env{ getEnv = e }
             local (const env') $
-              (Just var,) <$> check rhs (eval' env' dom_q)
+              (Just var,) <$> check rhs (eval' env' (dom_q (VVar var)))
         Nothing -> do
           env <- ask
+          n <- newName
           for (truthAssignments phi (getEnv env)) $ \e -> do
             let env' = env{ getEnv = e }
             local (const env') $
-              (Nothing,) <$> check rhs (eval' env' dom_q)
+              (Nothing,) <$> check rhs (eval' env' (dom_q (VVar n)))
     pure (n, (phi, head rhses))
 
   unify extent (foldl ior VI0 (map (fst . snd) eqns))
@@ -267,7 +268,7 @@ check (P.LamCase pats) ty =
     boundaryFormulas a b = error (show (a, b))
 
 check P.Hole ty = do
-  t <- newMeta ty
+  t <- newMeta' True ty
   pure (quote t)
 
 check exp ty = do
@@ -439,15 +440,15 @@ isSigmaType t = isSigmaType (force t) where
       wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
       pure (dom, const rng, wp)
 
-isPartialType :: NFType -> ElabM (NFEndp, Value)
+isPartialType :: NFType -> ElabM (NFEndp, Value -> Value)
 isPartialType t = isPartialType (force t) where
-  isPartialType (VPartial phi a) = pure (phi, a)
-  isPartialType (VPartialP phi a) = pure (phi, a)
+  isPartialType (VPartial phi a) = pure (phi, const a)
+  isPartialType (VPartialP phi a) = pure (phi, (a @@))
   isPartialType t = do
     phi <- newMeta VI
     dom <- newMeta (VPartial phi VType)
-    unify t (VPartial phi dom)
-    pure (phi, dom)
+    unify t (VPartialP phi dom)
+    pure (phi, (dom @@))
 
 checkStatement :: P.Statement -> ElabM a -> ElabM a
 checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
@@ -517,10 +518,10 @@ checkStatement (P.ReplTy e) k = do
 
 checkStatement (P.Data name tele retk constrs) k =
   do
-    checkTeleRetk True tele retk \kind tele undef -> do
+    checkTeleRetk tele retk \retk kind tele undef -> do
       kind_nf <- eval kind
-      defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' ->
-        checkCons tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
+      defineInternal (Defined name 0) kind_nf (\name' -> GluedVl (mkHead name') mempty (VNe (mkHead name') mempty)) \name' ->
+        checkCons retk tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
   where
     makeProj (x, p, _) = PApp p (VVar x)
 
@@ -530,26 +531,22 @@ checkStatement (P.Data name tele retk constrs) k =
       | any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name
       | otherwise = HData False name
 
-    checkTeleRetk allKan [] retk cont = do
+    checkTeleRetk [] retk cont = do
       t <- check retk VTypeω
-      t_nf <- eval t
-      when allKan $ unify t_nf VType
-      cont t [] id
-    checkTeleRetk allKan ((x, p, t):xs) retk cont = do
+      r <- eval t
+      cont r t [] id
+
+    checkTeleRetk ((x, p, t):xs) retk cont = do
       (t, ty) <- infer t
       _ <- isConvertibleTo ty VTypeω
-      let
-        allKan' = case ty of
-          VType -> allKan
-          _ -> False
       t_nf <- eval t
       let rm nm e = e{ nameMap = Map.delete (getNameText nm) (nameMap e), getEnv = Map.delete nm (getEnv e) }
-      assume (Bound x 0) t_nf $ \nm -> checkTeleRetk allKan' xs retk \k xs w -> cont (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
+      assume (Bound x 0) t_nf $ \nm -> checkTeleRetk xs retk \ret k xs w -> cont ret (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
 
-    checkCons _ _et [] k = k
+    checkCons _ _ _et [] k = k
 
-    checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
-      t <- check ty VTypeω
+    checkCons retk n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
+      t <- check ty retk
       ty_nf <- eval t
       let
         (args, ret') = splitPi ty_nf
@@ -557,11 +554,12 @@ checkStatement (P.Data name tele retk constrs) k =
         n' = map (\(x, _, y) -> (x, P.Im, y)) n
       unify ret' ret
       closed_nf <- eval closed
-      defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k
+      defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons retk n ret xs k
 
-    checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
+    checkCons retk n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
+      fibrant retk
       (con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
-        t <- check return VTypeω
+        t <- check return retk
         ty_nf <- eval t
         let
           (args, ret') = splitPi ty_nf
@@ -588,7 +586,7 @@ checkStatement (P.Data name tele retk constrs) k =
           `withNote` pretty "The formula determining the endpoints of a higher constructor must be a classical tautology"
 
         pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system)
-      defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k
+      defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons retk n ret xs k
 
     close []             t = t
     close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
@@ -608,6 +606,10 @@ checkStatement (P.Data name tele retk constrs) k =
     totalProp (x:xs) = ior (VVar x) (inot (VVar x) `ior` totalProp xs)
     totalProp [] = VI0
 
+    fibrant VTypeω = throwElab PathConPretype
+    fibrant VType = pure ()
+    fibrant x = error $ "not a constructor kind: " ++ show x
+
 
 checkProgram :: [P.Statement] -> ElabM a -> ElabM a
 checkProgram [] k = k
@@ -627,5 +629,9 @@ data NotACon = NotACon { theNotConstr :: Name }
   deriving          (Show, Typeable)
   deriving anyclass (Exception)
 
+data PathConPretype = PathConPretype
+  deriving          (Show, Typeable)
+  deriving anyclass (Exception)
+
 newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
   deriving (Eq, Show, Exception)
diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs
index 6638511..9666b2f 100644
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@@ -23,15 +23,13 @@ import Data.Foldable
 import Data.IORef
 import Data.Maybe
 
-import Elab.Eval.Formula
+import {-# SOURCE #-} Elab.Eval.Formula
 import Elab.Monad
 
 import GHC.Stack
 
 import Presyntax.Presyntax (Plicity(..))
 
-import Prettyprinter
-
 import Syntax.Pretty
 import Syntax
 
@@ -42,7 +40,6 @@ import {-# SOURCE #-} Elab.WiredIn
 eval :: HasCallStack => Term -> ElabM Value
 eval t = asks (flip eval' t)
 
--- everywhere force
 zonkIO :: Value -> IO Value
 zonkIO (VNe hd sp) = do
   sp' <- traverse zonkSp sp
@@ -64,7 +61,6 @@ zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b
 zonkIO (VPath line x y) = VPath <$> zonkIO line <*> zonkIO x <*> zonkIO y
 zonkIO (VLine line x y f) = VLine <$> zonkIO line <*> zonkIO x <*> zonkIO y <*> zonkIO f
 
--- Sorts
 zonkIO VType = pure VType
 zonkIO VTypeω = pure VTypeω
 
@@ -127,17 +123,17 @@ eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
 
 eval' env (Lam p s t) =
   VLam p $ Closure s $ \a ->
-    eval' env { getEnv = Map.insert s (error ("type of abs " ++ show (pretty (Lam p s t))), a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
 
 eval' env (Pi p s d t) =
   VPi p (eval' env d) $ Closure s $ \a ->
-    eval' env { getEnv = (Map.insert s (error "type of abs", a) (getEnv env))} t
+    eval' env { getEnv = (Map.insert s (idkT, a) (getEnv env))} t
 
 eval' _ (Meta m) = VNe (HMeta m) mempty
 
 eval' env (Sigma s d t) =
   VSigma (eval' env d) $ Closure s $ \a ->
-    eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
 
 eval' e (Pair a b) = VPair (eval' e a) (eval' e b)
 
@@ -187,6 +183,13 @@ eval' e (Syntax.Refl a x) = VReflStrict (eval' e a) (eval' e x)
 eval' e (Syntax.AxK a x p pr eq) = strictK (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e eq)
 eval' e (Syntax.AxJ a x p pr y eq) = strictJ (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e y) (eval' e eq)
 
+idkT :: NFType
+idkT = VVar (Defined (T.pack "dunno") (negate 1))
+
+isIdkT :: NFType -> Bool
+isIdkT (VVar (Defined (T.unpack -> "dunno") (negate -> 1))) = True
+isIdkT _ = False
+
 evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Int, Term)] -> Value
 evalCase env rng sc [] = VCase (getEnv env) (fun rng) sc []
 
@@ -214,7 +217,7 @@ evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
 evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs
 
 evalFix' :: HasCallStack => ElabEnv -> Name -> NFType -> Term -> Value
-evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term
+evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, GluedVl (HVar name) mempty val) (getEnv env) } term
 
 evalFix :: HasCallStack => Name -> NFType -> Term -> ElabM Value
 evalFix name nft term = do
@@ -225,6 +228,10 @@ data NotEqual = NotEqual Value Value
   deriving (Show, Typeable, Exception)
 
 unify' :: HasCallStack => Value -> Value -> ElabM ()
+unify' (GluedVl h sp a) (GluedVl h' sp' b)
+  | h == h', length sp == length sp' =
+    traverse_ (uncurry unify'Spine) (Seq.zip sp sp')
+      `catchElab` \(_ :: SomeException) -> unify' a b
 unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs
   go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs
@@ -234,10 +241,10 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VNe (HPCon s _ _) _) rhs | Just v <- trivialSystem s = go v rhs
   go lhs (VNe (HPCon s _ _) _) | Just v <- trivialSystem s = go lhs v
 
-  go (VCase e _ a b) (VCase e' _ a' b') = do
+  go (VCase e _ _ b) (VCase e' _ _ b') = do
     env <- ask
-    unify' a a'
-    let go (_, _, a) (_, _, b) = unify' (eval' env{getEnv=e} a) (eval' env{getEnv=e'} b)
+    let
+      go (_, _, a) (_, _, b) = unify' (eval' env{getEnv=moreDefinedFrom e e' <$> e} a) (eval' env{getEnv=moreDefinedFrom e e' <$> e'} b)
     zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b')
 
   go (VCase e _ _ b) y = do
@@ -264,13 +271,13 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VPair a b) vl = unify' a (vProj1 vl) *> unify' b (vProj2 vl)
   go vl (VPair a b) = unify' (vProj1 vl) a *> unify' (vProj2 vl) b
 
-  go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do
-    t <- VVar <$> newName
+  go (VPi p d (Closure n k)) (VPi p' d' (Closure _ k')) | p == p' = do
+    t <- VVar <$> newName' n
     unify' d d'
     unify' (k t) (k' t)
 
-  go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do
-    t <- VVar <$> newName
+  go (VSigma d (Closure n k)) (VSigma d' (Closure _ k')) = do
+    t <- VVar <$> newName' n
     unify' d d'
     unify' (k t) (k' t)
 
@@ -285,7 +292,7 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     unify' y y'
 
   go (VLine l x y p) p' = do
-    n <- VVar <$> newName
+    n <- VVar <$> newName' (Bound (T.singleton 'i') (- 1))
     unify' (p @@ n) (ielim l x y p' n)
 
   go p' (VLine l x y p) = do
@@ -301,6 +308,9 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VComp a phi u a0) (VComp a' phi' u' a0') =
     traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
 
+  go (VHComp a phi u a0) (VHComp a' phi' u' a0') =
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+
   go (VGlueTy _ (force -> VI1) u _0) rhs = unify' (u @@ VReflStrict VI VI1) rhs
   go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VReflStrict VI VI1)
 
@@ -343,6 +353,19 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     | compareDNFs x y = pure ()
     | otherwise = fail
 
+moreDefinedFrom :: Map Name (NFType, Value) -> Map Name (NFType, Value) -> (NFType, Value) -> (NFType, Value)
+moreDefinedFrom map1 map2 ours@(_, VNe (HVar name) _) =
+  case Map.lookup name map1 of
+    Just (_, VNe HVar{} _) -> map2's
+    Just (ty, x) -> (ty, x)
+    Nothing -> map2's
+  where
+    map2's = case Map.lookup name map2 of
+      Just (_, VNe HVar{} _) -> ours
+      Just (ty, x) -> (ty, x)
+      Nothing -> ours
+moreDefinedFrom _ _ ours = ours
+
 trivialSystem :: Value -> Maybe Value
 trivialSystem = go . force where
   go VSystem{} = Nothing
@@ -400,25 +423,32 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where
     unify' a b
     pure id
 
-newMeta :: Value -> ElabM Value
-newMeta dom = do
+newMeta' :: Bool -> Value -> ElabM Value
+newMeta' int dom = do
   loc <- liftM2 (,) <$> asks currentFile <*> asks currentSpan
   n <- newName
   c <- liftIO $ newIORef Nothing
-  let m = MV (getNameText n) c dom (flatten <$> loc)
+  let m = MV (getNameText n) c dom (flatten <$> loc) int
       flatten (x, (y, z)) = (x, y, z)
 
   env <- asks getEnv
 
-  t <- for (Map.toList env) $ \(n, _) -> pure $
+  t <- fmap catMaybes . for (Map.toList env) $ \(n, t) -> pure $
     case n of
-      Bound{} -> Just (PApp Ex (VVar n))
+      Bound{} -> Just (PApp Ex (VVar n), n, t)
       _ -> Nothing
 
+  let
+    ts = Map.fromList $ fmap (\(_, n, (t, _)) -> (n, t)) t
+    t' = fmap (\(x, _, _) -> x) t
+
   um <- asks unsolvedMetas
-  liftIO . atomicModifyIORef um $ \um -> (Map.insert m [] um, ())
+  liftIO . atomicModifyIORef um $ \um -> (Map.insert (m ts) [] um, ())
 
-  pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
+  pure (VNe (HMeta (m ts)) (Seq.fromList t'))
+
+newMeta :: Value -> ElabM Value
+newMeta = newMeta' False
 
 newName :: MonadIO m => m Name
 newName = liftIO $ do
@@ -435,27 +465,32 @@ _nameCounter = unsafePerformIO $ newIORef 0
 {-# NOINLINE _nameCounter #-}
 
 solveMeta :: MV -> Seq Projection -> Value -> ElabM ()
+solveMeta m Seq.Empty (VNe (HMeta m') Seq.Empty) | m == m' = pure ()
 solveMeta m@(mvCell -> cell) sp rhs = do
   env <- ask
   names <- tryElab $ checkSpine Set.empty sp
   case names of
     Right names -> do
-      checkScope (Set.fromList names) rhs
-        `withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)]
-      let tm = quote rhs
-          lam = eval' env $ foldr (Lam Ex) tm names
-      liftIO . atomicModifyIORef (unsolvedMetas env) $ \mp -> (Map.delete m mp, ())
-      liftIO . atomicModifyIORef' cell $ \case
-        Just _ -> error "filled cell in solvedMeta"
-        Nothing -> (Just lam, ())
-    Left (_ :: SpineProjection) -> do
+      scope <- tryElab $ checkScope m (Set.fromList names) rhs
+      case scope of
+        Right () -> do
+          let tm = quote rhs
+              lam = eval' env $ foldr (Lam Ex) tm names
+          liftIO . atomicModifyIORef (unsolvedMetas env) $ \mp -> (Map.delete m mp, ())
+          liftIO . atomicModifyIORef' cell $ \case
+            Just _ -> error "filled cell in solvedMeta"
+            Nothing -> (Just lam, ())
+        Left (_ :: MetaException) -> abort env
+    Left (_ :: MetaException) -> abort env
+  where
+    abort env =
       liftIO . atomicModifyIORef' (unsolvedMetas env) $ \x -> (, ()) $
         case Map.lookup m x of
           Just qs -> Map.insert m ((sp, rhs):qs) x
           Nothing -> Map.insert m [(sp, rhs)] x
 
-checkScope :: Set Name -> Value -> ElabM ()
-checkScope scope (VNe h sp) =
+checkScope :: MV -> Set Name -> Value -> ElabM ()
+checkScope mv scope (VNe h sp) =
   do
     case h of
       HVar v@Bound{} ->
@@ -464,65 +499,65 @@ checkScope scope (VNe h sp) =
       HVar{} -> pure ()
       HCon{} -> pure ()
       HPCon{} -> pure ()
-      HMeta{} -> pure ()
+      HMeta m' -> when (mv == m') $ throwElab $ CircularSolution mv
       HData{} -> pure ()
     traverse_ checkProj sp
   where
-    checkProj (PApp _ t) = checkScope scope t
-    checkProj (PIElim l x y i) = traverse_ (checkScope scope) [l, x, y, i]
-    checkProj (PK l x y i) = traverse_ (checkScope scope) [l, x, y, i]
-    checkProj (PJ l x y i j) = traverse_ (checkScope scope) [l, x, y, i, j]
-    checkProj (POuc a phi u) = traverse_ (checkScope scope) [a, phi, u]
+    checkProj (PApp _ t) = checkScope mv scope t
+    checkProj (PIElim l x y i) = traverse_ (checkScope mv scope) [l, x, y, i]
+    checkProj (PK l x y i) = traverse_ (checkScope mv scope) [l, x, y, i]
+    checkProj (PJ l x y i j) = traverse_ (checkScope mv scope) [l, x, y, i, j]
+    checkProj (POuc a phi u) = traverse_ (checkScope mv scope) [a, phi, u]
     checkProj PProj1 = pure ()
     checkProj PProj2 = pure ()
 
-checkScope scope (GluedVl _ _p vl) = checkScope scope vl
+checkScope mv scope (GluedVl _ _p vl) = checkScope mv scope vl
 
-checkScope scope (VLam _ (Closure n k)) =
-  checkScope (Set.insert n scope) (k (VVar n))
+checkScope mv scope (VLam _ (Closure n k)) =
+  checkScope mv (Set.insert n scope) (k (VVar n))
 
-checkScope scope (VPi _ d (Closure n k)) = do
-  checkScope scope d
-  checkScope (Set.insert n scope) (k (VVar n))
+checkScope mv scope (VPi _ d (Closure n k)) = do
+  checkScope mv scope d
+  checkScope mv (Set.insert n scope) (k (VVar n))
 
-checkScope scope (VSigma d (Closure n k)) = do
-  checkScope scope d
-  checkScope (Set.insert n scope) (k (VVar n))
+checkScope mv scope (VSigma d (Closure n k)) = do
+  checkScope mv scope d
+  checkScope mv (Set.insert n scope) (k (VVar n))
 
-checkScope s (VPair a b) = traverse_ (checkScope s) [a, b]
+checkScope mv s (VPair a b) = traverse_ (checkScope mv s) [a, b]
 
-checkScope _ VType = pure ()
-checkScope _ VTypeω = pure ()
+checkScope _ _ VType = pure ()
+checkScope _ _ VTypeω = pure ()
 
-checkScope _ VI = pure ()
-checkScope _ VI0 = pure ()
-checkScope _ VI1 = pure ()
+checkScope _ _ VI = pure ()
+checkScope _ _ VI0 = pure ()
+checkScope _ _ VI1 = pure ()
 
-checkScope s (VIAnd x y) = traverse_ (checkScope s) [x, y]
-checkScope s (VIOr x y)  = traverse_ (checkScope s) [x, y]
-checkScope s (VINot x)   = checkScope s x
+checkScope mv s (VIAnd x y) = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VIOr x y)  = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VINot x)   = checkScope mv s x
 
-checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
-checkScope s (VLine _ _ _ line)   = checkScope s line
+checkScope mv s (VPath line a b) = traverse_ (checkScope mv s) [line, a, b]
+checkScope mv s (VLine _ _ _ line)   = checkScope mv s line
 
-checkScope s (VPartial x y)  = traverse_ (checkScope s) [x, y]
-checkScope s (VPartialP x y) = traverse_ (checkScope s) [x, y]
-checkScope s (VSystem fs) =
-  for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope s) [x, y]
+checkScope mv s (VPartial x y)  = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VPartialP x y) = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VSystem fs) =
+  for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope mv s) [x, y]
 
-checkScope s (VSub a b c) = traverse_ (checkScope s) [a, b, c]
-checkScope s (VInc a b c) = traverse_ (checkScope s) [a, b, c]
-checkScope s (VComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
-checkScope s (VHComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
+checkScope mv s (VSub a b c) = traverse_ (checkScope mv s) [a, b, c]
+checkScope mv s (VInc a b c) = traverse_ (checkScope mv s) [a, b, c]
+checkScope mv s (VComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0]
+checkScope mv s (VHComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0]
 
-checkScope s (VGlueTy a phi ty eq) = traverse_ (checkScope s) [a, phi, ty, eq]
-checkScope s (VGlue a phi ty eq inv x) = traverse_ (checkScope s) [a, phi, ty, eq, inv, x]
-checkScope s (VUnglue a phi ty eq vl) = traverse_ (checkScope s) [a, phi, ty, eq, vl]
+checkScope mv s (VGlueTy a phi ty eq) = traverse_ (checkScope mv s) [a, phi, ty, eq]
+checkScope mv s (VGlue a phi ty eq inv x) = traverse_ (checkScope mv s) [a, phi, ty, eq, inv, x]
+checkScope mv s (VUnglue a phi ty eq vl) = traverse_ (checkScope mv s) [a, phi, ty, eq, vl]
 
-checkScope s (VCase _ _ v _) = checkScope s v
+checkScope mv s (VCase _ _ v _) = checkScope mv s v
 
-checkScope s (VEqStrict a x y) = traverse_ (checkScope s) [a, x, y]
-checkScope s (VReflStrict a x) = traverse_ (checkScope s) [a, x]
+checkScope mv s (VEqStrict a x y) = traverse_ (checkScope mv s) [a, x, y]
+checkScope mv s (VReflStrict a x) = traverse_ (checkScope mv s) [a, x]
 
 checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
 checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
@@ -531,10 +566,7 @@ checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
 checkSpine _     (p Seq.:<| _) = throwElab $ SpineProj p
 checkSpine _     Seq.Empty = pure []
 
-newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
-  deriving (Show, Typeable, Exception)
-
-newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
+data MetaException = NonLinearSpine { getDupeName :: Name } | SpineProj { getSpineProjection :: Projection } | CircularSolution { getCycle :: MV }
   deriving (Show, Typeable, Exception)
 
 substituteIO :: Map.Map Name Value -> Value -> IO Value
@@ -563,7 +595,6 @@ substituteIO sub = substituteIO . force where
   substituteIO (VPath line x y) = VPath <$> substituteIO line <*> substituteIO x <*> substituteIO y
   substituteIO (VLine line x y f) = VLine <$> substituteIO line <*> substituteIO x <*> substituteIO y <*> substituteIO f
 
-  -- Sorts
   substituteIO VType = pure VType
   substituteIO VTypeω = pure VTypeω
 
@@ -655,6 +686,7 @@ vApp p (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs)
 vApp p (VCase env rng sc branches) arg =
   VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
     (map (projIntoCase (flip (App p) (quote arg))) branches)
+-- vApp _ (VLine _ _ _ (VLam _ k)) arg = clCont k arg
 vApp _ x _             = error $ "can't apply " ++ show (prettyTm (quote x))
 
 (@@) :: HasCallStack => Value -> Value -> Value
diff --git a/src/Elab/Eval/Formula.hs b/src/Elab/Eval/Formula.hs
index ae313e8..e50c69e 100644
--- a/src/Elab/Eval/Formula.hs
+++ b/src/Elab/Eval/Formula.hs
@@ -9,6 +9,7 @@ import Data.Set (Set)
 import Syntax
 
 import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
+import Elab.Eval (substitute)
 
 toDnf :: Value -> Maybe Value
 toDnf = fmap (dnf2Val . normalise) . val2Dnf where
@@ -75,10 +76,13 @@ truthAssignments VI0 _ = []
 truthAssignments VI1 m = pure m
 truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m
 truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m
-truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) m)
+truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) (sub x VI1 <$> m))
 truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) m)
 truthAssignments _ m = pure m
 
+sub :: Name -> Value -> (NFType, NFEndp) -> (Value, Value)
+sub x v (a, b) = (substitute (Map.singleton x v) a, substitute (Map.singleton x v) b)
+
 idist :: Value -> Value -> Value
 idist (VIOr x y) z = (x `idist` z) `ior` (y `idist` z)
 idist z (VIOr x y) = (z `idist` x) `ior` (z `idist` y)
diff --git a/src/Elab/Eval/Formula.hs-boot b/src/Elab/Eval/Formula.hs-boot
new file mode 100644
index 0000000..6656f71
--- /dev/null
+++ b/src/Elab/Eval/Formula.hs-boot
@@ -0,0 +1,18 @@
+module Elab.Eval.Formula where
+
+import Syntax
+import Data.Map.Strict (Map)
+import Data.Set (Set)
+
+toDnf :: Value -> Maybe Value
+
+type Nf = Set (Set Value)
+
+normalise :: Value -> Nf
+compareDNFs :: Value -> Value -> Bool
+
+swap :: Ord b => b -> b -> (b, b)
+
+possible :: Map Head Bool -> Value -> (Bool, Map Head Bool)
+
+truthAssignments :: NFEndp -> Map Name (NFType, NFEndp) -> [Map Name (NFType, NFEndp)]
\ No newline at end of file
diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs
index 110f517..51bef9e 100644
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@@ -9,7 +9,7 @@
 {-# LANGUAGE KindSignatures #-}
 module Elab.WiredIn where
 
-import Control.Exception
+import Control.Exception ( assert, Exception )
 
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
@@ -31,6 +31,7 @@ import Syntax.Pretty (prettyTm, prettyVl)
 import Syntax
 
 import System.IO.Unsafe
+import Data.Text.Prettyprint.Doc (viaShow)
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -54,12 +55,9 @@ wiType WiOutS     = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a)
 
 wiType WiComp     = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> VSub (a @@ VI1) phi (u @@ VI1)
 
--- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
 wiType WiGlue     = dprod' "A" VType \a -> forAll' "phi" VI \phi -> dprod' "T" (VPartial phi VType) \t -> VPartialP phi (fun \o -> equiv (t @@ o) a) ~> VType
--- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
 wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \eqv ->
   dprod' "t" (VPartialP phi ty) \t -> VSub a phi (fun \o -> vProj1 (eqv @@ o) @@ (t @@ o)) ~> VGlueTy a phi ty eqv
--- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
 wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a
 
 wiType WiSEq   = forAll' "A" VTypeω \a -> a ~> a ~> VTypeω
@@ -176,8 +174,6 @@ newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
   deriving (Show, Typeable)
   deriving anyclass (Exception)
 
--- Interval operations
-
 iand, ior :: Value -> Value -> Value
 iand x = case force x of
   VI1 -> id
@@ -227,7 +223,7 @@ ielim line left right fn i =
         VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
         VInc (VPath _ _ _) _ u -> ielim line left right u i
 
-        VCase env r x xs -> VCase env r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
+        VCase env r x xs -> VCase env r x (fmap (projIntoCase (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
 
         _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
 
@@ -247,7 +243,6 @@ outS a phi u (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
 outS a phi u (VSystem fs) = mkVSystem (fmap (outS a phi u) fs)
 outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 
--- Composition
 comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
 comp _a VI1 u _a0 =  u @@ VI1 @@ VReflStrict VI VI1
 comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
@@ -302,7 +297,7 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
         types i  = substitute (Map.singleton name i) theTypes @@ VReflStrict VI VI1
         equivs i = substitute (Map.singleton name i) theEquivs
 
-        a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u)
+        a i u = unglue (base i) (phi i) (types i) (equivs i) (b @@ i @@ u)
         a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
 
         del = faceForall phi
@@ -440,6 +435,7 @@ glueType a phi tys eqvs = VGlueTy a phi tys eqvs
 
 glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
 glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VReflStrict VI VI1
+glueElem _a _phi _tys _eqvs _t (force -> VInc _ _ (force -> VUnglue _ _ _ _ vl)) = vl
 glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
 
 unglue   :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
@@ -447,7 +443,6 @@ unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VReflStrict VI VI1) @@ x
 unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ t vl) = outS _a _phi (t @@ VReflStrict VI VI1) vl
 unglue a phi tys eqvs (force -> VSystem fs) = VSystem (fmap (unglue a phi tys eqvs) fs)
 unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl
--- Definition of equivalences
 
 faceForall :: (NFEndp -> NFEndp) -> Value
 faceForall phi = T.length (getNameText name) `seq` go (phi (VVar name)) where
@@ -518,7 +513,7 @@ transHit name line phi x = transHit name line phi (force x) where
   transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi (outS (line VI0) phi u u0))
   transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
     x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
-    (_, VNe hd (length -> nargs)) = unPi con_type
+    (_, force -> VNe hd (length -> nargs)) = unPi con_type
     ourType = case hd of
       HData True n' -> n' == name
       _ -> False
@@ -526,7 +521,7 @@ transHit name line phi x = transHit name line phi (force x) where
   transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
     x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
     rec = transHit name line phi
-    (_, VNe hd (length -> nargs)) = unPi con_type
+    (_, force -> VNe hd (length -> nargs)) = unPi con_type
     ourType = case hd of
       HData True n' -> n' == name
       _ -> False
@@ -614,4 +609,4 @@ projIntoCase fun (pat, nLams, term) = (pat, nLams, go nLams term) where
   go 0 x = fun x
   go n (Lam p x r) = Lam p x (go (n - 1) r)
   go n (PathIntro l a b r) = PathIntro l a b (go (n - 1) r)
-  go _ x = x
+  go _ x = error $ show $ prettyTm x
diff --git a/src/Main.hs b/src/Main.hs
index c9bf2c2..5bf505f 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -108,6 +108,11 @@ enterReplIn env =
                   `catch` \e -> do
                     displayExceptions' inp (e :: SomeException)
                     pure env
+
+              metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
+              unless (Map.null metas) $ do
+                liftIO $ reportUnsolved (Just inp) metas
+
               liftIO $ writeIORef envvar env
               loop env envvar
 
@@ -142,9 +147,9 @@ checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
            in withSpan (fst pos) (snd pos) $ throwElab $ Elab.DeclaredUndefined v
       _ -> pure ()
 
-    metas <- liftIO $ readIORef (unsolvedMetas env)
+    metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
     unless (Map.null metas) $ do
-      liftIO $ reportUnsolved metas
+      liftIO $ reportUnsolved Nothing metas
     k
 
   go n (x:xs) k = do
@@ -230,6 +235,8 @@ displayExceptions lines =
       putStrLn $ "Variable not in scope: " ++ show (pretty x)
   , Handler \(Elab.DeclaredUndefined n) -> do
       putStrLn $ "Name declared but not defined: " ++ show (pretty n)
+  , Handler \Elab.PathConPretype -> do
+      putStrLn $ "Pretypes can not have path constructors, either change this definition so it lands in Type or remove it."
   ]
 
 redact :: Lt.Text -> Lt.Text
@@ -237,17 +244,29 @@ redact x
   | length (Lt.lines x) >= 2 = head (Lt.lines x) <> Lt.pack "\x1b[1;32m[...]\x1b[0m"
   | otherwise = x
 
-reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO ()
-reportUnsolved metas = do
+reportUnsolved :: Foldable t => Maybe Text -> Map.Map MV (t (Seq Projection, Value)) -> IO ()
+reportUnsolved code metas = do
   for_ (Map.toList metas) \(m, p) ->  do
     case mvSpan m of
-      Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
+      Just (f, s, e) ->
+        case code of
+          Just code -> T.putStrLn $ squiggleUnder s e code
+          Nothing -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
       Nothing -> pure ()
-    Lt.putStrLn . render $
-      "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyVl (zonk (mvType m)) <+> "should satisfy:"
-    for_ p \p ->
-      Lt.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p))
 
+    case null p of
+      True -> do
+        Lt.putStrLn . render $ "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <> pretty '.')
+      _ -> do
+        Lt.putStrLn . render $
+          "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <+> "should satisfy:")
+        for_ p \p ->
+          Lt.putStrLn . render $ indent 2 $ prettyTm (quote (zonk (VNe (HMeta m) (fst p)))) <+> pretty '≡' <+> prettyTm (quote (snd p))
+    
+    when (mvInteraction m && not (Map.null (mvContext m))) do
+      putStrLn "Context (first 10 entries):"
+      for_ (take 10 (Map.toList (mvContext m))) \(x, t) -> unless (isIdkT t) do
+        Lt.putStrLn . render $ indent 2 $ pretty x <+> pretty ':' <+> prettyVl (zonk t)
 
 displayExceptions' :: Exception e => Text -> e -> IO ()
 displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure ()
diff --git a/src/Syntax.hs b/src/Syntax.hs
index b858df8..47670cd 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -114,6 +114,8 @@ data MV =
      , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
      , mvType :: NFType
      , mvSpan :: Maybe (Text, Posn, Posn)
+     , mvInteraction :: Bool
+     , mvContext :: Map Name NFType
      }
 
 instance Eq MV where
@@ -226,7 +228,12 @@ quoteWith names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) =
 
 quoteWith names (GluedVl h sp vl)
   | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
-  | alwaysShort vl = quoteWith names vl
+  | True || alwaysShort vl = quoteWith names vl
+  | _ Seq.:|> PIElim _ x y i <- sp =
+    case i of
+      VI0 -> quoteWith names x
+      VI1 -> quoteWith names y
+      _ -> quoteWith names (VNe h sp)
   | otherwise = quoteWith names (VNe h sp)
 
 quoteWith names (VLam p (Closure n k)) =
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index a264ff8..5a4355b 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -18,7 +18,7 @@ import Prettyprinter
 import Syntax
 
 instance Pretty Name where
-  pretty = pretty . getNameText
+  pretty x = pretty (getNameText x) -- <> pretty '\'' <> pretty (getNameNum x)
 
 prettyTm' :: Bool -> Term -> Doc AnsiStyle
 prettyTm' implicits = go True 0 where
@@ -84,10 +84,15 @@ prettyTm' implicits = go True 0 where
       Type -> keyword (pretty "Type")
       Typeω -> keyword (pretty "Pretype")
 
+      Sigma (T.unpack . getNameText -> "_") d r ->
+        parenIf (p >= fun_prec) $
+              go False dom_prec d
+          <+> operator (pretty "*")
+          <+> go False dom_prec r
       Sigma v d r ->
         parenIf (p >= fun_prec) . align $
           group (parens (pretty v <+> colon <+> go False 0 d))
-            <+> operator (pretty "*") <+> go False 0 r
+            <+> operator (pretty "*") <+> go False dom_prec r
 
       Pair a b -> parens $ go False 0 a <> comma <+> go False 0 b
       Proj1 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".1")
@@ -114,12 +119,12 @@ prettyTm' implicits = go True 0 where
       Partial a p -> apps (con "Partial") [(Ex, a), (Ex, p)]
       PartialP a p -> apps (con "PartialP") [(Ex, a), (Ex, p)]
 
-      System fs | Map.null fs -> braces mempty
+      System fs | Map.null fs -> brackets mempty
       System fs ->
         let
           face (f, t) = go False 0 f <+> operator (pretty "=>") <+> go False 0 t
         in
-          braces (line <> nest 2 (vsep (punctuate comma (map face (Map.toList fs)))) <> line)
+          brackets (line <> nest 2 (vsep (punctuate comma (map face (Map.toList fs)))) <> line)
 
       Sub a phi u -> apps (con "Sub") [(Ex, a), (Ex, phi), (Ex, u)]
       Inc a phi u -> apps (con "inS") [(Im, a), (Im, phi), (Ex, u)]