From c318bfaf67c3d6cc50ae1c0c292ab5dc3d64781b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?=
 <magalhaes.alcantara@pucpr.edu.br>
Date: Sat, 10 Apr 2021 03:04:50 -0300
Subject: [PATCH] Small tweaks to some builtins
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Remove [φ] since it's the same thing as φ ≡s i1

* Change the type of comp to reflect that the returned element agrees
  with the sides on i1.
---
 intro.tt             | 138 ++++++++++++++++++++++++++++---------------
 src/Elab.hs          |  32 +++++-----
 src/Elab/Eval.hs     |  68 ++++++++++-----------
 src/Elab/WiredIn.hs  |  65 ++++++++++----------
 src/Main.hs          |  13 ++--
 src/Syntax.hs        |  16 +----
 src/Syntax/Pretty.hs |   9 +--
 7 files changed, 188 insertions(+), 153 deletions(-)

diff --git a/intro.tt b/intro.tt
index 438f6b2..5f1e436 100644
--- a/intro.tt
+++ b/intro.tt
@@ -141,18 +141,29 @@ funext h i x = h x i
 -- The proposition associated with an element of the interval
 -------------------------------------------------------------
 
+Eq_s : {A : Pretype} -> A -> A -> Pretype
+{-# PRIMITIVE Eq_s #-}
+
+refl_s : {A : Pretype} {x : A} -> Eq_s x x
+{-# PRIMITIVE refl_s #-}
+
+J_s : {A : Pretype} {x : A} (P : (y : A) -> Eq_s x y -> Pretype) -> P x (refl_s {A} {x}) -> {y : A} -> (p : Eq_s x y) -> P y p
+{-# PRIMITIVE J_s #-}
+
+K_s : {A : Pretype} {x : A} (P : Eq_s x x -> Pretype) -> P (refl_s {A} {x}) -> (p : Eq_s x x) -> P p
+{-# PRIMITIVE K_s #-}
+
 -- Associated with every element i : I of the interval, we have the type
 -- IsOne i which is inhabited only when i = i1. In the model, this
 -- corresponds to the map [φ] from the interval cubical set to the
 -- subobject classifier.
 
 IsOne : I -> Pretype
-{-# PRIMITIVE IsOne #-}
+IsOne i = Eq_s i i1
 
 -- The value itIs1 witnesses the fact that i1 = i1.
 itIs1 : IsOne i1
-
-{-# PRIMITIVE itIs1 #-}
+itIs1 = refl_s
 
 -- Partial elements
 -------------------
@@ -212,8 +223,11 @@ outS : {A : Type} {phi : I} {u : Partial phi A} -> Sub A phi u -> A
 -- and specifying that an element agrees with a partial cube,
 -- we can describe the composition operation.
 
+primComp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> Sub (A i1) phi (u i1)
+{-# PRIMITIVE comp primComp #-}
+
 comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1
-{-# PRIMITIVE comp #-}
+comp A {phi} u a0 = outS (primComp A {phi} u a0)
 
 -- In particular, when φ is a disjunction of the form
 -- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a
@@ -259,7 +273,7 @@ transp A x = comp A {i0} (\i [ ]) (inS 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)) -> Sub (A i0) phi (u i0) -> (i : I) -> A i
+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)}
@@ -269,7 +283,7 @@ fill A {phi} u a0 i =
 hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A
 hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0
 
-hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> (a0 : Sub A phi (u i0)) -> I -> A
+hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> (a0 : Sub A phi (u i0)) -> Path (outS a0) (hcomp u a0)
 hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
 
 -- For instance, the filler of the previous composition square
@@ -278,8 +292,8 @@ hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
 transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p
 transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)
 
-transpFill : {A : Type} (x : A) -> Path x (transp (\i -> A) x)
-transpFill {A} x i = fill (\i -> A) (\k []) (inS x) i
+transpFill : {A : I -> Type} (x : A i0) -> PathP A x (transp (\i -> A i) x)
+transpFill {A} x i = fill (\i -> A i) (\k []) (inS x) i
 
 -- Reduction of composition
 ---------------------------
@@ -315,7 +329,7 @@ transpDFun f = refl
 -- path f(x) = y.
 
 fiber : {A : Type} {B : Type} -> (A -> B) -> B -> Type
-fiber f y = (x : A) * Path (f x) y
+fiber f y = (x : A) * Path y (f x)
 
 -- An *equivalence* is a function where every fiber is contractible.
 -- That is, for every point in the codomain y : B, there is exactly one
@@ -327,13 +341,11 @@ isEquiv {A} {B} f = (y : B) -> isContr (fiber {A} {B} f y)
 -- By extracting this point, which must exist because the fiber is contractible,
 -- we can get an inverse of f:
 
-inverse : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
-inverse eqv y = (eqv y) .1 .1
+invert : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
+invert eqv y = (eqv y) .1 .1
 
--- We can prove that «inverse eqv» is a section of f:
-
-section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id
-section f eqv i y = (eqv y) .1 .2 i
+retract : {A : Type} {B : Type} -> (A -> B) -> (B -> A) -> Type
+retract {A} {B} f g = (a : A) -> Path (g (f a)) a
 
 contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> A
 contr {A} {phi} p u = comp (\i -> A) {phi} (\i is1 -> p.2 (u is1) i) (inS (p.1))
@@ -348,7 +360,7 @@ Equiv A B = (f : A -> B) * isEquiv {A} {B} f
 -- The identity function is an equivalence between any type A and
 -- itself.
 idEquiv : {A : Type} -> isEquiv (id {A})
-idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j)))
+idEquiv y = ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j)))
 
 -- The glue operation expresses that "extensibility is invariant under
 -- equivalence". Less concisely, the Glue type and its constructor,
