diff --git a/cubical.cabal b/cubical.cabal
index 69eba61..8d63fcf 100644
--- a/cubical.cabal
+++ b/cubical.cabal
@@ -13,6 +13,11 @@ build-type:          Simple
 cabal-version:       >=2.0
 extra-source-files:  README.md
 
+flag release
+  description: "Release" mode
+  manual: True
+  default: False
+
 executable cubical
   hs-source-dirs:      src
   main-is:             Main.hs
@@ -53,3 +58,5 @@ executable cubical
 
   ghc-options:         -Wall -Wextra -Wno-name-shadowing -rtsopts
 
+  if flag(release)
+    ghc-options:       -XCPP -DRELEASE
diff --git a/intro.tt b/intro.tt
index ad64b91..73f10d0 100644
--- a/intro.tt
+++ b/intro.tt
@@ -66,12 +66,12 @@ PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
 -- Path.
 
 Path : {A : Type} -> A -> A -> Type
-Path {A} = PathP (\i -> A)
+Path = PathP (\i -> A)
 
 -- reflexivity is given by constant paths
 
 refl : {A : Type} {x : A} -> Path x x
-refl {A} {x} i = x
+refl i = x
 
 -- Symmetry (for dpeendent paths) is given by inverting the argument to the path, such that
 --   sym p i0 = p (inot i0) = p i1
@@ -111,7 +111,7 @@ isContr A = (x : A) * ((y : A) -> Path x y)
 -- singletons are contracible. Together with transport later on,
 -- we get the J elimination principle of paths.
 singContr : {A : Type} {a : A} -> isContr (Singl A a)
-singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))
+singContr = ((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.
@@ -186,6 +186,9 @@ Partial : I -> Type -> Pretype
 PartialP : (phi : I) -> Partial phi Type -> Pretype
 {-# PRIMITIVE PartialP #-}
 
+partialExt : {A : Type} (phi : I) (psi : I) -> Partial phi A -> Partial psi A -> Partial (ior phi psi) A
+{-# PRIMITIVE partialExt #-}
+
 -- Why is Partial φ A not just defined as φ -> A? The difference is that
 -- Partial φ A has an internal representation which definitionally relates
 -- any two partial elements which "agree everywhere", that is, have
@@ -202,7 +205,7 @@ PartialP : (phi : I) -> Partial phi Type -> Pretype
 -- That is, element of A[phi -> u] is an element of A defined everywhere
 -- (a total element), which, when IsOne φ, agrees with u.
 
-Sub  : (A : Type) (phi : I) -> Partial phi A -> Pretype
+Sub : (A : Type) (phi : I) -> Partial phi A -> Pretype
 {-# PRIMITIVE Sub #-}
 
 -- Every total element u : A can be made partial on φ by ignoring the
@@ -227,7 +230,7 @@ primComp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (
 {-# PRIMITIVE comp primComp #-}
 
 comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1
-comp A {phi} u a0 = outS (primComp A {phi} u a0)
+comp A 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
@@ -257,18 +260,12 @@ comp A {phi} u a0 = outS (primComp A {phi} u a0)
 --        x----------y
 --             p i
 
-trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z
-trans {A} {x} p q i =
-  comp (\i -> A)
-    {ior i (inot i)}
-    (\j [ (i = i0) -> x, (i = i1) -> q j ])
-    (inS (p i))
 
 -- In particular when the formula φ = i0 we get the "opposite face" to a
 -- single point, which corresponds to transport.
 
 transp : (A : I -> Type) (x : A i0) -> A i1
-transp A x = comp A {i0} (\i [ ]) (inS x)
+transp A x = comp A (\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
@@ -278,19 +275,28 @@ subst P p x = transp (\i -> P (p i)) x
 
 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 =
+fill A u a0 i =
     comp (\j -> A (iand i j))
          {ior phi (inot i)}
          (\j [ (phi = i1) -> u (iand i j) itIs1
-             , (i = i0)   -> outS a0
+             , (i = i0)   -> outS {A i0} {phi} {u i0} a0
              ])
          (inS (outS a0))
 
 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
+hcomp 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)) -> Path (outS a0) (hcomp u a0)
-hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
+hfill u a0 i = fill (\i -> A) {phi} u a0 i
+
+
+trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z
+trans p q i = comp (\j -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> q k ]) (inS {A} {ior i (inot i)} (p i))
+
+transFiller : {A : Type} {x : A} {y : A} {z : A}
+           -> (p : Path x y) (q : Path y z)
+           -> PathP (\i -> Path x (q i)) p (trans {A} {x} {y} {z} p q)
+transFiller p q j i = hfill (\k [ (i = i0) -> x, (i = i1) -> q k ]) (inS (p i)) j
 
 -- For instance, the filler of the previous composition square
 -- tells us that trans p refl = p:
@@ -301,18 +307,18 @@ transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1)
 rightCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p (sym p)) refl
 rightCancel p j i = cube p i1 j i where
   cube : {A : Type} {x : A} {y : A} (p : Path x y) -> I -> I -> I -> A
-  cube {A} {x} p k j i =
-    hfill {A} (\ k [ (i = i0) -> x
-                   , (i = i1) -> p (iand (inot k) (inot j))
-                   , (j = i1) -> x
-                   ])
-               (inS (p (iand i (inot j)))) k
+  cube p k j i =
+    hfill (\ k [ (i = i0) -> x
+               , (i = i1) -> p (iand (inot k) (inot j))
+               , (j = i1) -> x
+               ])
+          (inS (p (iand i (inot j)))) k
 
 leftCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans (sym p) p) refl
 leftCancel p = rightCancel (sym p)
 
-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
+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
 ---------------------------
@@ -365,7 +371,7 @@ invert : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
 invert eqv y = (eqv y) .1 .1
 
 retract : {A : Type} {B : Type} -> (A -> B) -> (B -> A) -> Type
-retract {A} {B} f g = (a : A) -> Path (g (f a)) a
+retract f g = (a : A) -> Path (g (f a)) a
 
 -- Proving that it's also a retraction is left as an exercise to the
 -- reader. We can package together a function and a proof that it's an
@@ -377,7 +383,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} -> Equiv A A
-idEquiv {A} = (\x -> x, \y -> ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j))))
+idEquiv = (\x -> x, \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,
@@ -400,7 +406,7 @@ primGlue : (A : Type) {phi : I}
 -- Agreeing with the condition that Glue A [i1 -> (T, e)] = T,
 -- we have that glue {A} {i1} t im => t.
 prim'glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}
-         -> (t  : PartialP phi T)
+         -> (t  : PartialP phi (\o -> T o))
          -> (im : Sub A phi (\o -> (e o).1 (t o)))
          -> primGlue A T e
 
@@ -410,7 +416,7 @@ 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
+glue 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} ...
@@ -424,7 +430,7 @@ primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -
 
 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}
+unglue phi = 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:
@@ -445,7 +451,7 @@ unglue {A} phi {Te} = primUnglue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2}
 -- equivalences, we can make a line between two types (T i0) and (T i1).
 
 Glue : (A : Type) {phi : I} -> Partial phi ((X : Type) * Equiv X A) -> Type
-Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)
+Glue A u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)
 
 -- For example, we can glue together the type A and the type B as long
 -- as there exists an Equiv A B.
@@ -460,9 +466,9 @@ Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)
 --             \i → B
 --
 ua : {A : Type} {B : Type} -> Equiv A B -> Path A B
-ua {A} {B} equiv i =
-  Glue B (\[ (i = i0) -> (A, equiv),
-             (i = i1) -> (B, idEquiv) ]) 
+ua equiv i =
+  Glue B (\[ (i = i0) -> (A, equiv)
+           , (i = i1) -> (B, idEquiv) ]) 
 
 lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)
 {-# PRIMITIVE lineToEquiv #-}
@@ -493,7 +499,7 @@ isEquivTransport A = (lineToEquiv A).2
 -- we need to come up with a filler for the Bottom and right faces.
 
 uaBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> ua f i)) f.1
-uaBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i)
+uaBeta f i a = transpFill (\i -> B) (f.1 a) (inot i)
 
 -- The terms ua + uaBeta suffice to prove the "full"
 -- ua axiom of Voevodsky, as can be seen in the paper
@@ -513,7 +519,7 @@ 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)
+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)
@@ -532,7 +538,7 @@ Jay P d s = transp (\i -> P ((singContr {A} {x}).2 s i)) d
 -- definition of equivalence.
 
 isIso : {A : Type} -> {B : Type} -> (A -> B) -> Type
-isIso {A} {B} f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x)
+isIso f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x)
 
 -- The reason is that the family of types IsIso is not a proposition!
 -- This means that there can be more than one way for a function to be
@@ -548,7 +554,7 @@ Iso A B = (f : A -> B) * isIso f
 -- https://github.com/mortberg/cubicaltt/blob/master/experiments/isoToEquiv.ctt#L7-L55
 
 IsoToEquiv : {A : Type} {B : Type} -> Iso A B -> Equiv A B
-IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
+IsoToEquiv iso = (f, \y -> (fCenter y, fIsCenter y)) where
   f = iso.1
   g = iso.2.1
   s = iso.2.2.1
@@ -559,47 +565,47 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
   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 (inot i))))
+      rem0 i = hcomp (\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 (inot i))))
+      rem1 i = hcomp (\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))
+      p i = hcomp (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))
 
       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 (inot i)) 
-                                     ])
-                            (inS (g (p0 (inot i))))
+      fill0 i j = hcomp (\k [ (i = i0) -> t x0 (iand j k)
+                            , (i = i1) -> g y
+                            , (j = i0) -> g (p0 (inot 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 (inot i)) ])
-                            (inS (g (p1 (inot i))))
+      fill1 i j = hcomp (\k [ (i = i0) -> t x1 (iand j k)
+                            , (i = i1) -> g y
+                            , (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))
-                                     , (i = i1) -> rem1 (ior j (inot k))
-                                     , (j = i1) -> g y ])
-                            (inS (g y))
+      fill2 i j = hcomp (\k [ (i = i0) -> rem0 (ior j (inot k))
+                            , (i = i1) -> rem1 (ior j (inot k))
+                            , (j = i1) -> g y ])
+                        (inS (g y))
 
       sq : I -> I -> A
-      sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k)
-                                  , (i = i1) -> fill1 j (inot k)
-                                  , (j = i1) -> g y
-                                  , (j = i0) -> t (p i) (inot k) ])
-                          (inS (fill2 i j))
+      sq i j = hcomp (\k [ (i = i0) -> fill0 j (inot k)
+                         , (i = i1) -> fill1 j (inot k)
+                         , (j = i1) -> g y
+                         , (j = i0) -> t (p i) (inot k) ])
+                     (inS (fill2 i j))
 
       sq1 : I -> I -> B
-      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)))
+      sq1 i j = hcomp (\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 (inot j))
 
   fCenter : (y : B) -> fiber f y
@@ -615,7 +621,7 @@ IsoToId i = ua (IsoToEquiv i)
 -- such a function is its own inverse.
 
 involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f
-involToIso {A} f inv = (f, inv, inv)
+involToIso f inv = (f, inv, inv)
 
 -- An example of ua
 ---------------------------
@@ -720,7 +726,7 @@ universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs Bool Bool notp refl
 -- extensionality. The strong version is as follows:
 
 Hom : {A : Type} {B : A -> Type} (f : (x : A) -> B x) -> (g : (x : A) -> B x) -> Type
-Hom {A} f g = (x : A) -> Path (f x) (g x)
+Hom f g = (x : A) -> Path (f x) (g x)
 
 happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
       -> (p : Path f g) -> Hom f g
@@ -730,11 +736,11 @@ happly p x i = p i x
 
 happlyIsIso : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
            -> isIso {Path f g} {Hom f g} happly
-happlyIsIso {A} {B} {f} {g} = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl)
+happlyIsIso = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl)
 
 pathIsHom : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
          -> Path (Path f g) (Hom f g)
-pathIsHom {A} {B} {f} {g} =
+pathIsHom =
   let
     theIso : Iso (Path f g) (Hom f g)
     theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
@@ -978,7 +984,7 @@ poSusp : Type -> Type
 poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt)
 
 Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A)
-Susp_is_poSusp {A} = ua (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where
+Susp_is_poSusp = ua (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where
   poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A
   poSusp_to_Susp = \case
     inl x -> north
@@ -1014,8 +1020,8 @@ data T2 : Type where
       (i = i1) -> pathOne j
     ]
 
-TorusIsTwoCircles : Path T2 (S1 * S1)
-TorusIsTwoCircles = ua (IsoToEquiv theIso) where
+TorusIsTwoCircles : Equiv T2 (S1 * S1)
+TorusIsTwoCircles = IsoToEquiv theIso where
   torusToCircs : T2 -> S1 * S1
   torusToCircs = \case
     baseT -> (base, base)
@@ -1143,11 +1149,11 @@ 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))
+  , \x i -> hcomp (\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
@@ -1170,7 +1176,7 @@ propExt {A} {B} propA propB f g = (f, contract) where
     let arg : A
         arg = g y
      in ( (arg, propB y (f arg))
-        , \fib -> sigmaPath (propA _ _) (isProp_isSet {B} propB y (f fib.1) _ _))
+        , \fib -> sigmaPath (propA _ _) (isProp_isSet propB y (f fib.1) _ _))
 
 Sq_rec : {A : Type} {B : Type}
       -> isProp B
@@ -1185,6 +1191,9 @@ Sq_rec prop f =
     work = \case
       inc x -> f x
 
+Sq_prop : {A : Type} -> isProp (Sq A)
+Sq_prop x y i = sq x y i
+
 hitTranspExample : Path (inc false) (inc true)
 hitTranspExample i = transp (\i -> Sq (notp i)) (sq (inc true) (inc false) i)
 
@@ -1201,12 +1210,12 @@ S2IsSuspS1 = ua (IsoToEquiv iso) where
       loop j -> \i -> surf2 i j
 
   suspSurf : I -> I -> I -> Susp S1
-  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 {S1} base (iand (inot k) i)
-                                     ])
-                                 (inS (merid (loop j) i))
+  suspSurf i j = hfill (\k [ (i = i0) -> north {S1}
+                           , (i = i1) -> merid {S1} base (inot k)
+                           , (j = i0) -> merid {S1} base (iand (inot k) i)
+                           , (j = i1) -> merid {S1} base (iand (inot k) i)
+                           ])
+                       (inS (merid (loop j) i))
 
   fromS2 : S2 -> Susp S1
   fromS2 = \case { base2 -> north; surf2 i j -> suspSurf i j i1 }
@@ -1237,14 +1246,14 @@ S3IsSuspS2 = ua (IsoToEquiv iso) where
       surf2 j k -> \i -> surf3 i j k
 
   suspSurf : I -> I -> I -> I -> Susp S2
-  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 {S2} base2 (iand (inot l) i)
-                                       , (k = i0) -> merid base2 (iand (inot l) i)
-                                       , (k = i1) -> merid {S2} base2 (iand (inot l) i)
-                                       ])
-                                   (inS (merid (surf2 j k) i))
+  suspSurf i j k = hfill (\l [ (i = i0) -> north {S2}
+                             , (i = i1) -> merid {S2} base2 (inot l)
+                             , (j = i0) -> merid {S2} base2 (iand (inot l) i)
+                             , (j = i1) -> merid {S2} base2 (iand (inot l) i)
+                             , (k = i0) -> merid {S2} base2 (iand (inot l) i)
+                             , (k = i1) -> merid {S2} base2 (iand (inot l) i)
+                             ])
+                         (inS (merid (surf2 j k) i))
 
   fromS3 : S3 -> Susp S2
   fromS3 = \case { base3 -> north; surf3 i j k -> suspSurf i j k i1 }
@@ -1263,24 +1272,24 @@ S3IsSuspS2 = ua (IsoToEquiv iso) where
   iso = (fromS3, toS3, fromToS3, toFromS3)
 
 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
+ap_s f {x} = J_s (\y p -> Eq_s (f x) (f y)) refl_s
 
 subst_s : {A : Pretype} (P : A -> Pretype) {x : A} {y : A} -> Eq_s x y -> P x -> P y