@@ -377,6 +389,12 @@ prim'glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o ->
 
 {-# PRIMITIVE glue prim'glue #-}
 
+glue : {A : Type} {phi : I} {Te : Partial phi ((T : Type) * Equiv T A)}
+      -> (t : PartialP phi (\o -> (Te o).1))
+      -> (im : Sub A phi (\o -> (Te o).2.1 (t o)))
+      -> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2)
+glue {A} {phi} {Te} t im = prim'glue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} t im
+
 -- The unglue operation undoes a glueing. Since when φ = i1,
 -- Glue A [φ -> (T, f)] = T, the argument to primUnglue {A} {i1} ...
 -- will have type T, and so to get back an A we need to apply the
@@ -387,6 +405,10 @@ primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -
 
 {-# PRIMITIVE unglue primUnglue #-}
 
+unglue : {A : Type} (phi : I) {Te : Partial phi ((T : Type) * Equiv T A)}
+      -> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2) -> A
+unglue {A} phi {Te} = primUnglue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2}
+
 -- Diagramatically, i : I |- Glue A [(i \/ ~i) -> (T, e)] can be drawn
 -- as giving us the dotted line in:
 --
@@ -425,6 +447,11 @@ univalence {A} {B} equiv i =
   Glue B (\[ (i = i0) -> (A, equiv),
              (i = i1) -> (B, the B, idEquiv {B}) ]) 
 
+lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)
+{-# PRIMITIVE lineToEquiv #-}
+
+idToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
+idToEquiv p = lineToEquiv (\i -> p i)
 
 -- The fact that this diagram has 2 filled-in B sides explains the
 -- complication in the proof below.
@@ -517,15 +544,15 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
   s = iso.2.2.1
   t = iso.2.2.2
 
-  lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path (f x0) y) (p1 : Path (f x1) y)
+  lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path y (f x0)) (p1 : Path y (f x1))
         -> PathP (\i -> fiber f y) (x0, p0) (x1, p1)
   lemIso y x0 x1 p0 p1 =
     let
       rem0 : Path x0 (g y)
-      rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i)))
+      rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 (inot i))))
 
       rem1 : Path x1 (g y)
-      rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i)))
+      rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 (inot i))))
 
       p : Path x0 x1
       p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))
@@ -533,15 +560,15 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
       fill0 : I -> I -> A
       fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k)
                                      , (i = i1) -> g y
-                                     , (j = i0) -> g (p0 i) 
+                                     , (j = i0) -> g (p0 (inot i)) 
                                      ])
-                            (inS (g (p0 i)))
+                            (inS (g (p0 (inot i))))
 
       fill1 : I -> I -> A
       fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k)
                                      , (i = i1) -> g y
-                                     , (j = i0) -> g (p1 i) ])
-                            (inS (g (p1 i)))
+                                     , (j = i0) -> g (p1 (inot i)) ])
+                            (inS (g (p1 (inot i))))
 
       fill2 : I -> I -> A
       fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k))
@@ -557,16 +584,16 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
                           (inS (fill2 i j))
 
       sq1 : I -> I -> B
-      sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 j) k
-                                   , (i = i1) -> s (p1 j) k
+      sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 (inot j)) k
+                                   , (i = i1) -> s (p1 (inot j)) k
                                    , (j = i0) -> s (f (p i)) k
                                    , (j = i1) -> s y k
                                    ])
                           (inS (f (sq i j)))
-    in \i -> (p i, \j -> sq1 i j)
+    in \i -> (p i, \j -> sq1 i (inot j))
 
   fCenter : (y : B) -> fiber f y
-  fCenter y = (g y, s y)
+  fCenter y = (g y, sym (s y))
 
   fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w
   fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2
@@ -653,8 +680,12 @@ trueNotFalse p = transp (\i -> if (Bool -> Bool) Bottom (p i)) id
 --
 -- isHSet A = (x : A) (y : A) -> isHProp (Path x y)
 --
+
+isProp : Type -> Type
+isProp A = (x : A) (y : A) -> Path x y
+
 isHSet : Type -> Type
-isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q
+isHSet A = (x : A) (y : A) -> isProp (Path x y)
 
 -- We can prove *a* contradiction (note: this is a direct proof!) by adversarially
 -- choosing two paths p, q that we know are not equal. Since "equal" paths have