-subst_s {A} P {x} {z} p px = J_s {A} {x} (\y p -> P x -> P y) id p px
+subst_s {A} P {x} p px = J_s (\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
+sym_s = J_s (\y p -> Eq_s y x) refl_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
+UIP 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
-  uipRefl A x p = K_s {A} {x} (\q -> Eq_s refl_s q) refl_s p
+  uipRefl A x p = K_s (\q -> Eq_s refl_s q) refl_s p
 
 strictEq_pathEq : {A : Type} {x : A} {y : A} -> Eq_s x y -> Path x y
-strictEq_pathEq {A} {x} {y} eq = J_s {A} {x} (\y p -> Path x y) (\i -> x) {y} eq
+strictEq_pathEq eq = J_s {A} {x} (\y p -> Path x y) (\i -> x) {y} eq
 
 seq_pathRefl : {A : Type} {x : A} (p : Eq_s x x) -> Eq_s (strictEq_pathEq p) (refl {A} {x})
-seq_pathRefl {A} {x} p = K_s (\p -> Eq_s (strictEq_pathEq {A} {x} {x} p) (refl {A} {x})) refl_s p
+seq_pathRefl p = K_s (\p -> Eq_s (strictEq_pathEq {A} {x} {x} p) (refl {A} {x})) refl_s p
 
 Path_nat_strict_nat : (x : Nat) (y : Nat) -> Path x y -> Eq_s x y 
 Path_nat_strict_nat = \case { zero -> zeroCase; succ x -> succCase x } where
@@ -1296,7 +1305,7 @@ Path_nat_strict_nat = \case { zero -> zeroCase; succ x -> succCase x } where
 pathToEqS_K : {A : Type} {x : A}
            -> (s : {x : A} {y : A} -> Path x y -> Eq_s x y)
            -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p
-pathToEqS_K {A} {x} p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop where
+pathToEqS_K p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop where
   psloop : P (strictEq_pathEq (p_to_s loop))
   psloop = K_s (\l -> P (strictEq_pathEq {A} {x} {x} l)) pr (p_to_s {x} {x} loop)
 
@@ -1306,7 +1315,7 @@ 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 = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) where
+pathToEq_isSet 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
     uipRefl : (x : A) (p : Path x x) -> Path refl p
@@ -1334,34 +1343,33 @@ equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B)
 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) -> p.2 (u itIs1) i ]) (inS p.1)
+contr p u = primComp (\i -> A) (\i [ (phi = i1) -> p.2 (u itIs1) 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
+contr' 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)
+leftIsOne 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)
+rightIsOne 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)
+bothAreOne p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p)
 
 S1Map_to_baseLoop : {X : Type} -> (S1 -> X) -> (a : X) * Path a a
-S1Map_to_baseLoop {X} f = (f base, \i -> f (loop i))
+S1Map_to_baseLoop f = (f base, \i -> f (loop i))
 
-baseLoop_to_S1Map : {X : Type} -> ((a : X) * Path a a) -> S1 -> X
-baseLoop_to_S1Map {X} p = \case
-  base -> p.1
-  loop i -> p.2 i
 
 S1_univ : {X : Type} -> Path (S1 -> X) ((a : X) * Path a a)
-S1_univ = IsoToId {S1 -> X} {(a : X) * Path a a} (S1Map_to_baseLoop, baseLoop_to_S1Map, ret, sec) where
+S1_univ = IsoToId {S1 -> X} {(a : X) * Path a a} (S1Map_to_baseLoop, fro, ret, sec) where
   to = S1Map_to_baseLoop
-  fro = baseLoop_to_S1Map
+  fro : {X : Type} -> ((a : X) * Path a a) -> S1 -> X
+  fro p = \case
+    base -> p.1
+    loop i -> p.2 i
 
   sec : {X : Type} -> (f : S1 -> X) -> Path (fro (to f)) f
   sec {X} f = funext {S1} {\s -> X} {\x -> fro (to f) x} {f} h where
@@ -1386,7 +1394,7 @@ encodeDecode code c0 decode encDec based = IsoToId (encode {a0}, decode _, encDe
   encode alpha = transp (\i -> code (alpha i)) c0
 
   encodeRefl : Path (encode refl) c0
-  encodeRefl = sym (transpFill {\i -> code a0} c0)
+  encodeRefl = sym (transpFill (\i -> code a0) c0)
 
   decEnc : {x : A} (p : Path a0 x) -> Path (decode _ (encode p)) p
   decEnc p = J (\x p -> Path (decode _ (encode p)) p) q p where
@@ -1402,7 +1410,7 @@ S1_elim P pb pq = \case
   loop i -> pq i
 
 PathP_is_Path : (P : I -> Type) (p : P i0) (q : P i1) -> Path (PathP P p q) (Path {P i1} (transp (\i -> P i) p) q)
-PathP_is_Path P p q i = PathP (\j -> P (ior i j)) (transpFill {\j -> P j} p i) q
+PathP_is_Path P p q i = PathP (\j -> P (ior i j)) (transpFill (\j -> P j) p i) q
 
 Constant : {A : Type} {B : Type} -> (A -> B) -> Type
 Constant f = (y : B) * (x : A) -> Path y (f x)
@@ -1417,7 +1425,7 @@ Constant_weakly : {A : Type} {B : Type} (f : A -> B) -> Constant f -> Weakly f
 Constant_weakly f p x y = trans (sym (p.2 x)) (p.2 y)
 
 Constant_conditionally : {A : Type} {B : Type} -> (f : A -> B) -> Constant f -> Conditionally f
-Constant_conditionally {A} {B} f p = transp (\i -> Conditionally (c_const (inot i))) (const_c p.1) where
+Constant_conditionally f p = transp (\i -> Conditionally (c_const (inot i))) (const_c p.1) where
   c_const : Path f (\y -> p.1)
   c_const i x = p.2 x (inot i)
 
@@ -1441,7 +1449,7 @@ S1_connected f = (f'.1, p) where
               (Bool_isSet _ _ rr (transp (\i -> P (loop i)) rr))
 
 isProp_isEquiv : {A : Type} {B : Type} {f : A -> B} -> isProp (isEquiv f)
-isProp_isEquiv {f} p q i y =
+isProp_isEquiv p q i y =
   let
     p2 = (p y).2
     q2 = (q y).2
@@ -1462,10 +1470,10 @@ isProp_EqvSq x y = sigmaPath x1_is_y1 (isProp_isEquiv {P} {Sq P} {y.1} (transp (
 equivLemma : {A : Type} {B : Type} {e : Equiv A B} {e' : Equiv A B}
           -> Path e.1 e'.1
           -> Path e e'
-equivLemma {A} {B} {e} {e'} p = sigmaPath p (isProp_isEquiv {A} {B} {e'.1} (transp (\i -> isEquiv (p i)) e.2) e'.2)
+equivLemma p = sigmaPath p (isProp_isEquiv {A} {B} {e'.1} (transp (\i -> isEquiv (p i)) e.2) e'.2)
 
 isProp_to_Sq_equiv : {P : Type} -> isProp P -> Equiv P (Sq P)
-isProp_to_Sq_equiv {P} prop = propExt prop sqProp inc proj where
+isProp_to_Sq_equiv prop = propExt prop sqProp inc proj where
   proj : Sq P -> P
   proj = Sq_rec prop (\x -> x)
 
@@ -1476,69 +1484,58 @@ Sq_equiv_to_isProp : {P : Type} -> Equiv P (Sq P) -> isProp P
 Sq_equiv_to_isProp eqv = transp (\i -> isProp (ua eqv (inot i))) (\x y i -> sq 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
+exercise_3_21 = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp
 
 uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (ua {A} {B}) (idToEquiv {A} {B})
 uaret eqv = equivLemma (uaBeta eqv)
 
-f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B
-f1 {A} p = (p.1, ua p.2)
-
-f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B
-f2 {A} p = (p.1, idToEquiv p.2)
-
-uaretSig : {A : Type} (a : (B : Type) * Equiv A B) -> Path (f2 (f1 a)) a
-uaretSig {A} p = sigmaPath (\i -> p.1) (uaret {A} {p.1} p.2)
-
 isContrRetract : {A : Type} {B : Type}
               -> (f : A -> B) -> (g : B -> A)
               -> (h : retract f g)
               -> isContr B -> isContr A
-isContrRetract {A} {B} f g h v = (g b, p) where
+isContrRetract 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)))
 
+contrEquivSingl : {A : Type} -> isContr ((B : Type) * Equiv A B)
+contrEquivSingl = isContrRetract f1 f2 uaretSig singContr where
+  f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B
+  f1 p = (p.1, ua p.2)
+
+  f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B
+  f2 p = (p.1, idToEquiv p.2)
+
+  uaretSig : {A : Type} (a : (B : Type) * Equiv A B) -> Path (f2 (f1 a)) a
+  uaretSig {A} p = sigmaPath (\i -> p.1) (uaret {A} {p.1} p.2)
+
 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
+curry = 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)
 
-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
+contrToProp : {A : Type} -> (A -> isContr A) -> isProp A
+contrToProp cont x y = trans (sym (p.2 x)) (p.2 y) where
+  p = cont x
 
+ContractibleIfInhabited : {A : Type} -> isEquiv contrToProp
+ContractibleIfInhabited = (IsoToEquiv (contrToProp, from, toFrom, fromTo)).2 where
   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
+  toFrom : (y : isProp A) -> Path (contrToProp (from y)) y
+  toFrom y = isProp_isProp {A} (contrToProp (from y)) y
 
-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)
+  fromTo : (y : A -> isContr A) -> Path (from (contrToProp y)) y
+  fromTo y i a = isProp_isContr {A} (from (contrToProp y) a) (y a) i
 
 contrSinglEquiv : {B : Type} -> isContr ((A : Type) * Equiv A B)
-contrSinglEquiv {B} = (center, contract) where
+contrSinglEquiv = (center, contract) where
   center : (A : Type) * Equiv A B
   center = (B, idEquiv)
 
@@ -1564,51 +1561,75 @@ contrSinglEquiv {B} = (center, contract) where
           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)
+                          (inS (hcomp (\k [ (i = i0) -> v.2 (iand j k)
+                                          , (i = i1) -> ((w.2.2 b).2 v j).2 k
+                                          , (j = i0) -> fill (\j -> B)
+                                                          {ior i (inot i)}
+                                                          (\k [ (i = i0) -> b
+                                                              , (i = i1) -> (w.2.2 b).1.2 k ])
+                                                          (inS {B} {ior i (inot i)} b) k
+                                          , (j = i1) -> v.2 k
+                                          ])
+                                      (inS b)))
+                      , hfill (\k [ (i = i0) -> v.2 (iand j k)
+                                  , (i = i1) -> ((w.2.2 b).2 v j).2 k
+                                  , (j = i0) -> fill (\j -> B)
+                                                 {ior i (inot i)}
+                                                 (\k [ (i = i0) -> b
+                                                     , (i = i1) -> (w.2.2 b).1.2 k ])
+                                                 (inS {B} {ior i (inot i)} b) k
+                                  , (j = i1) -> v.2 k
+                                  ])
+                              (inS b)
                       )
         in (ctr, contr)
     in (GlueB, unglueB, unglueEquiv)
 
 uaIdEquiv : {A : Type} -> Path (ua idEquiv) (\i -> A)
-uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, idEquiv))
+uaIdEquiv i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, idEquiv))
 
 EquivJ : (P : (X : Type) (Y : Type) -> Equiv X Y -> Type)
       -> ((X : Type) -> P X X idEquiv)
       -> {X : Type} {Y : Type} (E : Equiv X Y)
       -> P X Y E