@@ -665,7 +696,7 @@ isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q
 -- of false as the point x is just from the endpoints of trueNotFalse.
 
 universeNotSet : isHSet Type -> Bottom
-universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false)
+universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs Bool Bool notp refl i j) false)
 
 -- Funext is an inverse of happly
 ---------------------------------
@@ -1048,9 +1079,6 @@ four = multInt two two
 sixteen : Int
 sixteen = multInt four four
 
-isProp : Type -> Type
-isProp A = (x : A) (y : A) -> Path x y
-
 Prop : Type
 Prop = (A : Type) * isProp A
 
@@ -1059,7 +1087,7 @@ data Sq (A : Type) : Type where
   sq i : (x : Sq A) (y : Sq A) -> Sq A [ (i = i0) -> x, (i = i1) -> y ]
 
 isProp_isSet : {A : Type} -> isProp A -> isHSet A
-isProp_isSet h {a} {b} p q j i =
+isProp_isSet h a b p q j i =
   hcomp {A}
     (\k [ (i = i0) -> h a a k
         , (i = i1) -> h a b k
@@ -1069,7 +1097,7 @@ isProp_isSet h {a} {b} p q j i =
     (inS a)
 
 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_isProp f g i a b = isProp_isSet f a b (f a b) (g a b) i
 
 Sq_rec : {A : Type} {B : Type}
       -> isProp B
@@ -1161,15 +1189,6 @@ S3IsSuspS2 = univalence (IsoToEquiv iso) where
   iso : Iso S3 (Susp S2)
   iso = (fromS3, toS3, fromToS3, toFromS3)
 
-Eq_s : {A : Pretype} -> A -> A -> Pretype
-{-# PRIMITIVE Eq_s #-}
-
-refl_s : {A : Pretype} {x : A} -> Eq_s x x
-{-# PRIMITIVE refl_s #-}
-
-J_s : {A : Pretype} {x : A} (P : (y : A) -> Eq_s x y -> Pretype) -> P x (refl_s {A} {x}) -> {y : A} -> (p : Eq_s x y) -> P y p
-{-# PRIMITIVE J_s #-}
-
 ap_s : {A : Pretype} {B : Pretype} (f : A -> B) {x : A} {y : A} -> Eq_s x y -> Eq_s (f x) (f y)
 ap_s {A} {B} f {x} {y} = J_s (\y p -> Eq_s (f x) (f y)) refl_s
 
@@ -1179,9 +1198,6 @@ subst_s {A} P {x} {z} p px = J_s {A} {x} (\y p -> P x -> P y) id p px
 sym_s : {A : Pretype} {x : A} {y : A} -> Eq_s x y -> Eq_s y x
 sym_s {A} {x} {y} = J_s {A} {x} (\y p -> Eq_s y x) refl_s
 
-K_s : {A : Pretype} {x : A} (P : Eq_s x x -> Pretype) -> P (refl_s {A} {x}) -> (p : Eq_s x x) -> P p
-{-# PRIMITIVE K_s #-}
-
 UIP : {A : Pretype} {x : A} {y : A} (p : Eq_s x y) (q : Eq_s x y) -> Eq_s p q
 UIP {A} {x} {y} p q = J_s (\y p -> (q : Eq_s x y) -> Eq_s p q) (uipRefl A x) p q where
   uipRefl : (A : Pretype) (x : A) (p : Eq_s x x) -> Eq_s refl_s p
@@ -1217,11 +1233,35 @@ pathToEqS_K {A} {x} p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop wh
     aux = seq_pathRefl (p_to_s (\i -> x))
 
 pathToEq_isSet : {A : Type} -> ({x : A} {y : A} -> Path x y -> Eq_s x y) -> isHSet A
-pathToEq_isSet {A} p_to_s {x} {y} p q = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) {x} {y} p q where
+pathToEq_isSet {A} p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) where
   axK_to_isSet : {A : Type} -> ({x : A} -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p) -> isHSet A
-  axK_to_isSet K {x} {y} p q = J (\y p -> (q : Path x y) -> Path p q) (uipRefl x) p q where
+  axK_to_isSet K x y p q = J (\y p -> (q : Path x y) -> Path p q) (uipRefl x) p q where
     uipRefl : (x : A) (p : Path x x) -> Path refl p
     uipRefl x p = K {x} (\q -> Path refl q) refl p
 
 Nat_isSet : isHSet Nat
-Nat_isSet {x} {y} = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y) {x} {y}
\ No newline at end of file
+Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y)
+
+equivCtr : {A : Type} {B : Type} (e : Equiv A B) (y : B) -> fiber e.1 y
+equivCtr e y = (e.2 y).1
+
+equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B)
+            -> (v : fiber e.1 y) -> Path (equivCtr e y) v
+equivCtrPath e y = (e.2 y).2
+
+contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> Sub A phi u
+contr {A} {phi} p u = primComp (\i -> A) (\i [ (phi = i1) as c -> p.2 (u c) i ]) (inS p.1)
+
+contr' : {A : Type} -> ({phi : I} -> (u : Partial phi A) -> Sub A phi u) -> isContr A
+contr' {A} contr = (x, \y i -> outS (contr (\ [ (i = i0) -> x, (i = i1) -> y ])) ) where
+  x : A
+  x = outS (contr (\ []))
+
+leftIsOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s (ior a b) i1
+leftIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior i b)) refl_s (sym_s p)
+
+rightIsOne : {a : I} {b : I} -> Eq_s b i1 -> Eq_s (ior a b) i1
+rightIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior a i)) refl_s (sym_s p)
+
+bothAreOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s b i1 -> Eq_s (iand a b) i1
+bothAreOne {a} {b} p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p)
\ No newline at end of file
diff --git a/src/Elab.hs b/src/Elab.hs
index 0b07e20..b1cea92 100644
--- a/src/Elab.hs
+++ b/src/Elab.hs
@@ -55,10 +55,10 @@ infer (P.App p f x) = do
       x_nf <- eval x
       pure (IElim (quote (fun li)) (quote le) (quote ri) (wp f) x, li x_nf)
     It'sPartial phi a w -> do