-EquivJ P p {X} {Y} E =
+EquivJ P p E =
   subst {(X : Type) * Equiv X Y}
         (\x -> P x.1 Y x.2)
         (\i -> isContr_isProp contrSinglEquiv (Y, idEquiv) (X, E) i)
         (p Y)
 
+EquivJ_domain : {Y : Type} (P : (X : Type) -> Equiv X Y -> Type)
+             -> P Y idEquiv
+             -> {X : Type} (E : Equiv X Y)
+             -> P X E
+EquivJ_domain P p E = subst {(X : Type) * Equiv X Y} (\x -> P x.1 x.2) q p where
+  q : Path {(X : Type) * Equiv X Y} (Y, idEquiv) (X, E)
+  q = isContr_isProp contrSinglEquiv (Y, idEquiv) (X, E)
+
+EquivJ_range : {X : Type} (P : (Y : Type) -> Equiv X Y -> Type)
+            -> P X idEquiv
+            -> {Y : Type} (E : Equiv X Y)
+            -> P Y E
+EquivJ_range P p E = subst {(Y : Type) * Equiv X Y} (\x -> P x.1 x.2) q p
+  where
+    q : Path {(Y : Type) * Equiv X Y} (X, idEquiv) (Y, E)
+    q = isContr_isProp {(Y : Type) * Equiv X Y} (contrEquivSingl {X}) (X, idEquiv) (Y, E)
+
 pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
-pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) idEquiv
+pathToEquiv = J {Type} {A} (\B p -> Equiv A B) idEquiv
 
 univalence : {A : Type} {B : Type} -> Equiv (Path A B) (Equiv A B)
 univalence = IsoToEquiv (pathToEquiv, ua, pathToEquiv_ua, ua_pathToEquiv) where
   pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) idEquiv
-  pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) idEquiv
+  pathToEquiv_refl = JRefl (\B p -> Equiv A B) idEquiv
 
   ua_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (ua (pathToEquiv p)) p