-      x <- check x (VIsOne phi)
+      x <- check x (VEqStrict VI phi VI1)
       pure (App P.Ex (w f) x, a)
     It'sPartialP phi a w -> do
-      x <- check x (VIsOne phi)
+      x <- check x (VEqStrict VI phi VI1)
       x_nf <- eval x
       pure (App P.Ex (w f) x, a @@ x_nf)
 
@@ -108,11 +108,11 @@ check (P.Lam p v b) ty = do
       pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
 
     It'sPartial phi a wp ->
-      assume (Bound v 0) (VIsOne phi) $ \var ->
+      assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
         wp . Lam p var <$> check b a
 
     It'sPartialP phi a wp ->
-      assume (Bound v 0) (VIsOne phi) $ \var ->
+      assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
         wp . Lam p var <$> check b (a @@ VVar var)
 
 check (P.Pair a b) ty = do
@@ -149,16 +149,18 @@ check (P.LamSystem bs) ty = do
   eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
     phi <- checkFormula (P.condF formula)
     rhses <-
-        case P.condV formula of
-          Just t -> assume (Bound t 0) (VIsOne phi) $ \var -> do
-            env <- ask
-            for (truthAssignments phi (getEnv env)) $ \e -> do
-              let env' = env{ getEnv = e }
+      case P.condV formula of
+        Just t -> assume (Bound t 0) (VEqStrict VI phi VI1) $ \var -> do
+          env <- ask
+          for (truthAssignments phi (getEnv env)) $ \e -> do
+            let env' = env{ getEnv = e }
+            local (const env') $
               (Just var,) <$> check rhs (eval' env' dom_q)
-          Nothing -> do
-            env <- ask
-            for (truthAssignments phi (getEnv env)) $ \e -> do
-              let env' = env{ getEnv = e }
+        Nothing -> do
+          env <- ask
+          for (truthAssignments phi (getEnv env)) $ \e -> do
+            let env' = env{ getEnv = e }
+            local (const env') $
               (Nothing,) <$> check rhs (eval' env' dom_q)
     pure (n, (phi, head rhses))
 
@@ -167,12 +169,12 @@ check (P.LamSystem bs) ty = do
   for_ eqns $ \(n, (formula, (binding, rhs))) -> do
     let
       k = case binding of
-        Just v -> assume v (VIsOne formula) . const
+        Just v -> assume v (VEqStrict VI formula VI1) . const
         Nothing -> id
     k $ for_ eqns $ \(n', (formula', (binding, rhs'))) -> do
       let
         k = case binding of
-          Just v -> assume v (VIsOne formula) . const
+          Just v -> assume v (VEqStrict VI formula VI1) . const
           Nothing -> id
         truth = possible mempty (iand formula formula')
         add [] = id
diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs
index b9ea7a1..6c57dda 100644
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@@ -76,9 +76,6 @@ zonkIO (VIAnd x y) = iand <$> zonkIO x <*> zonkIO y
 zonkIO (VIOr x y) = ior <$> zonkIO x <*> zonkIO y
 zonkIO (VINot x) = inot <$> zonkIO x
 
-zonkIO (VIsOne x) = VIsOne <$> zonkIO x
-zonkIO VItIsOne = pure VItIsOne
-
 zonkIO (VPartial x y)  = VPartial <$> zonkIO x <*> zonkIO y
 zonkIO (VPartialP x y) = VPartialP <$> zonkIO x <*> zonkIO y
 zonkIO (VSystem fs) = do
@@ -164,9 +161,6 @@ eval' e (PathP l a b) = VPath (eval' e l) (eval' e a) (eval' e b)
 eval' e (IElim l x y f i) = ielim (eval' e l) (eval' e x) (eval' e y) (eval' e f) (eval' e i)
 eval' e (PathIntro p x y f) = VLine (eval' e p) (eval' e x) (eval' e y) (eval' e f)
 
-eval' e (IsOne i)  = VIsOne (eval' e i)
-eval' _ ItIsOne    = VItIsOne
-
 eval' e (Partial x y)  = VPartial (eval' e x) (eval' e y)
 eval' e (PartialP x y) = VPartialP (eval' e x) (eval' e y)
 eval' e (System fs) = mkVSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
@@ -231,6 +225,8 @@ data NotEqual = NotEqual Value Value
   deriving (Show, Typeable, Exception)
 
 unify' :: HasCallStack => Value -> Value -> ElabM ()
+-- unify' (GluedVl h sp _) (GluedVl h' sp' _)
+--   | h == h', length sp == length sp' = traverse_ (uncurry unify'Spine) (Seq.zip sp sp')
 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
@@ -296,12 +292,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     n <- VVar <$> newName
     unify' (ielim l x y p' n) (p @@ n)
 
-  go (VIsOne x) (VIsOne y) = unify' x y
-
-  -- IsOne is proof-irrelevant:
-  go VItIsOne _ = pure ()
-  go _ VItIsOne = pure ()
-
   go (VPartial phi r) (VPartial phi' r')   = unify' phi phi' *> unify' r r'
   go (VPartialP phi r) (VPartialP phi' r') = unify' phi phi' *> unify' r r'
 
@@ -311,8 +301,8 @@ 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 (VGlueTy _ (force -> VI1) u _0) rhs = unify' (u @@ VItIsOne) rhs
-  go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VItIsOne)
+  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)
 
   go (VGlueTy a phi u a0) (VGlueTy a' phi' u' a0') =
     traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
@@ -320,11 +310,16 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VGlue a phi u a0 t x) (VGlue a' phi' u' a0' t' x') =
     traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')]
 
+  go (VUnglue a phi u a0 x) (VUnglue a' phi' u' a0' x') =
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (x, x')]
+
   go (VSystem sys) rhs = goSystem unify' sys rhs
   go rhs (VSystem sys) = goSystem (flip unify') sys rhs
 
   go (VEqStrict a x y) (VEqStrict a' x' y') = traverse_ (uncurry unify') [(a, a'), (x, x'), (y, y')]
   go (VReflStrict a x) (VReflStrict a' x') = traverse_ (uncurry unify') [(a, a'), (x, x')]
+  go _ VReflStrict{} = pure ()
+  go VReflStrict{} _ = pure ()
 
   go x y
     | x == y = pure ()
@@ -339,32 +334,33 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     env <- ask
     for_ (Map.toList sys) $ \(f, i) -> do
       let i_q = quote i
-      for (truthAssignments f (getEnv env)) $ \e ->
+      for (truthAssignments f (getEnv env)) $ \e -> do
         k (eval' env{getEnv = e} i_q) (eval' env{getEnv = e} rhs_q)
 
   fail = throwElab $ NotEqual topa topb
 
-  unify'Spine (PApp a v) (PApp a' v')
-    | a == a' = unify' v v'
+  unify'Formula x y
+    | compareDNFs x y = pure ()
+    | otherwise = fail
 
-  unify'Spine PProj1 PProj1 = pure ()
-  unify'Spine PProj2 PProj2 = pure ()
+unify'Spine :: Projection -> Projection -> ElabM ()
+unify'Spine (PApp a v) (PApp a' v')
+  | a == a' = unify' v v'
 
-  unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j
-  unify'Spine (POuc a phi u) (POuc a' phi' u') =
-    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
+unify'Spine PProj1 PProj1 = pure ()
+unify'Spine PProj2 PProj2 = pure ()
 
-  unify'Spine (PK a x p pr) (PK a' x' p' pr') =
-    traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr')]
+unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j
+unify'Spine (POuc a phi u) (POuc a' phi' u') =
+  traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
 
-  unify'Spine (PJ a x p pr y) (PJ a' x' p' pr' y') =
-    traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr'), (y, y')]
+unify'Spine (PK a x p pr) (PK a' x' p' pr') =
+  traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr')]
 
-  unify'Spine _ _ = fail
+unify'Spine (PJ a x p pr y) (PJ a' x' p' pr' y') =
+  traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr'), (y, y')]
 
-  unify'Formula x y
-    | compareDNFs x y = pure ()
-    | otherwise = fail
+unify'Spine _ _ = throwElab (NotEqual undefined undefined)
 
 unify :: HasCallStack => Value -> Value -> ElabM ()
 unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