-  ua_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (ua {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where
+  ua_pathToEquiv p = J {Type} {A} (\B p -> Path (ua {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where
     lemma : Path (ua (pathToEquiv (\i -> A))) (\i -> A)
     lemma = transp (\i -> Path (ua (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv
 
   pathToEquiv_ua : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (ua p)) p
-  pathToEquiv_ua {A} {B} p = EquivJ (\A B e -> Path (pathToEquiv (ua e)) e) lemma p where
+  pathToEquiv_ua p = EquivJ (\A B e -> Path (pathToEquiv (ua e)) e) lemma p where
     lemma : (A : Type) -> Path (pathToEquiv (ua idEquiv)) idEquiv
     lemma A = transp (\i -> Path (pathToEquiv (uaIdEquiv {A} (inot i))) idEquiv) pathToEquiv_refl
 
@@ -1621,19 +1642,18 @@ total_fibers : {A : Type} {P : A -> Type} {Q : A -> Type}
             -> {xv : (a : A) * Q a}
             -> (f : (el : A) -> P el -> Q el)
             -> Iso (fiber (total f) xv) (fiber (f xv.1) xv.2)
-total_fibers {A} {P} {Q} {xv} f = (to, fro, toFro {xv}, froTo) where
+total_fibers f = (to, fro, toFro {xv}, froTo) where
   to : {xv : (a : A) * Q a} -> fiber (total f) xv -> fiber (f xv.1) xv.2
-  to peq = J {(a : A) * Q a} {_} (\xv eq -> fiber (f xv.1) xv.2) (peq.1.2, refl) (sym peq.2)
+  to peq = J {(a : A) * Q a} (\xv eq -> fiber (f xv.1) xv.2) (peq.1.2, refl) (sym peq.2)
 
   fro : {xv : (a : A) * Q a} -> fiber (f xv.1) xv.2 -> fiber (total f) xv
   fro peq = ((xv.1, peq.1), \i -> (_, peq.2 i))
 
   toFro : {xv : (a : A) * Q a} -> (y : fiber (f xv.1) xv.2) -> Path (to (fro y)) y
-  toFro {xv} peq =
-    J {Q xv.1} {f xv.1 p}
+  toFro peq =
+    J {_} {f xv.1 p}
       (\xv1 eq1 -> Path (to {(xv.1, xv1)} (fro (p, sym eq1))) (p, sym eq1))
-      (JRefl {(a : A) * Q a} {(xv.1, f xv.1 peq.1)}
-        (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl))
+      (JRefl {(a : A) * Q a} {(_, _)} (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl))
       (sym eq)
     where p : P xv.1
           p = peq.1
@@ -1642,9 +1662,9 @@ total_fibers {A} {P} {Q} {xv} f = (to, fro, toFro {xv}, froTo) where
           eq = peq.2
 
   froTo : {xv : (a : A) * Q a} -> (y : fiber (total f) xv) -> Path (fro {xv} (to {xv} y)) y
-  froTo {xv} apeq =
+  froTo apeq =
     J {(a : A) * Q a} {total f (a, p)}
-      (\xv1 eq1 -> Path (fro {_} (to {_} ((a, p), sym eq1))) ((a, p), sym eq1))
+      (\xv1 eq1 -> Path (fro (to ((a, p), sym eq1))) ((a, p), sym eq1))
       (ap fro (JRefl {(a : A) * Q a} {(a, _)}
                 (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl)))
       (sym eq)
@@ -1669,22 +1689,162 @@ totalEquiv : {A : Type} {P : A -> Type} {Q : A -> Type}
           -> (f : (el : A) -> P el -> Q el)
           -> ((x : A) -> isEquiv (f x))
           -> isEquiv (total f)
-totalEquiv f iseqv xv = isContrRetract {fiber (total f) xv} {fiber (f xv.1) xv.2} eqv.1 eqv.2.1 eqv.2.2.2 (iseqv xv.1 xv.2) where
+totalEquiv f iseqv xv = isContrRetract eqv.1 eqv.2.1 eqv.2.2.2 (iseqv xv.1 xv.2) where
   eqv : Iso (fiber (total f) xv) (fiber (f xv.1) xv.2)
   eqv = total_fibers f
 
 contrIsEquiv : {A : Type} {B : Type} -> isContr A -> isContr B
             -> (f : A -> B) -> isEquiv f
-contrIsEquiv cA cB f y = ((cA.1, isContr_isProp cB _ _), \v -> sigmaPath (isContr_isProp cA _ _) (isProp_isSet (isContr_isProp cB) _ _ _ v.2))
+contrIsEquiv cA cB f y =
+  ( (cA.1, isContr_isProp cB _ _)
+  , \v -> sigmaPath (isContr_isProp cA _ _)
+            (isProp_isSet (isContr_isProp cB) _ _ _ v.2)
+  )
 
 theorem722 : {A : Type} {R : A -> A -> Type}
           -> ((x : A) (y : A) -> isProp (R x y))
           -> ({x : A} -> R x x)
           -> (f : (x : A) (y : A) -> R x y -> Path x y)
           -> {x : A} {y : A} -> isEquiv {R x y} {Path x y} (f x y)
-theorem722 {A} {R} prop rho toId {x} {y} = fiberEquiv {A} {R x} {Path x} (toId x) (totalEquiv x) y where
+theorem722 prop rho toId {x} {y} = fiberEquiv (toId x) (totalEquiv x) y where
   rContr : (x : A) -> isContr ((y : A) * R x y)
   rContr x = ((x, rho {x}), \y -> sigmaPath (toId _ _ y.2) (prop _ _ _ y.2))
 
-  totalEquiv : (x : A) -> isEquiv (total {A} {R x} {Path x} (toId x))
-  totalEquiv x = contrIsEquiv (rContr x) singContr (total {A} {R x} {Path x} (toId x))
\ No newline at end of file
+  totalEquiv : (x : A) -> isEquiv (total (toId x))
+  totalEquiv x = contrIsEquiv (rContr x) singContr (total (toId x))
+
+lemma492 : {A : Type} {B : Type} {X : Type}
+        -> (e : Equiv A B)
+        -> isEquiv {X -> A} {X -> B} (\f x -> e.1 (f x))
+lemma492 =
+  EquivJ (\A B e -> isEquiv {X -> _} {X -> B} (\f x -> e.1 (f x)))
+         (\R -> (idEquiv {X -> R}).2)
+
+twoOutOfThree_1 : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : B -> C}
+               -> isEquiv f
+               -> isEquiv g
+               -> isEquiv (\x -> g (f x))
+twoOutOfThree_1 feq geq =
+  EquivJ_range (\_ g -> isEquiv (\x -> g.1 (f x))) feq (g, geq)
+
+twoOutOfThree_2 : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : B -> C}
+               -> isEquiv f
+               -> isEquiv (\x -> g (f x))
+               -> isEquiv g
+twoOutOfThree_2 feq gofeq =
+  EquivJ_domain (\_ f -> isEquiv (\x -> g (f.1 x)) -> isEquiv g) id (f, feq) gofeq
+
+twoOutOfThree_3 : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : B -> C}
+               -> isEquiv g
+               -> isEquiv (\x -> g (f x))
+               -> isEquiv f
+twoOutOfThree_3 geq gofeq =
+  EquivJ_range (\_ g -> isEquiv (\x -> g.1 (f x)) -> isEquiv f) id (g, geq) gofeq
+
+equivalence_isEmbedding : {A : Type} {B : Type}
+                       -> {f : A -> B}
+                       -> isEquiv f
+                       -> {x : A} {y : A}
+                       -> isEquiv (ap f {x} {y})
+equivalence_isEmbedding feqv {x} {y} =
+  EquivJ (\A B eq -> (x : A) (y : A) -> isEquiv {_} {Path (eq.1 x) (eq.1 y)} (ap eq.1)) (\X x y -> (idEquiv {Path _ _}).2) (f, feqv) x y
+
+isOfHLevel : Type -> Nat -> Type
+isOfHLevel A = \case
+  zero -> (a : A) (b : A) -> Path a b
+  succ n -> (a : A) (b : A) -> isOfHLevel (Path a b) n
+
+Sphere : Nat -> Type
+Sphere = \case
+  zero -> Bottom
+  succ n -> Susp (Sphere n)
+
+sphereFull : {A : Type} {n : Nat} (f : Sphere n -> A) -> Type
+sphereFull f = (top : A) * (x : Sphere n) -> Path top (f x)
+
+spheresFull : {n : Nat} -> Type -> Type
+spheresFull A = (f : Sphere n -> A) -> sphereFull f
+
+spheresFull_hLevel : {A : Type} (n : Nat) -> spheresFull {succ n} A -> isOfHLevel A n
+spheresFull_hLevel =
+  \case
+    zero -> \full a b ->
+      let f : Sphere (succ zero) -> A
+          f = \case
+            north -> a
+            south -> b
+            merid u i -> absurd u
+          p = (full f).2
+      in trans (sym (p north)) (p south)
+    succ n -> \h x y -> spheresFull_hLevel n (helper h x y)
+  where
+    helper : {n : Nat} -> spheresFull {succ (succ n)} A -> (x : A) (y : A) -> spheresFull {succ n} (Path x y)
+    helper h x y f = (trans p q, r (transFiller p q)) where
+      f' : Susp (Sphere (succ n)) -> A
+      f' = \case
+        north -> x
+        south -> y
+        merid u i -> f u i
+
+      p : Path x (h f').1
+      p i = (h f').2 north (inot i)
+
+      q : Path (h f').1 y
+      q = (h f').2 south
+
+      r : (fillpq : PathP (\i -> Path x (q i)) p (trans p q))
+          (s : Sphere (succ n))
+       -> Path (fillpq i1) (f s)
+      r fillpq s i j = hcomp (\k [ (i = i0) -> fillpq k j
+                                 , (i = i1) -> (h f').2 (merid s j) k
+                                 , (j = i0) -> p (iand (inot k) i)
+                                 , (j = i1) -> q k ])
+                             (inS (p (ior i j)))
+
+isOfHLevel_hasSpheres : {A : Type} (n : Nat) -> isOfHLevel A n -> spheresFull {succ n} A
+isOfHLevel_hasSpheres =
+  \case
+    zero -> \prop f -> (f north, \x -> prop (f north) (f x))
+    succ n -> \h -> helper {n} (\x y -> isOfHLevel_hasSpheres n (h x y))
+  where
+    helper : {n : Nat} -> ((a : A) (b : A) -> spheresFull {succ n} (Path a b))
+                       -> spheresFull {succ (succ n)} A
+    helper {n} h f = (f north, r) where
+      north' = north {Sphere (succ n)}
+      south' = south {Sphere (succ n)}
+      merid' = merid {Sphere (succ n)}
+
+      r : (x : Sphere (succ (succ n))) -> Path (f north) (f x)
+      r = \case
+        north -> refl
+        south -> (h (f north') (f south') (\x i -> f (merid x i))).1
+        merid x i -> \j ->
+          hcomp (\k [ (i = i0) -> f north'
+                    , (i = i1) -> (h (f north') (f south') (\x i -> f (merid' x i))).2 x (inot k) j
+                    , (j = i0) -> f north'
+                    , (j = i1) -> f (merid' x i) ])
+                (inS (f (merid' x (iand i j))))
+
+data nTrunc (A : Type) (n : Nat) : Type where
+  incn : A -> nTrunc A n
+  hub  : (f : Sphere (succ n) -> nTrunc A n) -> nTrunc A n
+  spoke i : (f : Sphere (succ n) -> nTrunc A n) (x : Sphere (succ n)) -> nTrunc A n [ (i = i0) -> hub f, (i = i1) -> f x ]
+
+nTrunc_isOfHLevel : {A : Type} {n : Nat} -> isOfHLevel (nTrunc A n) n
+nTrunc_isOfHLevel = spheresFull_hLevel {nTrunc A n} n (\f -> (hub f, \x i -> spoke f x i))
+
+nTrunc_rec : {A : Type} {n : Nat} {B : Type}
+          -> isOfHLevel B n
+          -> (A -> B)
+          -> nTrunc A n -> B
+nTrunc_rec bofhl f = go (isOfHLevel_hasSpheres n bofhl) where
+  work : (p : spheresFull {succ n} B) -> nTrunc A n -> B
+  work p = \case
+    hub sph -> (p (\x -> work p (sph x))).1
+    incn x -> f x
+
+  go : (p : spheresFull {succ n} B) -> nTrunc A n -> B
+  go p = \case
+    incn x -> f x
+    hub sph -> (p (\x -> work p (sph x))).1
+    spoke sph cell i -> (p (\x -> work p (sph x))).2 cell i
\ No newline at end of file
diff --git a/src/Debug.hs b/src/Debug.hs
index 295751c..8d5190b 100644
--- a/src/Debug.hs
+++ b/src/Debug.hs
@@ -1,18 +1,20 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE BangPatterns #-}
+#undef RELEASE
 module Debug where
 
 import qualified Debug.Trace as D
 
 #if defined(RELEASE)
 import GHC.Exts
-#else
+#endif
+
 import GHC.Stack
 import Prettyprinter
 import qualified Data.Text.Lazy as T
 import Data.Text.Prettyprint.Doc.Render.Text (renderLazy)
-#endif
 
 traceDoc :: Doc a -> b -> b
 
diff --git a/src/Elab.hs b/src/Elab.hs
index 0f79805..e7692f7 100644
--- a/src/Elab.hs
+++ b/src/Elab.hs
@@ -33,7 +33,6 @@ import Prettyprinter
 
 import Syntax.Pretty
 import Syntax
-import Debug (traceM, traceDocM)
 
 infer :: P.Expr -> ElabM (Term, NFType)
 infer (P.Span ex a b) = withSpan a b $ infer ex
@@ -146,47 +145,36 @@ check (P.Let items body) ty = do
 
 check (P.LamSystem bs) ty = do
   (extent, dom) <- isPartialType ty
-  eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
+  env <- ask
+  eqns <- for bs \(formula, rhs) -> do
     (phi, fv) <- checkFormula formula
-    env <- ask
     n <- newName
     rhses <- for (truthAssignments phi (getEnv env)) $ \e -> do
       let env' = env{ getEnv = e }
       local (const env') $
-        (Nothing,) <$> check rhs (substitute (snd <$> Map.restrictKeys e fv) (dom (VVar n)))
+        check rhs (substitute (snd <$> Map.restrictKeys e fv) (dom (VVar n)))
     pure (n, (phi, head rhses))
 
   unify extent (foldl ior VI0 (map (fst . snd) eqns))
 
-  for_ eqns $ \(n, (formula, (binding, rhs))) -> do
-    let
-      k = case binding of
-        Just v -> assume v (VEqStrict VI formula VI1) . const
-        Nothing -> id
-    k $ for_ eqns $ \(n', (formula', (binding, rhs'))) -> do
+  for_ eqns \(n, (formula, rhs)) -> do
+    for_ eqns $ \(n', (formula', rhs')) -> do
       let
-        k = case binding of
-          Just v -> assume v (VEqStrict VI formula VI1) . const
-          Nothing -> id
         truth = possible mempty (iand formula formula')
-        add [] = id
-        add ((~(HVar x), True):xs) = redefine x VI VI1 . add xs
-        add ((~(HVar x), False):xs) = redefine x VI VI0 . add xs
-      k $ when ((n /= n') && fst truth) . add (Map.toList (snd truth)) $ do
-        vl <- eval rhs
-        vl' <- eval rhs'
+
+      when ((n /= n') && fst truth) . for_ (truthAssignments (iand formula formula') (getEnv env)) $ \e -> do
+        let env' = env { getEnv = e }
+            vl = eval' env' rhs
+            vl' = eval' env' rhs'
         unify vl vl'
           `withNote` vsep [ pretty "These two cases must agree because they are both possible:"
-                          , indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm rhs
-                          , indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> prettyTm rhs'
+                          , indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> pretty vl
+                          , indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> pretty (zonk vl')
                           ]
           `withNote` (pretty "Consider this face, where both are true:" <+> showFace False (snd truth))
 
   name <- newName
-  let
-    mkB name (Just v, b) = App P.Ex (Lam P.Ex v b) (Ref name)
-    mkB _ (Nothing, b) = b
-  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, mkB name y)) eqns))))
+  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, y)) eqns))))
 
 check (P.LamCase pats) ty =
   do
@@ -510,7 +498,7 @@ checkStatement (P.ReplNf e) k = do
 checkStatement (P.ReplTy e) k = do
   (t, ty) <- infer e
   h <- asks commHook
-  liftIO (h (prettyTm t <+> colon <+> align (prettyVl ty)))
+  liftIO (h (prettyTm t <+> colon <+> align (prettyVl (zonk ty))))
   k
 
 checkStatement (P.Data name tele retk constrs) k =
diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs
index 9666b2f..08bdd98 100644
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@@ -36,6 +36,8 @@ import Syntax
 import System.IO.Unsafe ( unsafePerformIO )
 
 import {-# SOURCE #-} Elab.WiredIn
+import Debug (traceM, traceDocM)
+import Prettyprinter (pretty, (<+>))
 
 eval :: HasCallStack => Term -> ElabM Value
 eval t = asks (flip eval' t)
@@ -214,37 +216,51 @@ evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
   | x == x'   = foldl applProj (eval' env k) sp
   | otherwise = evalCase env rng val xs
 
+evalCase _ _ (VVar ((== trueCaseSentinel) -> True)) _ = VI1
+
 evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs
 
+-- This is a great big HACK; When we see a system [ case x of ... => p
+-- ], we somehow need to make the 'case x of ...' become VI1. The way we
+-- do this is by substituting x/trueCaseSentinel in truthAssignments,
+-- and then making case trueCaseSentinel of ... => VI1 always.
+trueCaseSentinel :: Name
+trueCaseSentinel = Bound (T.pack "sentinel for true cases") (-1000)
+
 evalFix' :: HasCallStack => ElabEnv -> Name -> NFType -> Term -> Value
 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
   t <- ask
-  pure (evalFix' t name nft term)
+  pure (evalFix' t name (GluedVl (HVar name) mempty nft) term)
 
 data NotEqual = NotEqual Value Value
   deriving (Show, Typeable, Exception)
 
-unify' :: HasCallStack => Value -> Value -> ElabM ()
-unify' (GluedVl h sp a) (GluedVl h' sp' b)
+unify' :: HasCallStack => Bool -> Value -> Value -> ElabM ()
+
+unify' cs topa@(GluedVl h sp a) topb@(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
+    traverse_ (uncurry (unify'Spine cs topa topb)) (Seq.zip sp sp')
+      `catchElab` \(_ :: SomeException) -> unify' cs a b
+
+unify' canSwitch 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
 
-  go (VNe (HPCon _ _ x) sp) (VNe (HPCon _ _ y) sp')
-    | x == y = traverse_ (uncurry unify'Spine) (Seq.zip sp sp')
+  go topa@(VNe (HPCon _ _ x) sp) topb@(VNe (HPCon _ _ y) sp')
+    | x == y = traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip sp sp')
+
   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 _ _ b) (VCase e' _ _ b') = do
     env <- ask
     let
-      go (_, _, a) (_, _, b) = unify' (eval' env{getEnv=moreDefinedFrom e e' <$> e} a) (eval' env{getEnv=moreDefinedFrom e e' <$> e'} b)
+      go (_, _, a) (_, _, b)
+        | a == b = pure ()
+        | otherwise = unify' canSwitch (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
@@ -253,33 +269,33 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
       go (_, n, a') = do
         ns <- replicateM n (VVar <$> newName)
         let a = foldl (vApp Ex) (eval' env{getEnv=e} a') ns
-        unify' a y
+        unify' canSwitch a y
     traverse_ go b
 
-  go (VNe x a) (VNe x' a')
+  go topa@(VNe x a) topb@(VNe x' a')
     | x == x', length a == length a' =
-      traverse_ (uncurry unify'Spine) (Seq.zip a a')
+      traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip a a')
 
   go (VLam p (Closure n k)) vl = do
     t <- VVar <$> newName' n
-    unify' (k t) (vApp p vl t)
+    unify' canSwitch (k t) (vApp p vl t)
 
   go vl (VLam p (Closure n k)) = do
     t <- VVar <$> newName' n
-    unify' (vApp p vl t) (k t)
+    unify' canSwitch (vApp p vl t) (k t)
 
-  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 (VPair a b) vl = unify' canSwitch a (vProj1 vl) *> unify' canSwitch b (vProj2 vl)
+  go vl (VPair a b) = unify' canSwitch (vProj1 vl) a *> unify' canSwitch (vProj2 vl) b
 
   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)
+    unify' canSwitch d d'
+    unify' canSwitch (k t) (k' t)
 
   go (VSigma d (Closure n k)) (VSigma d' (Closure _ k')) = do
     t <- VVar <$> newName' n
-    unify' d d'
-    unify' (k t) (k' t)
+    unify' canSwitch d d'
+    unify' canSwitch (k t) (k' t)
 
   go VType VType   = pure ()
   go VTypeω VTypeω = pure ()
@@ -287,56 +303,63 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go VI VI   = pure ()
 
   go (VPath l x y) (VPath l' x' y') = do
-    unify' l l'
-    unify' x x'
-    unify' y y'
+    unify' canSwitch l l'
+    unify' canSwitch x x'
+    unify' canSwitch y y'
 
   go (VLine l x y p) p' = do
     n <- VVar <$> newName' (Bound (T.singleton 'i') (- 1))
-    unify' (p @@ n) (ielim l x y p' n)
+    unify' canSwitch (p @@ n) (ielim l x y p' n)
 
   go p' (VLine l x y p) = do
     n <- VVar <$> newName
-    unify' (ielim l x y p' n) (p @@ n)
+    unify' canSwitch (ielim l x y p' n) (p @@ n)
 
-  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'
+  go (VPartial phi r) (VPartial phi' r')   = unify' canSwitch phi phi' *> unify' canSwitch r r'
+  go (VPartialP phi r) (VPartialP phi' r') = unify' canSwitch phi phi' *> unify' canSwitch r r'
 
-  go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
-  go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
+  go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u')]
+  go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u')]
 
   go (VComp a phi u a0) (VComp a' phi' u' a0') =
-    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+    traverse_ (uncurry (unify' canSwitch)) [(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')]
+    traverse_ (uncurry (unify' canSwitch)) [(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)
+  go (VGlueTy _ (force -> VI1) u _0) rhs = unify' canSwitch (u @@ VReflStrict VI VI1) rhs
+  go lhs (VGlueTy _ (force -> VI1) u _0) = unify' canSwitch 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')]
+    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
 
   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')]
+    traverse_ (uncurry (unify' canSwitch)) [(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')]
+    traverse_ (uncurry (unify' canSwitch)) [(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 (VSystem sys) rhs = goSystem (unify' canSwitch) sys rhs
+  go rhs (VSystem sys) = goSystem (flip (unify' canSwitch)) 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 (VEqStrict a x y) (VEqStrict a' x' y') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (x, x'), (y, y')]
+  go (VReflStrict a x) (VReflStrict a' x') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (x, x')]
   go _ VReflStrict{} = pure ()
   go VReflStrict{} _ = pure ()
 
-  go x y
-    | x == y = pure ()
-    | otherwise =
-      case (toDnf x, toDnf y) of
-        (Just xs, Just ys) -> unify'Formula xs ys
-        _ -> fail
+  go (VINot x) (VINot y) = unify' canSwitch x y
+
+  go x y =
+    case (toDnf x, toDnf y) of
+      (Just xs, Just ys) -> unify'Formula xs ys
+      _ ->
+        if canSwitch
+          then goDumb x y
+          else fail
+
+  goDumb (VIOr a b) (VIOr a' b') = unify' canSwitch a a' *> goDumb b b'
+  goDumb (VIAnd a b) (VIAnd a' b') = unify' canSwitch a a' *> goDumb b b'
+  goDumb x y = switch $ unify' False x y
 
   goSystem :: (Value -> Value -> ElabM ()) -> Map.Map Value Value -> Value -> ElabM ()
   goSystem k sys rhs = do
@@ -348,7 +371,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
         k (eval' env{getEnv = e} i_q) (eval' env{getEnv = e} rhs_q)
 
   fail = throwElab $ NotEqual topa topb
-
   unify'Formula x y
     | compareDNFs x y = pure ()
     | otherwise = fail
@@ -371,31 +393,32 @@ trivialSystem = go . force where
   go VSystem{} = Nothing
   go x = Just x
 
-unify'Spine :: Projection -> Projection -> ElabM ()
-unify'Spine (PApp a v) (PApp a' v')
-  | a == a' = unify' v v'
+unify'Spine :: Bool -> Value -> Value -> Projection -> Projection -> ElabM ()
+unify'Spine cs _ _ (PApp a v) (PApp a' v')
+  | a == a' = unify' cs v v'
 
-unify'Spine PProj1 PProj1 = pure ()
-unify'Spine PProj2 PProj2 = pure ()
+unify'Spine _ _ _ PProj1 PProj1 = pure ()
+unify'Spine _ _ _ PProj2 PProj2 = pure ()
 
-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 cs _ _ (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' cs i j
+unify'Spine cs _ _ (POuc a phi u) (POuc a' phi' u') =
+  traverse_ (uncurry (unify' cs)) [(a, a'), (phi, phi'), (u, u')]
 
-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 cs _ _ (PK a x p pr) (PK a' x' p' pr') =
+  traverse_ (uncurry (unify' cs)) [(a, a'), (x, x'), (p, p'), (pr, pr')]
 
-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 cs _ _ (PJ a x p pr y) (PJ a' x' p' pr' y') =
+  traverse_ (uncurry (unify' cs)) [(a, a'), (x, x'), (p, p'), (pr, pr'), (y, y')]
 
-unify'Spine _ _ = throwElab (NotEqual undefined undefined)
+unify'Spine _ x y _ _ = throwElab (NotEqual x y)
 
 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 a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
+unify x y = shallowly $ go x y where
+  go topa@(GluedVl h sp a) topb@(GluedVl h' sp' b)
+    | h == h', length sp == length sp' =
+      traverse_ (uncurry (unify'Spine True topa topb)) (Seq.zip sp sp')
+        `catchElab` \(_ :: SomeException) -> unify' True a b
+  go a b = unify' True a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
 
 isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
 isConvertibleTo a b = isConvertibleTo (force a) (force b) where
@@ -420,7 +443,7 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where
     pure (\f -> Lam Ex nm (wp (IElim (quote a) (quote x) (quote y) f (Ref nm))))
 
   isConvertibleTo a b = do
-    unify' a b
+    unify' True a b
     pure id
 
 newMeta' :: Bool -> Value -> ElabM Value
@@ -495,7 +518,7 @@ checkScope mv scope (VNe h sp) =
     case h of
       HVar v@Bound{} ->
         unless (v `Set.member` scope) . throwElab $
-          NotInScope v
+          ScopeCheckingFail v
       HVar{} -> pure ()
       HCon{} -> pure ()
       HPCon{} -> pure ()
@@ -566,7 +589,10 @@ checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
 checkSpine _     (p Seq.:<| _) = throwElab $ SpineProj p
 checkSpine _     Seq.Empty = pure []
 
-data MetaException = NonLinearSpine { getDupeName :: Name } | SpineProj { getSpineProjection :: Projection } | CircularSolution { getCycle :: MV }
+data MetaException = NonLinearSpine { getDupeName :: Name }
+                   | SpineProj { getSpineProjection :: Projection } 
+                   | CircularSolution { getCycle :: MV }
+                   | ScopeCheckingFail { outOfScope :: Name }
   deriving (Show, Typeable, Exception)
 
 substituteIO :: Map.Map Name Value -> Value -> IO Value
@@ -582,7 +608,7 @@ substituteIO sub = substituteIO . force where
       HVar v ->
         case Map.lookup v sub of
           Just vl -> substituteIO $ foldl applProj vl sp'
-          Nothing -> pure $ VNe hd sp'
+          Nothing -> pure $ foldl applProj (VNe hd mempty) sp'
       hd -> pure $ VNe hd sp'
 
   substituteIO (GluedVl h sp vl) = GluedVl h <$> traverse (substituteSp sub) sp <*> substituteIO vl
diff --git a/src/Elab/Eval/Formula.hs b/src/Elab/Eval/Formula.hs
index e50c69e..b4ea30f 100644
--- a/src/Elab/Eval/Formula.hs
+++ b/src/Elab/Eval/Formula.hs
@@ -9,7 +9,7 @@ import Data.Set (Set)
 import Syntax
 
 import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
-import Elab.Eval (substitute)
+import Elab.Eval (substitute, trueCaseSentinel)
 
 toDnf :: Value -> Maybe Value
 toDnf = fmap (dnf2Val . normalise) . val2Dnf where
@@ -77,7 +77,8 @@ 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) (sub x VI1 <$> m))
-truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) m)
+truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) (sub x VI0 <$> m))
+truthAssignments (VCase _ _ (VNe (HVar x) _) _) m = pure (Map.insert x (VI, VVar trueCaseSentinel) m)
 truthAssignments _ m = pure m
 
 sub :: Name -> Value -> (NFType, NFEndp) -> (Value, Value)
diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs
index 539b10b..3e12d21 100644
--- a/src/Elab/Monad.hs
+++ b/src/Elab/Monad.hs
@@ -137,10 +137,13 @@ switch :: ElabM a -> ElabM a
 switch k =
   do
     depth <- asks pingPong
-    when (depth >= 128) $ throwElab StackOverflow
+    when (depth >= 128) $ error "stack overflow"
     local go k
   where go e = e { pingPong = pingPong e + 1 }
 
+shallowly :: ElabM a -> ElabM a
+shallowly = local (\e -> e { pingPong = 0 })
+
 newtype NotInScope = NotInScope { nameNotInScope :: Name }
   deriving          (Show, Typeable)
   deriving anyclass (Exception)
diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs
index 51bef9e..4bb03bc 100644
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@@ -7,7 +7,31 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE KindSignatures #-}
-module Elab.WiredIn where
+module Elab.WiredIn
+       ( wiType
+       , wiValue
+       , wiredInNames
+       , NoSuchPrimitive(..)
+
+       , iand
+       , ior
+       , inot
+       , ielim
+       , incS
+       , outS
+       , comp
+       , fill
+       , hComp
+       , glueType
+       , glueElem
+       , unglue
+       , fun
+       , system
+       , strictK
+       , strictJ
+       , projIntoCase
+       )
+  where
 
 import Control.Exception ( assert, Exception )
 
@@ -31,7 +55,6 @@ import Syntax.Pretty (prettyTm, prettyVl)
 import Syntax
 
 import System.IO.Unsafe
-import Data.Text.Prettyprint.Doc (viaShow)
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -48,6 +71,7 @@ wiType WiPathP    = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
 
 wiType WiPartial  = VI ~> VType ~> VTypeω
 wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
+wiType WiPOr      = forAll VType \a -> dprod VI \phi -> dprod VI \psi -> VPartial phi a ~> VPartial psi a ~> VPartial (ior phi psi) a
 
 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))
@@ -82,6 +106,8 @@ wiValue WiPathP     = functions [(Ex, "A"), (Ex, "x"), (Ex, "y")] \[a, x, y] ->
 
 wiValue WiPartial  = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartial phi a
 wiValue WiPartialP = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartialP phi a
+wiValue WiPOr      = functions [(Im, "A"), (Ex, "phi"), (Ex, "psi"), (Ex, "a"), (Ex, "b")] \[_, phi, psi, a, b] -> mkVSystem (Map.fromList [(phi, a), (psi, b)])
+
 wiValue WiSub      = functions [(Ex, "A"), (Ex, "phi"), (Ex, "u")] \[a, phi, u] -> VSub a phi u
 wiValue WiInS      = functions [(Im, "A"), (Im, "phi"), (Ex, "u")] \[a, phi, u] -> incS a phi u
 wiValue WiOutS     = functions [(Im, "A"), (Im, "phi"), (Im, "u"), (Ex, "u0")] \[a, phi, u, x] -> outS a phi u x
@@ -153,6 +179,7 @@ wiredInNames = Map.fromList
 
   , ("Partial", WiPartial)
   , ("PartialP", WiPartialP)
+  , ("partialExt", WiPOr)
   , ("Sub", WiSub)
   , ("inS", WiInS)
   , ("outS", WiOutS)
@@ -244,7 +271,7 @@ outS a phi u (VSystem fs) = mkVSystem (fmap (outS a phi u) fs)
 outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 
 comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
-comp _a VI1 u _a0 =  u @@ VI1 @@ VReflStrict VI VI1
+comp _a (force -> VI1) u _a0 =  u @@ VI1 @@ VReflStrict VI VI1
 comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
   case force (a @@ VVar name) of
     VPi{} ->
@@ -418,7 +445,7 @@ nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prett
 system :: (Value -> Value -> Value) -> Value
 system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "[i]" 0) \isone -> k i isone
 
-fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
+fill :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
 fill a phi u a0 j =
   comp (line \i -> a @@ (i `iand` j))
        (phi `ior` inot j)
@@ -505,9 +532,6 @@ transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (incS (line
 gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value
 gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (incS (line VI0) VI0 a0)
 
-forward :: (Value -> Value) -> Value -> Value -> Value
-forward line phi a0 = gtrans (\i -> line (ior phi i)) phi a0
-
 transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value
 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))
diff --git a/src/Main.hs b/src/Main.hs
index 5bf505f..347a203 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -66,7 +66,7 @@ evalArgExpr env str =
     Right e ->
       flip runElab env (do
         (e, _) <- infer e
-        liftIO . Lt.putStrLn . render . prettyTm . quote . zonk =<< Elab.Eval.eval e)
+        liftIO . print . prettyTm . quote =<< Elab.Eval.eval e)
       `catch` \e -> do
           displayExceptions' inp (e :: SomeException)
     Left e -> liftIO $ print e
@@ -121,7 +121,7 @@ enterReplIn env =
       newe <- liftIO $ try $ mkrepl <$> checkFiles (reverse loadedFiles)
       case newe of
         Left e -> do
-          liftIO $ displayExceptions' ":r" (e :: SomeException)
+          liftIO $ do displayExceptions' ":r" (e :: SomeException)
           loop env envref
         Right newe -> do
           liftIO $ writeIORef envref newe
@@ -156,7 +156,7 @@ checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
     liftIO . putStrLn $ "[" ++ pad (show n) ++ "/" ++ show size ++ "] Loading " ++ x
     code <- liftIO $ Bsl.readFile x
     case runAlex (code <> Bsl.singleton 10) parseProg of
-      Left e -> liftIO $ print e *> error (show e)
+      Left e -> liftIO (print e) *> k
       Right prog ->
         local (\e -> e { currentFile = Just (T.pack x), loadedFiles = x:loadedFiles e }) (checkProgram prog (go (n + 1 :: Int) xs k))
           `catchElab` \e -> liftIO $ displayAndDie (T.decodeUtf8 (Bsl.toStrict code)) (e :: SomeException)
diff --git a/src/Syntax.hs b/src/Syntax.hs
index ad9c6f5..9af058c 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -31,6 +31,7 @@ data WiredIn
 
   | WiPartial  -- (φ : I) -> Type           -> Typeω
   | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
+  | WiPOr      -- (A : Type) (φ ψ : I) -> Partial φ A -> Partial ψ A -> Partial (ior φ ψ) A
 
   | WiSub      -- (A : Type) (φ : I) -> Partial φ A -> Typeω
   | WiInS      -- {A : Type} {φ : I} (u : A) -> Sub A φ (λ x -> u)
@@ -228,7 +229,7 @@ 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
@@ -321,7 +322,15 @@ data Head
   | HPCon Value Value Name
   | HMeta MV
   | HData Bool Name
-  deriving (Eq, Ord, Show)
+  deriving (Ord, Show)
+
+instance Eq Head where
+  HVar x == HVar y = x == y
+  HCon _ x == HCon _ y = x == y
+  HPCon _ _ x == HPCon _ _ y = x == y
+  HMeta x == HMeta y = x == y
+  HData x y == HData x' y' = x == x' && y == y'
+  _ == _ = False
 
 data Projection
   = PApp   Plicity Value
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index 5a4355b..e16c005 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -102,10 +102,10 @@ prettyTm' implicits = go True 0 where
       I0 -> keyword (pretty "i0")
       I1 -> keyword (pretty "i1")
 
-      IAnd x y -> parenIf (p > and_prec) $
+      IAnd x y -> parenIf (True || p > and_prec) $
         go False and_prec x <+> operator (pretty "/\\") <+> go False and_prec y
 
-      IOr x y -> parenIf (p > or_prec) $
+      IOr x y -> parenIf (True || p > or_prec) $
         go False or_prec x <+> operator (pretty "\\/") <+> go False or_prec y
 
       INot x -> operator (pretty "~") <> go False p x
@@ -213,7 +213,7 @@ printImplicits :: Bool
 #if defined(RELEASE)
 printImplicits = False
 #else
-printImplicits = False
+printImplicits = True
 #endif
 
 render :: Doc AnsiStyle -> Lazy.Text