@@ -385,6 +381,12 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where
     wp' <- k (VVar n) `isConvertibleTo` k' (wp_n @@ VVar n)
     pure (\f -> Lam p n (wp' (App p f (wp (Ref n)))))
 
+  VPath a x y `isConvertibleTo` VPi Ex d (Closure _ k') = do
+    unify d VI
+    nm <- newName
+    wp <- isConvertibleTo (a @@ VVar nm) (k' (VVar nm))
+    pure (\f -> Lam Ex nm (wp (IElim (quote a) (quote x) (quote y) f (Ref nm))))
+
   isConvertibleTo a b = do
     unify' a b
     pure id
@@ -490,9 +492,6 @@ checkScope s (VINot x)   = checkScope s x
 checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
 checkScope s (VLine _ _ _ line)   = checkScope s line
 
-checkScope s (VIsOne x) = checkScope s x
-checkScope _ VItIsOne   = pure ()
-
 checkScope s (VPartial x y)  = traverse_ (checkScope s) [x, y]
 checkScope s (VPartialP x y) = traverse_ (checkScope s) [x, y]
 checkScope s (VSystem fs) =
@@ -563,9 +562,6 @@ substituteIO sub = substituteIO . force where
   substituteIO (VIOr x y) = ior <$> substituteIO x <*> substituteIO y
   substituteIO (VINot x) = inot <$> substituteIO x
 
-  substituteIO (VIsOne x) = VIsOne <$> substituteIO x
-  substituteIO VItIsOne = pure VItIsOne
-
   substituteIO (VPartial x y)  = VPartial <$> substituteIO x <*> substituteIO y
   substituteIO (VPartialP x y) = VPartialP <$> substituteIO x <*> substituteIO y
   substituteIO (VSystem fs) = do
diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs
index deaf6ac..93da268 100644
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@@ -39,9 +39,6 @@ wiType WiIOr      = VI ~> VI ~> VI
 wiType WiINot     = VI ~> VI
 wiType WiPathP    = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
 
-wiType WiIsOne    = VI ~> VTypeω
-wiType WiItIsOne  = VIsOne VI1
-
 wiType WiPartial  = VI ~> VType ~> VTypeω
 wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
 
@@ -49,7 +46,8 @@ wiType WiSub      = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω
 wiType WiInS      = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (fun (const u))
 wiType WiOutS     = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> 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) ~> a @@ VI1
+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
@@ -63,6 +61,8 @@ wiType WiSRefl = forAll' "A" VTypeω \a -> forAll' "x" a \x -> VEqStrict a x x
 wiType WiSK    = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (VEqStrict a x x ~> VTypeω) \bigp -> (bigp @@ VReflStrict a x) ~> dprod' "p" (VEqStrict a x x) \p -> bigp @@ p
 wiType WiSJ    = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (dprod' "y" a \y -> VEqStrict a x y ~> VTypeω) \bigp -> bigp @@ x @@ VReflStrict a x ~> forAll' "y" a \y -> dprod' "p" (VEqStrict a x y) \p -> bigp @@ y @@ p
 
+wiType WiLineToEquiv = dprod' "P" (VI ~> VType) \a -> equiv (a @@ VI0) (a @@ VI1)
+
 wiValue :: WiredIn -> Value
 wiValue WiType     = VType
 wiValue WiPretype  = VTypeω
@@ -76,15 +76,12 @@ wiValue WiIOr       = fun \x -> fun \y -> ior x y
 wiValue WiINot      = fun inot
 wiValue WiPathP     = fun \a -> fun \x -> fun \y -> VPath a x y
 
-wiValue WiIsOne   = fun VIsOne
-wiValue WiItIsOne = VItIsOne
-
 wiValue WiPartial  = fun \phi -> fun \r -> VPartial phi r
 wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
 wiValue WiSub      = fun \a -> fun \phi -> fun \u -> VSub a phi u
 wiValue WiInS      = forallI \a -> forallI \phi -> fun \u -> VInc a phi u
 wiValue WiOutS     = forallI \a -> forallI \phi -> forallI \u -> fun \x -> outS a phi u x
-wiValue WiComp     = fun \a -> forallI \phi -> fun \u -> fun \x -> comp a phi u x
+wiValue WiComp     = fun \a -> forallI \phi -> fun \u -> fun \x -> VInc (a @@ VI1) phi (comp a phi u x)
 
 wiValue WiGlue     = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a phi t e
 wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
@@ -95,6 +92,12 @@ wiValue WiSRefl = forallI \a -> forallI \x -> VReflStrict a x
 wiValue WiSK    = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> fun \p -> strictK a x bigp pr p
 wiValue WiSJ    = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> forallI \y -> fun \p -> strictJ a x bigp pr y p
 
+wiValue WiLineToEquiv = fun \l ->
+  GluedVl
+    (HCon VType (Defined "lineToEquiv" (-1)))
+    (Seq.fromList [(PApp P.Ex l)])
+    (makeEquiv' ((l @@) . inot))
+
 (~>) :: Value -> Value -> Value
 a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
 infixr 7 ~>
@@ -140,9 +143,6 @@ wiredInNames = Map.fromList
   , ("inot", WiINot)
   , ("PathP", WiPathP)
 
-  , ("IsOne", WiIsOne)
-  , ("itIs1", WiItIsOne)
-
   , ("Partial", WiPartial)
   , ("PartialP", WiPartialP)
   , ("Sub", WiSub)
@@ -158,6 +158,8 @@ wiredInNames = Map.fromList
   , ("refl_s", WiSRefl)
   , ("K_s", WiSK)
   , ("J_s", WiSJ)
+
+  , ("lineToEquiv", WiLineToEquiv)
   ]
 
 newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
@@ -220,7 +222,7 @@ ielim line left right fn i =
         _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
 
 outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
-outS _ (force -> VI1) u _  = u @@ VItIsOne
+outS _ (force -> VI1) u _  = u @@ VReflStrict VI VI1
 
 outS _ _phi _ (VInc _ _ x) = x
 outS _ VI0 _  x            = x
@@ -232,8 +234,8 @@ outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 
 -- Composition
 comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
-comp _a VI1 u _a0 =  u @@ VI1 @@ VItIsOne
-comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
+comp _a VI1 u _a0 =  u @@ VI1 @@ VReflStrict VI VI1
+comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
   case force (a @@ VVar name) of
     VPi{} ->
       let
@@ -281,7 +283,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
       let
         base i   = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b
         phi i    = substitute (Map.singleton name i) thePhi
-        types i  = substitute (Map.singleton name i) theTypes @@ VItIsOne
+        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)
@@ -294,7 +296,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
         (omega_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0
         omega = outS omega_t psi omega_rep omega_st
 
-        (t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VItIsOne) (del `ior` psi) (fun ts) (fun ps) a1'
+        (t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VReflStrict VI VI1) (del `ior` psi) (fun ts) (fun ps) a1'
         t1alpha = outS t1a_t (del `ior` psi) t1a_rep t1alpha_st
 
         (t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha)
@@ -305,14 +307,14 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
         a1 = comp
           (fun (const (base VI1)))
           (phi VI1 `ior` psi)
-          (system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VItIsOne)) alpha j)
-                                                   , (psi, a VI1 VItIsOne)]))
+          (system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)
+                                                   , (psi, a VI1 (VReflStrict VI VI1))]))
           (VInc (base VI1) (phi VI1 `ior` psi) a1')
         b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
        in b1
 
     VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
-                            (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VItIsOne))
+                            (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VReflStrict VI VI1))
 
     VNe (HData False _) Seq.Empty -> a0
     VNe (HData False _) args ->
@@ -324,7 +326,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
     VNe (HData True name) args -> compHIT name (length args) (a @@) phi u incA0
 
     VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
-    sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
+    VSystem map -> mkVSystem (fmap (\x -> comp x psi u incA0) map)
 
     _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
   where
@@ -347,13 +349,13 @@ forceAndGlue v =
 compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
 compHIT name n a phi u a0 =
   case force phi of
-    VI1 -> u @@ VI1 @@ VItIsOne
+    VI1 -> u @@ VI1 @@ VReflStrict VI VI1
     VI0 | n == 0 -> compOutS (a VI0) phi u a0
         | otherwise -> transHit name a VI0 (compOutS (a VI0) phi u a0)
     x -> go n a x u a0
   where
     go 0 a phi u a0 = VHComp (a VI0) phi u a0
-    go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VItIsOne) a0))
+    go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))
 
 compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
             -> Int
@@ -413,19 +415,19 @@ fill a phi u a0 j =
        a0
 
 hComp :: NFSort -> NFEndp -> Value -> Value -> Value
-hComp _ (force -> VI1) u _ = u @@ VI1 @@ VItIsOne
+hComp _ (force -> VI1) u _ = u @@ VI1 @@ VReflStrict VI VI1
 hComp a phi u a0 = VHComp a phi u a0
 
 glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
 glueType a phi tys eqvs = VGlueTy a phi tys eqvs
 
 glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
-glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VItIsOne
+glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VReflStrict VI VI1
 glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
 
 unglue   :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
-unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VItIsOne) @@ x
-unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ _ vl) = vl
+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
@@ -450,7 +452,7 @@ isContr :: Value -> Value
 isContr a = exists' "x" a \x -> dprod' "y" a \y -> VPath (line (const a)) x y
 
 fiber :: NFSort -> NFSort -> Value -> Value -> Value
-fiber a b f y = exists' "x" a \x -> VPath (line (const b)) (f @@ x) y
+fiber a b f y = exists' "x" a \x -> VPath (line (const b)) y (f @@ x)
 
 isEquiv :: NFSort -> NFSort -> Value -> Value
 isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y)
@@ -468,7 +470,7 @@ pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), p
   a0 = f VI0 @@ t0
   v = fill (fun tyT) phi (system \i u -> t i @@ u) t0
 
-  path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0
+  path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) (VInc (tyA VI0) phi a0)
 
 opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
 opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
@@ -525,9 +527,12 @@ makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0
 makeTransFiller _ _ _ _ _ _ a0 = fun (const a0)
 
 makeEquiv :: Name -> Value -> Value
-makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
+makeEquiv var vne = makeEquiv' \x -> substitute (Map.singleton var x) vne
+
+makeEquiv' :: (NFEndp -> Value) -> Value
+makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
   where
-    line = fun \i -> substitute (Map.singleton var (inot i)) vne
+    line = fun \i -> line' (inot i)
     a = line @@ VI0
     b = line @@ VI1
 
diff --git a/src/Main.hs b/src/Main.hs
index 4bb4d14..42f05a6 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -110,10 +110,15 @@ enterReplIn env =
               loop env envvar
 
     reload :: ElabEnv -> IORef ElabEnv -> InputT IO ()
-    reload ElabEnv{loadedFiles} envref = do
-      newe <- liftIO $ mkrepl <$> checkFiles (reverse loadedFiles)
-      liftIO $ writeIORef envref newe
-      loop newe envref
+    reload env@ElabEnv{loadedFiles} envref = do
+      newe <- liftIO $ try $ mkrepl <$> checkFiles (reverse loadedFiles)
+      case newe of
+        Left e -> do
+          liftIO $ displayExceptions' ":r" (e :: SomeException)
+          loop env envref
+        Right newe -> do
+          liftIO $ writeIORef envref newe
+          loop newe envref
 
 checkFiles :: [String] -> IO ElabEnv
 checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
diff --git a/src/Syntax.hs b/src/Syntax.hs
index 352b20f..04fbcd0 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -29,9 +29,6 @@ data WiredIn
   | WiINot
   | WiPathP
 
-  | WiIsOne   -- Proposition associated with an element of the interval
-  | WiItIsOne -- 1 = 1
-
   | WiPartial  -- (φ : I) -> Type           -> Typeω
   | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
 
@@ -41,12 +38,14 @@ data WiredIn
 
   | WiComp  --    {A : I -> Type} {phi : I}
             -- -> ((i : I) -> Partial phi (A i)
-            -- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u i1]
+            -- -> (A i0)[phi -> u i0] -> A i1
 
   | WiGlue      -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
   | WiGlueElem  -- {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
   | WiUnglue    -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
 
+  | WiLineToEquiv -- {A : I -> Type} -> Equiv (P i0) (P i1)
+
   -- Two-level
   | WiSEq   -- Eq_s   : {A : Pretype} (x y : A) -> Pretype
   | WiSRefl -- refl_s : {A : Pretype} {x : A} -> EqS {A} x x
@@ -86,9 +85,6 @@ data Term
   -- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
   --   ~~~~~~~~~ not printed at all
 
-  | IsOne Term
-  | ItIsOne
-
   | Partial  Term Term
   | PartialP Term Term
 
@@ -171,9 +167,6 @@ data Value
   | VPath NFLine Value Value
   | VLine NFLine Value Value Value
 
-  | VIsOne NFEndp
-  | VItIsOne
-
   | VPartial  NFEndp Value
   | VPartialP NFEndp Value
   | VSystem (Map Value Value)
@@ -258,9 +251,6 @@ quoteWith names (VINot x) = INot (quoteWith names x)
 quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
 quoteWith names (VLine p x y f)  = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
 
-quoteWith names (VIsOne v)  = IsOne (quoteWith names v)
-quoteWith _     VItIsOne    = ItIsOne
-
 quoteWith names (VPartial x y)  = Partial (quoteWith names x) (quoteWith names y)
 quoteWith names (VPartialP x y) = PartialP (quoteWith names x) (quoteWith names y)
 quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index 203bc60..0b26feb 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -76,7 +76,7 @@ prettyTm = go True 0 where
               <> keyword (pretty "in")
               <+> go False 0 body
 
-      Meta MV{mvName} -> keyword (pretty mvName)
+      Meta MV{mvName} -> keyword (pretty '?' <> pretty mvName)
 
       Type -> keyword (pretty "Type")
       Typeω -> keyword (pretty "Pretype")
@@ -108,9 +108,6 @@ prettyTm = go True 0 where
       IElim _a _x _y f i -> instead (App Ex f i)
       PathIntro _a _x _y f -> instead f
 
-      IsOne p -> brackets (go False 0 p)
-      ItIsOne -> keyword (pretty "1=1")
-
       Partial a p -> apps (con "Partial") [(Ex, a), (Ex, p)]
       PartialP a p -> apps (con "PartialP") [(Ex, a), (Ex, p)]
 
@@ -122,8 +119,8 @@ prettyTm = go True 0 where
           braces (line <> indent 2 (vsep (map face (Map.toList fs))) <> line)
 
       Sub a phi u -> apps (con "Sub") [(Ex, a), (Ex, phi), (Ex, u)]
-      Inc _ _hi u -> apps (con "inS") [(Ex, u)]
-      Ouc _ _hi _ a0 -> apps (con "outS") [(Ex, a0)]
+      Inc a phi u -> apps (con "inS") [(Ex, a), (Ex, phi), (Ex, u)]
+      Ouc a phi u a0 -> apps (con "outS") [(Ex, a), (Ex, phi), (Ex, u), (Ex, a0)]
 
       GlueTy a phi t e -> apps (con "primGlue") [(Ex, a), (Ex, phi), (Ex, t), (Ex, e)]
       Glue _a _phi _ty _e t im -> apps (con "glue") [(Ex, t), (Ex, im)]