From 81ed8ae8ae6a8082afa1e24228a41b47effc4bcd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Tue, 6 Apr 2021 08:36:48 -0300
Subject: [PATCH] Add strict equality

---
 Setup.hs                 |   1 -
 intro.tt                 | 328 ++++++++++++++++++++++++++---------
 src/Elab.hs              |  21 ++-
 src/Elab/Eval.hs         |  90 +++++++---
 src/Elab/Eval/Formula.hs |  33 +++-
 src/Elab/Monad.hs        |  27 ++-
 src/Elab/WiredIn.hs      | 112 ++++++++----
 src/Elab/WiredIn.hs-boot |   7 +-
 src/Main.hs              | 112 ++++++++----
 src/Syntax.hs            |  29 +++-
 src/Syntax/Pretty.hs     | 357 +++++++++++++++++++--------------------
 stack.yaml               |  66 +-------
 stack.yaml.lock          |   8 +-
 13 files changed, 738 insertions(+), 453 deletions(-)

diff --git a/Setup.hs b/Setup.hs
index 09e11ce..e8ef27d 100644
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,4 +1,3 @@
-
 import Distribution.Simple
 
 main = defaultMain
diff --git a/intro.tt b/intro.tt
index 6449b74..2b55196 100644
--- a/intro.tt
+++ b/intro.tt
@@ -84,7 +84,7 @@ sym p i = p (inot i)
 id : {A : Type} -> A -> A
 id x = x
 
-the : (A : Type) -> A -> A
+the : (A : Pretype) -> A -> A
 the A x = x
 
 -- The eliminator for the interval says that if you have x : A i0 and y : A i1,
@@ -266,12 +266,12 @@ fill A {phi} u a0 i =
          (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])
          (inS (outS a0))
 
-hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> I -> A
-hfill {A} {phi} u a0 i = fill (\i -> 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} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
+
 -- For instance, the filler of the previous composition square
 -- tells us that trans p refl = p:
 
@@ -296,11 +296,11 @@ transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path
                                  (\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x)))
 transpFun p q f = refl
 
--- transpDFun : {A : I -> Type} {B : (i : I) -> A i -> Type}
---           -> (f : (x : A i0) -> B i0 x) 
---           -> Path (transp (\i -> (x : A i) -> B i x) f)
---                   (\x -> transp (\i -> B i (fill (\j -> A (inot j)) (\k []) (inS x) (inot i))) (f (fill (\j -> A (inot j)) (\k []) (inS x) i1)))
--- transpDFun f = refl
+transpDFun : {A : I -> Type} {B : (i : I) -> A i -> Type}
+          -> (f : (x : A i0) -> B i0 x) 
+          -> Path (transp (\i -> (x : A i) -> B i x) f)
+                  (\x -> transp (\i -> B i (fill (\j -> A (inot j)) (\k []) (inS x) (inot i))) (f (fill (\j -> A (inot j)) (\k []) (inS x) i1)))
+transpDFun f = refl
 
 -- When considering the more general case of a composition respecing sides,
 -- the outer transport becomes a composition.
@@ -628,10 +628,10 @@ notp = univalence (IsoToEquiv (not, involToIso not notInvol))
 
 data bottom : Type where {}
 
-elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b
+elimBottom : (P : bottom -> Pretype) -> (b : bottom) -> P b
 elimBottom P = \case {}
 
-absurd : {P : Type} -> bottom -> P
+absurd : {P : Pretype} -> bottom -> P
 absurd = \case {}
 
 -- We prove that true != false by transporting along the path
@@ -715,6 +715,20 @@ Nat_elim P pz ps = \case
   zero -> pz
   succ x -> ps x (Nat_elim P pz ps x)
 
+zeroNotSucc : {x : Nat} -> Path zero (succ x) -> bottom
+zeroNotSucc p = transp (\i -> fun (p i)) (p i0) where
+  fun : Nat -> Type
+  fun = \case
+    zero -> Nat
+    succ x -> bottom
+
+succInj : {x : Nat} {y : Nat} -> Path (succ x) (succ y) -> Path x y
+succInj p i = pred (p i) where
+  pred : Nat -> Nat
+  pred = \case
+    zero -> zero
+    succ x -> x
+
 -- The type of integers can be defined as A + B, where "pos n" means +n
 -- and "neg n" means -(n + 1).
 
@@ -882,41 +896,40 @@ data Susp (A : Type) : Type where
 data Unit : Type where
   tt : Unit
 
-poSusp : Type -> Type
-poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt)
-
-poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A
-poSusp_to_Susp = \case
-  inl x -> north
-  inr x -> south
-  push x i -> merid x i
-
-Susp_to_poSusp : {A : Type} -> Susp A -> poSusp A
-Susp_to_poSusp = \case
-  north -> inl tt
-  south -> inr tt
-  merid x i -> push x i
-
-Susp_to_poSusp_to_Susp : {A : Type} -> (x : Susp A) -> Path (poSusp_to_Susp (Susp_to_poSusp x)) x
-Susp_to_poSusp_to_Susp = \case
-  north -> refl
-  south -> refl
-  merid x i -> refl
-
 unitEta : (x : Unit) -> Path x tt
 unitEta = \case tt -> refl
 
 unitContr : isContr Unit
 unitContr = (tt, \x -> sym (unitEta x))
 
-poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x
-poSusp_to_Susp_to_poSusp {A} = \case
-  inl x -> cong inl (sym (unitEta x))
-  inr x -> cong inr (sym (unitEta x))
-  push x i -> refl
+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} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A}))
+Susp_is_poSusp {A} = univalence (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
+    inr x -> south
+    push x i -> merid x i
+
+  Susp_to_poSusp : {A : Type} -> Susp A -> poSusp A
+  Susp_to_poSusp = \case
+    north -> inl tt
+    south -> inr tt
+    merid x i -> push x i
+
+  Susp_to_poSusp_to_Susp : {A : Type} -> (x : Susp A) -> Path (poSusp_to_Susp (Susp_to_poSusp x)) x
+  Susp_to_poSusp_to_Susp = \case
+    north -> refl
+    south -> refl
+    merid x i -> refl
+
+  poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x
+  poSusp_to_Susp_to_poSusp {A} = \case
+    inl x -> cong inl (sym (unitEta x))
+    inr x -> cong inr (sym (unitEta x))
+    push x i -> refl
 
 data T2 : Type where
   baseT : T2
@@ -929,41 +942,42 @@ data T2 : Type where
       (i = i1) -> pathOne j
     ]
 
-torusToCircs : T2 -> S1 * S1
-torusToCircs = \case
-  baseT -> (base, base)
-  pathOne i -> (loop i, base)
-  pathTwo i -> (base, loop i)
-  square i j -> (loop i, loop j)
-
-circsToTorus : (S1 * S1) -> T2
-circsToTorus pair = go pair.1 pair.2
-  where
-    baseCase : S1 -> T2
-    baseCase = \case
-      base -> baseT
-      loop j -> pathTwo j
-
-    loopCase : Path baseCase baseCase
-    loopCase i = \case
-      base -> pathOne i
-      loop j -> square i j
-
-    go : S1 -> S1 -> T2
-    go = \case
-      base -> baseCase
-      loop i -> loopCase i
-
-torusToCircsToTorus : (x : T2) -> Path (circsToTorus (torusToCircs x)) x
-torusToCircsToTorus = \case
-  baseT -> refl
-  pathOne i -> refl
-  pathTwo i -> refl
-  square i j -> refl
-
-circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p
-circsToTorusToCircs pair = go pair.1 pair.2
-  where
+TorusIsTwoCircles : Path T2 (S1 * S1)
+TorusIsTwoCircles = univalence (IsoToEquiv theIso) where
+  torusToCircs : T2 -> S1 * S1
+  torusToCircs = \case
+    baseT -> (base, base)
+    pathOne i -> (loop i, base)
+    pathTwo i -> (base, loop i)
+    square i j -> (loop i, loop j)
+
+  circsToTorus : (S1 * S1) -> T2
+  circsToTorus pair = go pair.1 pair.2
+    where
+      baseCase : S1 -> T2
+      baseCase = \case
+        base -> baseT
+        loop j -> pathTwo j
+
+      loopCase : Path baseCase baseCase
+      loopCase i = \case
+        base -> pathOne i
+        loop j -> square i j
+
+      go : S1 -> S1 -> T2
+      go = \case
+        base -> baseCase
+        loop i -> loopCase i
+
+  torusToCircsToTorus : (x : T2) -> Path (circsToTorus (torusToCircs x)) x
+  torusToCircsToTorus = \case
+    baseT -> refl
+    pathOne i -> refl
+    pathTwo i -> refl
+    square i j -> refl
+
+  circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p
+  circsToTorusToCircs pair = go pair.1 pair.2 where
     baseCase : (y : S1) -> Path (torusToCircs (circsToTorus (base, y))) (base, y)
     baseCase = \case
       base -> refl
@@ -979,11 +993,9 @@ circsToTorusToCircs pair = go pair.1 pair.2
       base -> baseCase
       loop i -> loopCase i
 
-TorusIsTwoCircles : Path T2 (S1 * S1)
-TorusIsTwoCircles = univalence (IsoToEquiv theIso) where
   theIso : Iso T2 (S1 * S1)
   theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus)
-
+  
 abs : Int -> Nat
 abs = \case
   pos n -> n
@@ -1041,15 +1053,169 @@ isProp A = (x : A) (y : A) -> Path x y
 
 data Sq (A : Type) : Type where
   inc : A -> Sq A
-  sq i : (x : A) (y : A) -> Sq A [ (i = i0) -> inc x, (i = i1) -> inc y ]
+  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 =
+  hcomp {A}
+    (\k [ (i = i0) -> h a a k
+        , (i = i1) -> h a b k
+        , (j = i0) -> h a (p i) k
+        , (j = i1) -> h a (q i) k
+        ])
+    (inS a)
 
 Sq_rec : {A : Type} {B : Type}
       -> isProp B
       -> (f : A -> B)
       -> Sq A -> B
-Sq_rec prop f = \case
-  inc x -> f x
-  sq x y i -> prop (f x) (f y) i
+Sq_rec prop f =
+  \case
+    inc x -> f x
+    sq x y i -> prop (work x) (work y) i
+  where
+    work : Sq A -> B
+    work = \case
+      inc x -> f x
 
 hitTranspExample : Path (inc false) (inc true)
-hitTranspExample i = transp (\i -> Sq (notp i)) (sq true false i)
\ No newline at end of file
+hitTranspExample i = transp (\i -> Sq (notp i)) (sq (inc true) (inc false) i)
+
+data S2 : Type where
+  base2 : S2
+  surf2 i j : S2 [ (i = i0) -> base2, (i = i1) -> base2, (j = i0) -> base2, (j = i1) -> base2]
+
+S2IsSuspS1 : Path S2 (Susp S1)
+S2IsSuspS1 = univalence (IsoToEquiv iso) where
+  toS2 : Susp S1 -> S2
+  toS2 = \case { north -> base2; south -> base2; merid x i -> sphMerid x i } where
+    sphMerid = \case
+      base -> \i -> base2
+      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 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 }
+
+  toFromS2 : (x : S2) -> Path (toS2 (fromS2 x)) x
+  toFromS2 = \case { base2 -> refl; surf2 i j -> refl }
+
+  fromToS2 : (x : Susp S1) -> Path (fromS2 (toS2 x)) x
+  fromToS2 = \case { north -> refl; south -> \i -> merid base i; merid x i -> meridCase i x } where
+    meridCase : (i : I) (x : S1) -> Path (fromS2 (toS2 (merid x i))) (merid x i)
+    meridCase i = \case
+      base -> \k -> merid base (iand i k)
+      loop j -> \k -> suspSurf i j (inot k)
+
+  iso : Iso S2 (Susp S1)
+  iso = (fromS2, toS2, fromToS2, toFromS2)
+
+data S3 : Type where
+  base3 : S3
+  surf3 i j k : S3 [ (i = i0) -> base3, (i = i1) -> base3, (j = i0) -> base3, (j = i1) -> base3, (k = i0) -> base3, (k = i1) -> base3 ]
+
+S3IsSuspS2 : Path S3 (Susp S2)
+S3IsSuspS2 = univalence (IsoToEquiv iso) where
+  toS3 : Susp S2 -> S3
+  toS3 = \case { north -> base3; south -> base3; merid x i -> sphMerid x i } where
+    sphMerid = \case
+      base2 -> \i -> base3
+      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 base2 (iand (inot l) i)
+                                       , (k = i0) -> merid base2 (iand (inot l) i)
+                                       , (k = i1) -> merid 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 }
+
+  toFromS3 : (x : S3) -> Path (toS3 (fromS3 x)) x
+  toFromS3 = \case { base3 -> refl; surf3 i j k -> refl }
+
+  fromToS3 : (x : Susp S2) -> Path (fromS3 (toS3 x)) x
+  fromToS3 = \case { north -> refl; south -> \i -> merid base2 i; merid x i -> meridCase i x } where
+    meridCase : (i : I) (x : S2) -> Path (fromS3 (toS3 (merid x i))) (merid x i)
+    meridCase i = \case
+      base2 -> \k -> merid base2 (iand i k)
+      surf2 j k -> \l -> suspSurf i j k (inot l)
+
+  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
+
+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
+
+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
+  uipRefl A x p = K_s {A} {x} (\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
+
+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
+
+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
+  zeroCase : (y : Nat) -> Path zero y -> Eq_s zero y
+  zeroCase = \case
+    zero -> \p -> refl_s
+    succ x -> \p -> absurd (zeroNotSucc p)
+  succCase : (x : Nat) (y : Nat) -> Path (succ x) y -> Eq_s (succ x) y
+  succCase x = \case
+    zero -> \p -> absurd (zeroNotSucc (sym p))
+    succ y -> \p -> ap_s succ (Path_nat_strict_nat x y (succInj p))
+
+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
+  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)
+
+  inv : (y : A) (l : Path x y) -> Path (strictEq_pathEq (p_to_s l)) l
+  inv y l = J {A} {x} (\y l -> Path (strictEq_pathEq (p_to_s l)) l) (strictEq_pathEq aux) {y} l where
+    aux : Eq_s (strictEq_pathEq (p_to_s (\i -> x))) (\i -> x)
+    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
+  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
+    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
diff --git a/src/Elab.hs b/src/Elab.hs
index e6e4aad..0b07e20 100644
--- a/src/Elab.hs
+++ b/src/Elab.hs
@@ -102,11 +102,8 @@ check (P.Lam p v b) ty = do
 
       tm_nf <- eval tm
 
-      unify (tm_nf @@ VI0) le
-        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI0)
-
-      unify (tm_nf @@ VI1) ri
-        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI1)
+      unify (tm_nf @@ VI0) le `catchElab` (throwElab . WhenCheckingEndpoint (Bound v 0) le ri VI0)
+      unify (tm_nf @@ VI1) ri `catchElab` (throwElab . WhenCheckingEndpoint (Bound v 0) le ri VI1)
 
       pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
 
@@ -237,6 +234,8 @@ check (P.LamCase pats) ty =
                     unify vl rhs
                       `withNote` vcat [ pretty "These must be the same because of the face"
                                       , indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
+                                      , pretty "which evaluates into"
+                                      , indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyVl rhs
                                       ]
                       `withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf))
               _ -> pure ()
@@ -501,13 +500,13 @@ checkStatement (P.ReplNf e) k = do
   (e, _) <- infer e
   e_nf <- eval e
   h <- asks commHook
-  liftIO (h e_nf)
+  liftIO (h (prettyVl e_nf))
   k
 
 checkStatement (P.ReplTy e) k = do
-  (_, ty) <- infer e
+  (t, ty) <- infer e
   h <- asks commHook
-  liftIO (h ty)
+  liftIO (h (prettyTm t <+> colon <+> align (prettyVl ty)))
   k
 
 checkStatement (P.Data name tele retk constrs) k =
@@ -579,7 +578,7 @@ checkStatement (P.Data name tele retk constrs) k =
 
         system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList (map snd faces))) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices)
 
-        unify (foldr ior VI0 (map fst faces)) (totalProp indices)
+        unify (foldl ior VI0 (map fst faces)) (totalProp indices)
           `withNote` pretty "The formula determining the endpoints of a higher constructor must be a classical tautology"
 
         pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system)
@@ -600,7 +599,7 @@ checkStatement (P.Data name tele retk constrs) k =
     makePCon cty sp [] ((nm, p, _):ys) zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) [] ys zs (sys @@ a) con
     makePCon cty sp [] []         (nm:zs) sys con = VLam P.Ex $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp P.Ex a) [] [] zs (sys @@ a) con
 
-    totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs
+    totalProp (x:xs) = ior (VVar x) (inot (VVar x) `ior` totalProp xs)
     totalProp [] = VI0
 
 
@@ -611,7 +610,7 @@ checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
 newtype Redefinition = Redefinition { getRedefName :: Name }
   deriving (Show, Typeable, Exception)
 
-data WhenCheckingEndpoint = WhenCheckingEndpoint { leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
+data WhenCheckingEndpoint = WhenCheckingEndpoint { direction :: Name, leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
   deriving (Show, Typeable, Exception)
 
 data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs
index 002bb0d..dced8ed 100644
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@@ -35,7 +35,7 @@ import Prettyprinter
 import Syntax.Pretty
 import Syntax
 
-import System.IO.Unsafe
+import System.IO.Unsafe ( unsafePerformIO )
 
 import {-# SOURCE #-} Elab.WiredIn
 
@@ -93,13 +93,19 @@ zonkIO (VGlueTy a phi ty e)   = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO
 zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x
 zonkIO (VUnglue a phi ty e x) = unglue   <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO x
 zonkIO (VCase env t x xs) = do
-  env' <- emptyEnv
-  evalCase env'{getEnv = env} . (@@) <$> zonkIO t <*> zonkIO x <*> pure xs
+  env' <- (\x -> x {getEnv = env}) <$> emptyEnv
+  let xs' = map (\(a, i, n) -> (a, i, quote (eval' env' n))) xs
+  evalCase env' . (@@) <$> zonkIO t <*> zonkIO x <*> pure xs'
+
+zonkIO (VEqStrict a x y) = VEqStrict <$> zonkIO a <*> zonkIO x <*> zonkIO y
+zonkIO (VReflStrict a x) = VReflStrict <$> zonkIO a <*> zonkIO x
 
 zonkSp :: Projection -> IO Projection
 zonkSp (PApp p x) = PApp p <$> zonkIO x
 zonkSp (PIElim l x y i) = PIElim <$> zonkIO l <*> zonkIO x <*> zonkIO y <*> zonkIO i
 zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u
+zonkSp (PK a x p pr) = PK <$> zonkIO a <*> zonkIO x <*> zonkIO p <*> zonkIO pr
+zonkSp (PJ a x p pr y) = PJ <$> zonkIO a <*> zonkIO x <*> zonkIO p <*> zonkIO pr <*> zonkIO y
 zonkSp PProj1 = pure PProj1
 zonkSp PProj2 = pure PProj2
 
@@ -122,7 +128,6 @@ eval' env (PCon sys x) =
     Just (ty, _) -> VNe (HPCon (eval' env sys) ty x) mempty
     Nothing -> error $ "constructor " ++ show x ++ " has no type in scope"
 
-
 eval' _ (Data n x) = VNe (HData n x) mempty
 eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
 
@@ -164,7 +169,7 @@ 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) = VSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
+eval' e (System fs) = mkVSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
 
 eval' e (Sub a phi u)   = VSub (eval' e a) (eval' e phi) (eval' e u)
 eval' e (Inc a phi u)   = VInc (eval' e a) (eval' e phi) (eval' e u)
@@ -186,6 +191,11 @@ eval' e (Let ns x) =
 
 eval' e (Case range sc xs) = evalCase e (eval' e range @@) (force (eval' e sc)) xs
 
+eval' e (EqS a x y) = VEqStrict (eval' e a) (eval' e x) (eval' e y)
+eval' e (Syntax.Refl a x) = VReflStrict (eval' e a) (eval' e x)
+eval' e (Syntax.AxK a x p pr eq) = strictK (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e eq)
+eval' e (Syntax.AxJ a x p pr y eq) = strictJ (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e y) (eval' e eq)
+
 evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Int, Term)] -> Value
 evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
 
@@ -225,11 +235,23 @@ 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
 
-  go (VNe (HPCon s _ _) _) rhs
-    | VSystem _ <- s = go (force s) rhs
+  go (VNe (HPCon s _ _) _) rhs = go (force s) rhs
+  go lhs (VNe (HPCon s _ _) _) = go lhs (force s)
+
+  go (VCase e _ a b) (VCase e' _ a' b') = do
+    env <- ask
+    unify' a a'
+    let go (_, _, a) (_, _, b) = unify' (eval' env{getEnv=e} a) (eval' env{getEnv=e'} b)
+    zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b')
 
-  go lhs (VNe (HPCon s _ _) _)
-    | VSystem _ <- s = go lhs (force s)
+  go (VCase e _ _ b) y = do
+    env <- ask
+    let
+      go (_, n, a') = do
+        ns <- replicateM n (VVar <$> newName)
+        let a = foldl (vApp Ex) (eval' env{getEnv=e} a') ns
+        unify' a y
+    traverse_ go b
 
   go (VNe x a) (VNe x' a')
     | x == x', length a == length a' =
@@ -301,10 +323,8 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VSystem sys) rhs = goSystem unify' sys rhs
   go rhs (VSystem sys) = goSystem (flip unify') sys rhs
 
-  go (VCase _ _ a b) (VCase _ _ a' b') = do
-    unify' a a'
-    let go (_, _, a) (_, _, b) = join $ unify' <$> eval a <*> eval b
-    zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b')
+  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 x y
     | x == y = pure ()
@@ -334,6 +354,12 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   unify'Spine (POuc a phi u) (POuc a' phi' u') =
     traverse_ (uncurry unify') [(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 (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 _ _ = fail
 
   unify'Formula x y
@@ -429,6 +455,8 @@ checkScope scope (VNe h sp) =
   where
     checkProj (PApp _ t) = checkScope scope t
     checkProj (PIElim l x y i) = traverse_ (checkScope scope) [l, x, y, i]
+    checkProj (PK l x y i) = traverse_ (checkScope scope) [l, x, y, i]
+    checkProj (PJ l x y i j) = traverse_ (checkScope scope) [l, x, y, i, j]
     checkProj (POuc a phi u) = traverse_ (checkScope scope) [a, phi, u]
     checkProj PProj1 = pure ()
     checkProj PProj2 = pure ()
@@ -481,6 +509,9 @@ checkScope s (VUnglue a phi ty eq vl) = traverse_ (checkScope s) [a, phi, ty, eq
 
 checkScope s (VCase _ _ v _) = checkScope s v
 
+checkScope s (VEqStrict a x y) = traverse_ (checkScope s) [a, x, y]
+checkScope s (VReflStrict a x) = traverse_ (checkScope s) [a, x]
+
 checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
 checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
   | n `Set.member` scope = throwElab $ NonLinearSpine n
@@ -549,6 +580,8 @@ substituteIO sub = substituteIO . force where
   substituteIO (VGlue a phi ty e t x) = glueElem <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO t <*> substituteIO x
   substituteIO (VUnglue a phi ty e x) = unglue   <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO x
   substituteIO (VCase env t x xs) = VCase env <$> substituteIO t <*> substituteIO x <*> pure xs
+  substituteIO (VEqStrict a x y) = VEqStrict <$> zonkIO a <*> zonkIO x <*> zonkIO y
+  substituteIO (VReflStrict a x) = VReflStrict <$> zonkIO a <*> zonkIO x
 
 substitute :: Map Name Value -> Value -> Value
 substitute sub = unsafePerformIO . substituteIO sub
@@ -556,16 +589,23 @@ substitute sub = unsafePerformIO . substituteIO sub
 substituteSp :: Map Name Value -> Projection -> IO Projection
 substituteSp sub (PApp p x) = PApp p <$> substituteIO sub x
 substituteSp sub (PIElim l x y i) = PIElim <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i
+substituteSp sub (PK l x y i) = PK <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i
+substituteSp sub (PJ l x y i j) = PJ <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i <*> substituteIO sub j
 substituteSp sub (POuc a phi u) = POuc <$> substituteIO sub a <*> substituteIO sub phi <*> substituteIO sub u
 substituteSp _ PProj1 = pure PProj1
 substituteSp _ PProj2 = pure PProj2
 
 mkVSystem :: Map.Map Value Value -> Value
 mkVSystem vals =
-  let map' = Map.fromList (map (\(a, b) -> (force a, b)) (Map.toList vals)) in
-  case Map.lookup VI1 map' of
+  let map' = Map.fromList (Map.toList vals >>= go)
+      go (x, y) = 
+        case (force x, y) of
+          (VI0, _) -> []
+          (VIOr _ _, VSystem y) -> Map.toList y >>= go
+          (a, b) -> [(a, b)]
+  in case Map.lookup VI1 map' of
     Just x -> x
-    Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map')
+    Nothing -> VSystem map'
 
 forceIO :: MonadIO m => Value -> m Value
 forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do
@@ -579,6 +619,7 @@ forceIO vl@(VSystem fs) =
     Nothing -> pure vl
 forceIO (GluedVl _ _ vl) = forceIO vl
 forceIO (VComp line phi u a0) = comp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0
+forceIO (VHComp line phi u a0) = hComp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0
 forceIO (VCase env rng v vs) = do
   env' <- liftIO emptyEnv
   r <- forceIO rng
@@ -592,17 +633,17 @@ applProj :: HasCallStack => Value -> Projection -> Value
 applProj fun (PApp p arg)     = vApp p fun arg
 applProj fun (PIElim l x y i) = ielim l x y fun i
 applProj fun (POuc a phi u)   = outS a phi u fun
+applProj fun (PK a x p pr)    = strictK a x p pr fun
+applProj fun (PJ a x p pr y)  = strictJ a x p pr y fun
 applProj fun PProj1           = vProj1 fun
 applProj fun PProj2           = vProj2 fun
 
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
 vApp p (VLam p' k) arg
-  | p == p'   = clCont k arg
-  | otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg))
-vApp p (VNe h sp) arg    = VNe h (sp Seq.:|> PApp p arg)
+  | p == p' = clCont k arg
+vApp p (VNe h sp) arg  = VNe h (sp Seq.:|> PApp p arg)
 vApp p (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg)
-vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
-vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg)
+vApp p (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs)
 vApp p (VCase env rng sc branches) arg =
   VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
     (map (projIntoCase (flip (App p) (quote arg))) branches)
@@ -631,10 +672,3 @@ vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c)
 vProj2 (VCase env rng sc branches) =
   VCase env rng sc (map (projIntoCase Proj2) branches)
 vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))
-
-projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)
-projIntoCase fun (pat, nLams, term) = (pat, nLams, go nLams term) where
-  go 0 x = fun x
-  go n (Lam p x r) = Lam p x (go (n - 1) r)
-  go n (PathIntro l a b r) = PathIntro l a b (go (n - 1) r)
-  go _ x = x
\ No newline at end of file
diff --git a/src/Elab/Eval/Formula.hs b/src/Elab/Eval/Formula.hs
index 4958f07..70fc9c3 100644
--- a/src/Elab/Eval/Formula.hs
+++ b/src/Elab/Eval/Formula.hs
@@ -7,17 +7,32 @@ import Data.Map.Strict (Map)
 import Syntax
 
 import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
+import Data.Set (Set)
+import qualified Data.Set as Set
 
 toDnf :: Value -> Maybe Value
-toDnf (VNe _ _) = Nothing
-toDnf x = toDnf x where
-  toDnf (VIAnd x y) = idist <$> toDnf (inot x) <*> toDnf (inot y)
-  toDnf (VIOr x y) = ior <$> toDnf x <*> toDnf y
-  toDnf (VINot x) = inot <$> toDnf x
-  toDnf VI0 = pure VI0
-  toDnf VI1 = pure VI1
-  toDnf v@(VNe _ Seq.Empty) = pure v
-  toDnf _ = Nothing
+toDnf = fmap (dnf2Val . normalise) . val2Dnf where
+  val2Dnf (VNe _ _) = Nothing
+  val2Dnf x = toDnf x where
+    toDnf (VIAnd x y) = idist <$> toDnf (inot x) <*> toDnf (inot y)
+    toDnf (VIOr x y) = ior <$> toDnf x <*> toDnf y
+    toDnf (VINot x) = inot <$> toDnf x
+    toDnf VI0 = pure VI0
+    toDnf VI1 = pure VI1
+    toDnf v@(VNe _ Seq.Empty) = pure v
+    toDnf _ = Nothing
+
+  dnf2Val xs = Set.foldl ior VI0 (Set.map (Set.foldl iand VI1) xs)
+
+type Nf = Set (Set Value)
+
+normalise :: Value -> Nf
+normalise = normaliseOr where
+  normaliseOr (VIOr x y) = Set.singleton (normaliseAnd x) <> normaliseOr y
+  normaliseOr x = Set.singleton (normaliseAnd x)
+
+  normaliseAnd (VIAnd x y) = Set.insert x (normaliseAnd y)
+  normaliseAnd x = Set.singleton x
 
 compareDNFs :: Value -> Value -> Bool
 compareDNFs (VIOr x y) (VIOr x' y') =
diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs
index 68bfe62..539b10b 100644
--- a/src/Elab/Monad.hs
+++ b/src/Elab/Monad.hs
@@ -26,17 +26,19 @@ data ElabEnv =
 
           , nameMap     :: Map Text Name
           , pingPong    :: {-# UNPACK #-} !Int
-          , commHook    :: Value -> IO ()
+          , commHook    :: Doc AnsiStyle -> IO ()
 
           , currentSpan :: Maybe (P.Posn, P.Posn)
           , currentFile :: Maybe Text
 
-          , whereBound  :: Map Name (P.Posn, P.Posn)
+          , whereBound   :: Map Name (P.Posn, P.Posn)
           , definedNames :: Set Name
 
-          , boundaries :: Map Name Boundary
+          , boundaries   :: Map Name Boundary
 
           , unsolvedMetas :: {-# UNPACK #-} !(IORef (Map MV [(Seq Projection, Value)]))
+
+          , loadedFiles :: [String]
           }
 
 newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
@@ -44,7 +46,24 @@ newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
     via ReaderT ElabEnv IO
 
 emptyEnv :: IO ElabEnv
-emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing Nothing mempty mempty mempty <$> newIORef mempty
+emptyEnv = do
+  u <- newIORef mempty
+  pure $ ElabEnv { getEnv      = mempty
+                 , nameMap     = mempty
+                 , pingPong    = 0
+                 , commHook    = const (pure ())
+
+                 , currentSpan = Nothing
+                 , currentFile = Nothing
+
+                 , whereBound   = mempty
+                 , definedNames = mempty
+
+                 , boundaries   = mempty
+
+                 , unsolvedMetas = u
+                 , loadedFiles = []
+                 }
 
 addBoundary :: Name -> Boundary -> ElabM a -> ElabM a
 addBoundary nm boundary = local (\e -> e { boundaries = Map.insert nm boundary (boundaries e)} )
diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs
index 302011d..60c06ed 100644
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@@ -21,7 +21,7 @@ import GHC.Stack (HasCallStack)
 
 import qualified Presyntax.Presyntax as P
 
-import Syntax.Pretty (prettyTm)
+import Syntax.Pretty (prettyTm, prettyVl)
 import Syntax
 
 import System.IO.Unsafe
@@ -58,6 +58,11 @@ wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T"
 -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
 wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a
 
+wiType WiSEq   = forAll' "A" VTypeω \a -> a ~> a ~> VTypeω
+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
+
 wiValue :: WiredIn -> Value
 wiValue WiType     = VType
 wiValue WiPretype  = VTypeω
@@ -85,6 +90,11 @@ wiValue WiGlue     = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a ph
 wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
 wiValue WiUnglue   = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> unglue a phi ty eqv x
 
+wiValue WiSEq   = forallI \a -> fun \x -> fun \y -> VEqStrict a x y
+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
+
 (~>) :: Value -> Value -> Value
 a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
 infixr 7 ~>
@@ -143,6 +153,11 @@ wiredInNames = Map.fromList
   , ("Glue", WiGlue)
   , ("glue", WiGlueElem)
   , ("unglue", WiUnglue)
+  
+  , ("Eq_s", WiSEq)
+  , ("refl_s", WiSRefl)
+  , ("K_s", WiSK)
+  , ("J_s", WiSJ)
   ]
 
 newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
@@ -199,7 +214,9 @@ ielim line left right fn i =
         VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i)
         VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
         VInc (VPath _ _ _) _ u -> ielim line left right u i
+
         VCase env r x xs -> VCase env r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
+
         _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
 
 outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
@@ -210,7 +227,7 @@ outS _ VI0 _  x            = x
 
 outS a phi u  (GluedVl x sp vl) = GluedVl x (sp Seq.:|> POuc a phi u) (outS a phi u vl)
 outS a phi u  (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
-outS a phi u (VSystem fs) = VSystem (fmap (outS a phi u) fs)
+outS a phi u (VSystem fs) = mkVSystem (fmap (outS a phi u) fs)
 outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 
 -- Composition
@@ -237,7 +254,6 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
         rng i = let VSigma _ (Closure _ r) = force (a @@ i) in r
 
         w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i
-        -- c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0))
         c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0))
        in
          VPair (w VI1) c2
@@ -332,11 +348,12 @@ compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value
 compHIT name n a phi u a0 =
   case force phi of
     VI1 -> u @@ VI1 @@ VItIsOne
-    VI0 -> transHit name a VI0 (compOutS (a VI0) phi u a0)
+    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 -> squeezeHit 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 @@ VItIsOne) a0))
 
 compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
             -> Int
@@ -370,21 +387,22 @@ makeSetFiller typeArgument nth (VNe (HData _ n') args) phi u a0
 makeSetFiller _ _ _ _ _ a0 = fun (const a0)
 
 nthArg :: Int -> Value -> Value
-nthArg i (VNe hd s) =
+nthArg i (force -> VNe hd s) =
   case s Seq.!? i of
     Just (PApp _ t) -> t
     _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
-nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs)
+nthArg i (force -> VSystem vs) = VSystem (fmap (nthArg i) vs)
 nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))
 
 compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
 compOutS a b c d = compOutS a b c (force d) where
-  compOutS _ _hi _0 vl@VComp{}   = vl
+  compOutS _ _hi _0 vl@VComp{}   = error $ "unwrapped composition given as input to composition operation is fuckign illegal " ++ show (prettyTm (quote (zonk vl)))
+  compOutS _ _hi _0 vl@VHComp{}  = error $ "unwrapped composition (gay) given as input to composition operation is fuckign illegal " ++ show (prettyTm (quote (zonk vl)))
   compOutS _ _hi _0 (VInc _ _ x) = x
   compOutS a phi a0 v = outS a phi a0 v
 
 system :: (Value -> Value -> Value) -> Value
-system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "phi" 0) \isone -> k i isone
+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 a phi u a0 j =
@@ -471,34 +489,35 @@ gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value
 gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (VInc (line VI0) VI0 a0)
 
 transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value
-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 u0)
-transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
-  x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
-  (_, VNe hd (length -> nargs)) = unPi con_type
-  ourType = case hd of
-    HData True n' -> n' == name
-    _ -> False
-
-transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
-  x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
-  rec = transHit name line phi
-  (_, VNe hd (length -> nargs)) = unPi con_type
-  ourType = case hd of
-    HData True n' -> n' == name
-    _ -> False
-
-transHit name line phi (VSystem xs) = mkVSystem (fmap (transHit name line phi) xs)
-transHit _ line phi a0 = gtrans line phi a0
-
-fillHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> NFEndp -> Value
-fillHit name a phi a0 i = transHit name (\j -> a (iand i j)) (phi `ior` inot i) a0 where
-
-squeezeHit :: Name -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> NFEndp -> Value
-squeezeHit name a phi x i = transHit name (\j -> a (ior i j)) (phi `ior` i) (x i)
+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 (compOutS (line VI0) phi u u0))
+  transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
+    x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
+    (_, VNe hd (length -> nargs)) = unPi con_type
+    ourType = case hd of
+      HData True n' -> n' == name
+      _ -> False
+
+  transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
+    x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
+    rec = transHit name line phi
+    (_, VNe hd (length -> nargs)) = unPi con_type
+    ourType = case hd of
+      HData True n' -> n' == name
+      _ -> False
+
+  transHit name line phi (VSystem xs) = mkVSystem (fmap (transHit name line phi) xs)
+  transHit _ line phi a0 = gtrans line phi a0
+
+transFill :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> NFEndp -> Value
+transFill name a phi a0 i = transHit name (\j -> a (iand i j)) (phi `ior` inot i) a0 where
+
+transSqueeze :: Name -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> NFEndp -> Value
+transSqueeze name a phi x i = transHit name (\j -> a (ior i j)) (phi `ior` i) (x i)
 
 makeTransFiller :: Name -> Name -> p -> Value -> NFEndp -> () -> Value -> Value
 makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0
-  | n' == typeArgument = fun (fillHit thedata (makeDomain args) phi a0)
+  | n' == typeArgument = fun (transFill thedata (makeDomain args) phi a0)
   where
     makeDomain (PApp _ x Seq.:<| xs) = \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
     makeDomain _ = error "somebody smuggled something that smells"
@@ -544,4 +563,27 @@ idEquiv a = VPair idfun idisequiv where
       VLine (fun (const a)) y (vProj1 u) $ fun \j ->
         ielim (fun (const a)) y y (vProj2 u) (iand i j)
 
-  id_fiber y = VPair y (VLine a y y (fun (const y)))
\ No newline at end of file
+  id_fiber y = VPair y (VLine a y y (fun (const y)))
+
+strictK :: Value -> Value -> Value -> Value -> Value -> Value
+strictK _ _ _ pr (VReflStrict _ _) = pr
+strictK a x bigp pr (VNe h sp) = VNe h (sp Seq.:|> PK a x bigp pr)
+strictK a x bigp pr (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
+  func = AxK (quote a) (quote x) (quote bigp) (quote pr)
+strictK a x bigp pr (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PK a x bigp pr) (strictK a x bigp pr vl)
+strictK _ _ _ _r eq = error $ "can't K " ++ show (prettyVl eq)
+
+strictJ :: Value -> Value -> Value -> Value -> Value -> Value -> Value
+strictJ _a _x _bigp pr _ (VReflStrict _ _) = pr
+strictJ a x bigp pr y (VNe h sp) = VNe h (sp Seq.:|> PJ a x bigp pr y)
+strictJ a x bigp pr y (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
+  func = AxJ (quote a) (quote x) (quote bigp) (quote pr) (quote y)
+strictJ a x bigp pr y (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PJ a x bigp pr y) (strictJ a x bigp pr y vl)
+strictJ _ _ _ _r _ eq = error $ "can't J " ++ show eq
+
+projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)
+projIntoCase fun (pat, nLams, term) = (pat, nLams, go nLams term) where
+  go 0 x = fun x
+  go n (Lam p x r) = Lam p x (go (n - 1) r)
+  go n (PathIntro l a b r) = PathIntro l a b (go (n - 1) r)
+  go _ x = x
\ No newline at end of file
diff --git a/src/Elab/WiredIn.hs-boot b/src/Elab/WiredIn.hs-boot
index 756cbc3..bfca174 100644
--- a/src/Elab/WiredIn.hs-boot
+++ b/src/Elab/WiredIn.hs-boot
@@ -21,4 +21,9 @@ glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value ->
 unglue   :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
 
 fun :: (Value -> Value) -> Value
-system :: (Value -> Value -> Value) -> Value
\ No newline at end of file
+system :: (Value -> Value -> Value) -> Value
+
+strictK :: NFSort -> Value -> NFSort -> Value -> Value -> Value
+strictJ :: NFSort -> Value -> NFSort -> Value -> Value -> Value -> Value
+
+projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)
\ No newline at end of file
diff --git a/src/Main.hs b/src/Main.hs
index e298fe3..4bb4d14 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE NamedFieldPuns #-}
 module Main where
 
 import Control.Monad.IO.Class
@@ -55,7 +56,7 @@ main = do
     Check files verbose -> do
       env <- checkFiles files
       when verbose $ dumpEnv env
-    Repl -> enterReplIn =<< checkFiles ["./test.tt"]
+    Repl -> enterReplIn =<< emptyEnv
 
 evalArgExpr :: ElabEnv -> String -> IO ()
 evalArgExpr env str =
@@ -71,30 +72,59 @@ evalArgExpr env str =
     inp = T.pack str
 
 enterReplIn :: ElabEnv -> IO ()
-enterReplIn env = runInputT defaultSettings (loop env') where
-  env' = env { commHook = T.putStrLn . render . prettyTm . quote . zonk }
+enterReplIn env =
+  do
+    let env' = mkrepl env
+    envref <- newIORef env'
+    runInputT (setComplete (complete envref) defaultSettings) (loop env' envref)
+  where
+    mkrepl env = env { commHook = T.putStrLn . render }
 
-  loop :: ElabEnv -> InputT IO ()
-  loop env = do
-    inp <- fmap T.pack <$> getInputLine "% "
-    case inp of
-      Nothing -> pure ()
-      Just inp ->
-        case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseRepl of
-          Left e -> do
-            liftIO $ print e
-            loop env
-          Right st -> do
-            env <- liftIO $
-              runElab (checkStatement st ask) env
-                `catch` \e -> do
-                  displayExceptions' inp (e :: SomeException)
-                  pure env
-            loop env
+    complete :: IORef ElabEnv -> (String, String) -> IO (String, [Completion])
+    complete c = completeWord Nothing " \n\t\r" go where
+      go w = do
+        env <- readIORef c
+        let
+          w' = T.pack w
+          words = Set.toList $ Set.filter ((w' `T.isPrefixOf`) . getNameText) (definedNames env)
+        pure (map (simpleCompletion . T.unpack . getNameText) words)
+
+    loop :: ElabEnv -> IORef ElabEnv -> InputT IO ()
+    loop env envvar = do
+      inp <- fmap T.pack <$> getInputLine "% "
+      case inp of
+        Nothing -> pure ()
+        Just inp | ":r" `T.isPrefixOf` inp -> reload env envvar
+        Just inp ->
+          case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseRepl of
+            Left e -> do
+              liftIO $ print e
+              loop env envvar
+            Right st -> do
+              env <- liftIO $
+                runElab (checkStatement st ask) env
+                  `catch` \e -> do
+                    displayExceptions' inp (e :: SomeException)
+                    pure env
+              liftIO $ writeIORef envvar 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
 
 checkFiles :: [String] -> IO ElabEnv
-checkFiles files = runElab (go files ask) =<< emptyEnv where
-  go [] k = do
+checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
+  size = length files
+  sl = length (show size)
+
+  pad s
+    | length s < sl = replicate (sl - length s) ' ' ++ s
+    | otherwise = s
+
+  go _ [] k = do
     env <- ask
     for_ (Map.toList (nameMap env)) \case
       (_, v@Defined{})
@@ -108,28 +138,35 @@ checkFiles files = runElab (go files ask) =<< emptyEnv where
     metas <- liftIO $ readIORef (unsolvedMetas env)
     unless (Map.null metas) $ do
       liftIO $ reportUnsolved metas
-
     k
-  go (x:xs) k = do
+
+  go n (x:xs) k = do
+    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)
       Right prog ->
-        local (\e -> e { currentFile = Just (T.pack x) }) (checkProgram prog (go xs k))
+        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)
 
 dumpEnv :: ElabEnv -> IO ()
 dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) ->
   let nft = fst $ getEnv env Map.! name in
-  T.putStrLn $ render (pretty name <+> align (nest (negate 1) (colon <+> prettyTm (quote (zonk nft)))))
+  T.putStrLn $ render (pretty name <+> nest (negate 1) (colon <+> align (prettyTm (quote (zonk nft)))))
 
 parser :: ParserInfo Opts
-parser = info (subparser (load <> check) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
+parser = info (subparser (load <> check <> repl) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
   where
     load  = command "load" $
       info ((Load <$> (some (argument str (metavar "file...")))
                   <*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression"))))
        <**> helper) (progDesc "Check and load a list of files in the REPL")
+
+    repl  = command "load" $
+      info ((Load <$> (many (argument str (metavar "file...")))
+                  <*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression"))))
+       <**> helper) (progDesc "Enter the REPL, optionally with loaded files")
+
     check = command "check" $
       info ((Check <$> some (argument str (metavar "file..."))
                    <*> switch ( long "verbose"
@@ -160,23 +197,25 @@ displayExceptions lines =
   , Handler \(AttachedNote n e) -> do
       displayExceptions' lines e
       T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
-  , Handler \(WhenCheckingEndpoint le ri ep e) -> do
+  , Handler \(WhenCheckingEndpoint dir le ri ep e) -> do
       displayExceptions' lines e
       let
         endp = case ep of
           VI0 -> T.pack "left"
           VI1 -> T.pack "right"
           _ -> T.pack $ show (prettyTm (quote ep))
+        left = render (prettyTm (quote le))
+        right = render (prettyTm (quote ri))
       T.putStrLn . T.unlines $
-        [ "\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram"
-        , "\t " <> render (prettyTm (quote le)) <> " " <> T.replicate 7 (T.singleton '\x2500') <> " " <> render (prettyTm (quote ri))
-        , "\x1b[1;32mnote\x1b[0m: the " <> endp <> " endpoint is incorrect"
+        [ "\n\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram <<"
+        , "\t " <> redact left <> " " <> T.replicate 7 (T.singleton '\x2500') <> " " <> redact right
+        , "      >> in the direction " <> render (pretty dir) <> ", but the " <> endp <> " endpoint is incorrect"
         ]
   , Handler \(NotEqual ta tb) -> do
-      putStrLn . unlines $
+      T.putStrLn . render . vsep $
         [ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
-        , "  * \x1b[1mActual\x1b[0m:   " ++ showValue (zonk ta)
-        , "  * \x1b[1mExpected\x1b[0m: " ++ showValue (zonk tb)
+        , indent 2 $ "* \x1b[1mActual\x1b[0m:" <> softline <> align (prettyVl (zonk ta))
+        , indent 2 $ "* \x1b[1mExpected\x1b[0m:" <> softline <> align (prettyVl (zonk tb))
         ]
   , Handler \(NoSuchPrimitive x) -> do
       putStrLn $ "Unknown primitive: " ++ T.unpack x
@@ -186,6 +225,11 @@ displayExceptions lines =
       putStrLn $ "Name declared but not defined: " ++ show (pretty n)
   ]
 
+redact :: Text -> Text
+redact x
+  | length (T.lines x) >= 2 = head (T.lines x) <> T.pack "\x1b[1;32m[...]\x1b[0m"
+  | otherwise = x
+
 reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO ()
 reportUnsolved metas = do
   for_ (Map.toList metas) \(m, p) ->  do
diff --git a/src/Syntax.hs b/src/Syntax.hs
index 4e531a7..352b20f 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -45,6 +46,12 @@ data WiredIn
   | 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
+
+  -- Two-level
+  | WiSEq   -- Eq_s   : {A : Pretype} (x y : A) -> Pretype
+  | WiSRefl -- refl_s : {A : Pretype} {x : A} -> EqS {A} x x
+  | WiSK    -- K_s    : {A : Pretype} {x : A} (P : x = x -> Pretype) -> P refl -> (p : x = x) -> P p
+  | WiSJ    -- J_s   : {A : Pretype} {x : A} (P : (y : A) -> x = y -> Pretype) -> P x refl -> {y : A} -> (p : x = y) -> P y p
   deriving (Eq, Show, Ord)
 
 data Term
@@ -99,6 +106,11 @@ data Term
   | Unglue Term Term Term Term Term
 
   | Case Term Term [(Term, Int, Term)]
+
+  | EqS  Term Term Term
+  | Refl Term Term
+  | AxK  Term Term Term Term Term
+  | AxJ  Term Term Term Term Term Term
   deriving (Eq, Show, Ord, Data)
 
 data MV =
@@ -177,6 +189,9 @@ data Value
   | VUnglue NFSort NFEndp NFPartial NFPartial Value
 
   | VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Int, Term)]
+
+  | VEqStrict   NFSort Value Value
+  | VReflStrict NFSort Value
   deriving (Eq, Show, Ord)
 
 pattern VVar :: Name -> Value
@@ -198,6 +213,8 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
 
   goSpine t (PApp p v) = App p t (quoteWith names v)
   goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i)
+  goSpine t (PK l x y i) = AxK (quote l) (quote x) (quote y) (quote i) t
+  goSpine t (PJ l x y i f) = AxJ (quote l) (quote x) (quote y) (quote i) (quote f) t
   goSpine t PProj1 = Proj1 t
   goSpine t PProj2 = Proj2 t
   goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t
@@ -212,7 +229,7 @@ quoteWith names (GluedVl h sp (VLam p (Closure n k))) =
 
 quoteWith names (GluedVl h sp vl)
   | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
-  | True || alwaysShort vl = quoteWith names vl
+  | alwaysShort vl = quoteWith names vl
   | otherwise = quoteWith names (VNe h sp)
 
 quoteWith names (VLam p (Closure n k)) =
@@ -258,9 +275,15 @@ quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith n
 
 quoteWith names (VCase _ rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs
 
+quoteWith names (VEqStrict a x y) = EqS (quoteWith names a) (quoteWith names x) (quoteWith names y)
+quoteWith names (VReflStrict a x) = Syntax.Refl (quoteWith names a) (quoteWith names x)
+
 alwaysShort :: Value -> Bool
 alwaysShort (VNe HCon{} _) = True
+alwaysShort (VNe HPCon{} _) = True
 alwaysShort VVar{} = True
+alwaysShort (VLine _ _ _ v) = alwaysShort v
+alwaysShort (VLam _ (Closure n k)) = alwaysShort (k (VVar n))
 alwaysShort _ = False
 
 refresh :: Maybe Value -> Set Name -> Name -> Name
@@ -303,7 +326,9 @@ data Projection
   | PIElim Value Value Value NFEndp
   | PProj1
   | PProj2
-  | POuc   NFSort NFEndp Value
+  | POuc  NFSort NFEndp Value
+  | PK    NFSort Value NFSort Value
+  | PJ    NFSort Value NFSort Value Value
   deriving (Eq, Show, Ord)
 
 data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value }
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index a304270..203bc60 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -1,17 +1,15 @@
+{-# LANGUAGE LambdaCase #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NamedFieldPuns #-}
 module Syntax.Pretty where
 
-import Control.Arrow (Arrow(first))
 
 import qualified Data.Map.Strict as Map
 import qualified Data.Text.Lazy as L
-import qualified Data.Set as Set
 import qualified Data.Text as T
 import Data.Map.Strict (Map)
 import Data.Text (Text)
-import Data.Set (Set)
-import Data.Generics
 
 import Presyntax.Presyntax (Plicity(..))
 
@@ -24,187 +22,188 @@ instance Pretty Name where
   pretty = pretty . getNameText
 
 prettyTm :: Term -> Doc AnsiStyle
-prettyTm = prettyTm . everywhere (mkT beautify) where
-  prettyTm (Ref v) =
-    case T.uncons (getNameText v) of
-      Just ('.', w) -> keyword (pretty w)
-      _ -> pretty v
-  prettyTm (Con v) = keyword (pretty v)
-  prettyTm (PCon _ v) = keyword (pretty v)
-  prettyTm (Data _ v) = operator (pretty v)
+prettyTm = go True 0 where
+  go t p =
+    \case
+      Ref v    -> pretty v
+      Con v    -> keyword $ pretty v
+      PCon _ v -> keyword $ pretty v
+      Data _ v -> keyword $ pretty v
+
+      App Im f _ -> go t p f
+      App Ex f x ->
+        parenIf (p >= arg_prec) $
+              go False fun_prec f
+          <+> group (go False arg_prec x)
+      
+      Lam Ex v (App Ex f (Ref v')) | v == v' -> instead f
+      Lam i v t ->
+        let
+          getArgs (Lam i v t) =
+            let (as, b) = getArgs t in ((i, v):as, b)
+          getArgs (PathIntro _ _ _ (Lam _ v t)) =
+            let (as, b) = getArgs t in ((Ex, v):as, b)
+          getArgs t = ([], t)
+
+          (as, b) = getArgs (Lam i v t)
+        in
+          parenIf (p >= fun_prec) . group $
+            pretty '\\' <> hsep (map (\(i, v) -> braceIf (i == Im) (pretty v)) as)
+              <+> arrow
+              <+> nest 2 (go False 0 b)
+      
+      Pi _ (T.unpack . getNameText -> "_") d r ->
+        parenIf (p >= fun_prec) $
+          group (go False dom_prec d)
+            <> space <> arrow <> sp
+            <> go t 0 r
+
+      Pi i x d r ->
+        let
+          c = case r of
+            Pi _ (getNameText -> x) _ _ | x /= T.pack "_" -> sp
+            _ -> space <> arrow <> sp
+        in
+          parenIf (p >= fun_prec) $
+            plic i (pretty x <+> colon <+> go False 0 d)
+              <> c <> go t 0 r
+      
+      Let binds body ->
+        parenIf (p >= fun_prec) $
+          align $ keyword (pretty "let")
+              <> line
+              <> indent 2 (prettyBinds binds)
+              <> keyword (pretty "in")
+              <+> go False 0 body
+
+      Meta MV{mvName} -> keyword (pretty mvName)
+
+      Type -> keyword (pretty "Type")
+      Typeω -> keyword (pretty "Pretype")
+
+      Sigma v d r ->
+        parenIf (p >= fun_prec) . align $
+          group (parens (pretty v <+> colon <+> go False 0 d))
+            <+> operator (pretty "*") <+> go False 0 r
+
+      Pair a b -> parens $ go False 0 a <> comma <+> go False 0 b
+      Proj1 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".1")
+      Proj2 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".2")
+
+      I -> keyword (pretty "I")
+      I0 -> keyword (pretty "i0")
+      I1 -> keyword (pretty "i1")
+
+      IAnd x y -> parenIf (p > and_prec) $
+        go False and_prec x <+> operator (pretty "/\\") <+> go False and_prec y
+
+      IOr x y -> parenIf (p > or_prec) $
+        go False or_prec x <+> operator (pretty "\\/") <+> go False or_prec y
+
+      INot x -> operator (pretty "~") <> go False p x
+
+      PathP _ x y -> parenIf (p >= arg_prec) $
+        go False 0 x <+> operator (pretty "≡") <+> go False 0 y
+      
+      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)]
+
+      System fs | Map.null fs -> braces mempty
+      System fs ->
+        let
+          face (f, t) = go False 0 f <+> operator (pretty "=>") <+> align (go False 0 t)
+        in
+          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)]
+
+      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)]
+      Unglue _a _phi _ty _e t -> apps (con "unglue") [(Ex, t)]
+
+      Comp a phi u a0 -> apps (con "comp") [(Ex, a), (Ex, phi), (Ex, u), (Ex, a0)]
+      HComp a phi u a0 -> apps (con "hcomp") [(Ex, a), (Ex, phi), (Ex, u), (Ex, a0)]
+
+      Case _ t cs ->
+        let
+          oneCase (c, 0, l) = go False 0 c <+> operator (pretty "=>") <+> go False 0 l
+          oneCase (c, i, l) =
+            let (args, bd) = getLams i l
+             in go False 0 c <+> hsep (map pretty args) <+> operator (pretty "=>") <+> go False 0 bd
+
+          getLams 0 x = ([], x)
+          getLams n (Lam _ v t) = let (as, b) = getLams (n - 1) t in (v:as, b)
+          getLams _ x = ([], x)
+        in
+          parenIf (p >= fun_prec) $
+            keyword (pretty "case") <+> go False 0 t <+> keyword (pretty "of")
+                <> line
+                <> indent 2 (vsep (map oneCase cs))
+
+      EqS _ x y -> parenIf (p >= arg_prec) $
+        go False 0 x <+> operator (pretty "≡S") <+> go False 0 y
+
+      Syntax.Refl _ _ -> keyword (pretty "refl")
+      Syntax.AxK _ _ bigp pr eq   -> apps (con "K_s") [(Ex, bigp), (Ex, pr), (Ex, eq)]
+      Syntax.AxJ _ _ bigp pr _ eq -> apps (con "J_s") [(Ex, bigp), (Ex, pr), (Ex, eq)]
+    where
+      sp | t         = softline
+         | otherwise = space
+
+      parenIf p x | p = parens x
+                  | otherwise = x
+
+      braceIf p x | p = braces x
+                  | otherwise = x
+
+      con x = Con (Bound (T.pack x) 0)
+      
+      plic = \case
+        Ex -> parens
+        Im -> braces
+
+      arrow = operator (pretty "->")
+
+      instead = go t p
+      apps :: Term -> [(Plicity, Term)] -> Doc AnsiStyle 
+      apps f xs = instead (foldl (\f (p, x) -> App p f x) f xs)
+
+prettyBinds :: [(Name, Term, Term)] -> Doc AnsiStyle
+prettyBinds [] = mempty
+prettyBinds ((x, ty, tm):bs) =
+     pretty x <+> colon <+> align (prettyTm ty)
+  <> line
+  <> pretty x <+> equals <+> align (prettyTm tm)
+  <> line
+  <> prettyBinds bs
 
-  prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
-  prettyTm (App Ex f x) = parenFun f <+> parenArg x
-
-  prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y
-  prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
-  prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
-
-  prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> nest 2 (prettyTm bod) where
-    unwindLam (Lam p x y) = first ((p, x):) (unwindLam y)
-    unwindLam (PathIntro _ _ _ (Lam p x y)) = first ((p, x):) (unwindLam y)
-    unwindLam t = ([], t)
-
-    (al, bod) = unwindLam l
-
-    used = freeVars bod
-
-    prettyArgList (Ex, v)
-      | v `Set.member` used = pretty v
-      | otherwise = pretty "_"
-    prettyArgList (Im, v)
-      | v `Set.member` used = braces $ pretty v
-      | otherwise = pretty "_"
-
-  prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x)
-  prettyTm Type{}  = keyword $ pretty "Type"
-  prettyTm Typeω{} = keyword $ pretty "Typeω"
-  prettyTm I{}     = keyword $ pretty "I"
-  prettyTm I0{}    = keyword $ pretty "i0"
-  prettyTm I1{}    = keyword $ pretty "i1"
-
-  prettyTm (Pi Ex (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "->" <+> prettyTm r
-  prettyTm (Pi Im v d r)                 = group (braces (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
-  prettyTm (Pi Ex v d r)                 = group (parens (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
-
-  prettyTm (Sigma (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "*" <+> prettyTm r
-  prettyTm (Sigma v d r)                 = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "*" <+> prettyTm r
-
-  prettyTm (IAnd x y) = parens $ prettyTm x <+> operator (pretty "&&") <+> prettyTm y
-  prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y
-  prettyTm (INot x) = operator (pretty '~') <> prettyTm x
-
-  prettyTm (System (Map.null -> True)) = braces mempty
-
-  prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where
-    go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
-
-  prettyTm (Case _ x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (line <> indent 2 (prettyCase xs) <> line)
-  prettyTm (Let xs e) = align $ keyword (pretty "let") <+> braces (line <> indent 2 (prettyLet xs) <> line) <+> keyword (pretty "in") <+> prettyTm e
-
-  prettyTm x = error (show x)
-
-  prettyCase = vcat . map go where
-    go (x, _, xs) = prettyTm x <+> operator (pretty "=>") <+> prettyTm xs
-
-  prettyLet = vcat . map go where
-    go (x, t, y) = pretty x <+> align (colon <+> nest (- 1) (prettyTm t)) <> line <> pretty x <+> pretty "=" <+> prettyTm y
-
-  beautify (PathP l x y)       = toFun "PathP" [l, x, y]
-  beautify (IElim _ _ _ f i)   = App Ex f i
-  beautify (PathIntro _ _ _ f) = f
-
-  beautify (App _ (Lam _ v b) _)
-    | v `Set.notMember` freeVars b = beautify b
-
-  beautify (IsOne phi)  = toFun "IsOne" [phi]
-  beautify ItIsOne      = Ref (Bound (T.pack ".1=1") 0)
-
-  beautify (Lam Ex v (App Ex f (Ref v')))
-    | v == v', v `Set.notMember` freeVars f = f
-
-  beautify (Comp a I0 (System (Map.null -> True)) a0) = toFun "transp" [a, a0]
-  beautify (Lam _ _ (Lam _ _ (System (Map.null -> True)))) = System mempty
+showFace :: Map Head Bool -> Doc AnsiStyle
+showFace = hsep . map go . Map.toList where
+  go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
 
-  beautify (Partial phi a)    = toFun "Partial" [phi, a]
-  beautify (PartialP phi a)   = toFun "PartialP" [phi, a]
-  beautify (Comp a phi u a0)  = toFun "comp" [a, phi, u, a0]
-  beautify (HComp a phi u a0) = toFun "hcomp" [a, phi, u, a0]
-  beautify (Sub a phi u)      = toFun "Sub" [a, phi, u]
-  beautify (Inc _ _ u)        = toFun "inS" [u]
-  beautify (Ouc a phi u u0)   = toFun "outS" [a, phi, u, u0]
+prettyVl :: Value -> Doc AnsiStyle
+prettyVl = prettyTm . quote
 
-  beautify (GlueTy _ I1 (Lam _ _ a) _) = a
-  beautify (GlueTy a b c d) = toFun "Glue"   [a,b,c,d]
-  beautify (Glue a b c d e f) = toFun "glue"   [a,b,c,d,e,f]
-  beautify (Unglue a b c d e) = toFun "unglue" [a,b,c,d,e]
-  beautify x = x
+render :: Doc AnsiStyle -> Text
+render = L.toStrict . renderLazy . layoutSmart defaultLayoutOptions
 
-  toFun s a = foldl (App Ex) (Ref (Bound (T.pack ('.':s)) 0)) a
+arg_prec, fun_prec, dom_prec, and_prec, or_prec :: Int
+dom_prec = succ fun_prec
+arg_prec = succ and_prec
+and_prec = succ or_prec
+or_prec  = succ fun_prec
+fun_prec = 1
 
 keyword :: Doc AnsiStyle -> Doc AnsiStyle
 keyword = annotate (color Magenta)
 
 operator :: Doc AnsiStyle -> Doc AnsiStyle
-operator = annotate (color Yellow)
-
-parenArg :: Term -> Doc AnsiStyle
-parenArg x@App{} = parens (prettyTm x)
-parenArg x@IElim{} = parens (prettyTm x)
-parenArg x@IsOne{} = parens $ prettyTm x
-parenArg x@Partial{} = parens $ prettyTm x
-parenArg x@PartialP{} = parens $ prettyTm x
-
-parenArg x@Sub{} = parens $ prettyTm x
-parenArg x@Inc{} = parens $ prettyTm x
-parenArg x@Ouc{} = parens $ prettyTm x
-
-parenArg x@Comp{} = parens $ prettyTm x
-parenArg x@Case{} = parens $ prettyTm x
-
-parenArg x = prettyDom x
-
-prettyDom :: Term -> Doc AnsiStyle
-prettyDom x@Pi{}    = parens (prettyTm x)
-prettyDom x@Sigma{} = parens (prettyTm x)
-prettyDom x         = parenFun x
-
-parenFun :: Term -> Doc AnsiStyle
-parenFun x@Lam{} = parens $ prettyTm x
-parenFun x@PathIntro{} = parens $ prettyTm x
-parenFun x = prettyTm x
-
-render :: Doc AnsiStyle -> Text
-render = L.toStrict . renderLazy . layoutSmart defaultLayoutOptions
-
-showValue :: Value -> String
-showValue = L.unpack . renderLazy . layoutSmart defaultLayoutOptions . prettyTm . quote
-
-showFace :: Map Head Bool -> Doc AnsiStyle
-showFace = hsep . map go . Map.toList where
-  go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
-
-freeVars :: Term -> Set Name
-freeVars (Ref v) = Set.singleton v
-freeVars (App _ f x) = Set.union (freeVars f) (freeVars x)
-freeVars (Pi _ n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
-freeVars (Lam _ n x) = n `Set.delete` freeVars x
-freeVars (Let ns x) = Set.union (freeVars x `Set.difference` bound) freed where
-  bound = Set.fromList (map (\(x, _, _) -> x) ns)
-  freed = foldr (\(_, x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty ns
-freeVars Meta{} = mempty
-freeVars Con{} = mempty
-freeVars PCon{} = mempty
-freeVars Data{} = mempty
-freeVars Type{} = mempty
-freeVars Typeω{} = mempty
-freeVars I{} = mempty
-freeVars I0{} = mempty
-freeVars I1{} = mempty
-freeVars (Sigma n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
-freeVars (Pair x y) = Set.unions $ map freeVars [x, y]
-freeVars (Proj1 x) = Set.unions $ map freeVars [x]
-freeVars (Proj2 x) = Set.unions $ map freeVars [x]
-freeVars (IAnd x y) = Set.unions $ map freeVars [x, y]
-freeVars (IOr x y) = Set.unions $ map freeVars [x, y]
-freeVars (INot x) = Set.unions $ map freeVars [x]
-freeVars (PathP x y z) = Set.unions $ map freeVars [x, y, z]
-freeVars (IElim x y z a b) = Set.unions $ map freeVars [x, y, z, a, b]
-freeVars (PathIntro x y z a) = Set.unions $ map freeVars [x, y, z, a]
-freeVars (IsOne a) = Set.unions $ map freeVars [a]
-freeVars ItIsOne{} = mempty
-freeVars (Partial x y) = Set.unions $ map freeVars [x, y]
-freeVars (PartialP x y) = Set.unions $ map freeVars [x, y]
-freeVars (System fs) = foldr (\(x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty (Map.toList fs)
-
-freeVars (Sub x y z) = Set.unions $ map freeVars [x, y, z]
-freeVars (Inc x y z) = Set.unions $ map freeVars [x, y, z]
-freeVars (Ouc x y z a) = Set.unions $ map freeVars [x, y, z, a]
-
-freeVars (Comp x y z a) = Set.unions $ map freeVars [x, y, z, a]
-freeVars (HComp x y z a) = Set.unions $ map freeVars [x, y, z, a]
-
-freeVars (GlueTy x y z a) = Set.unions $ map freeVars [x, y, z, a]
-freeVars (Glue x y z a b c) = Set.unions $ map freeVars [x, y, z, a, b, c]
-freeVars (Unglue x y z a c) = Set.unions $ map freeVars [x, y, z, a, c]
-freeVars (Case rng x y) = freeVars rng <> freeVars x <> foldMap (\(_, _, y) -> freeVars y) y
+operator = annotate (color Yellow)
\ No newline at end of file
diff --git a/stack.yaml b/stack.yaml
index 60846eb..5169ef0 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,67 +1,5 @@
-# This file was automatically generated by 'stack init'
-#
-# Some commonly used options have been documented as comments in this file.
-# For advanced use and comprehensive documentation of the format, please see:
-# https://docs.haskellstack.org/en/stable/yaml_configuration/
-
-# Resolver to choose a 'specific' stackage snapshot or a compiler version.
-# A snapshot resolver dictates the compiler version and the set of packages
-# to be used for project dependencies. For example:
-#
-# resolver: lts-3.5
-# resolver: nightly-2015-09-21
-# resolver: ghc-7.10.2
-#
-# The location of a snapshot can be provided as a file or url. Stack assumes
-# a snapshot provided as a file might change, whereas a url resource does not.
-#
-# resolver: ./custom-snapshot.yaml
-# resolver: https://example.com/snapshots/2018-01-01.yaml
 resolver:
-  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
 
-# User packages to be built.
-# Various formats can be used as shown in the example below.
-#
-# packages:
-# - some-directory
-# - https://example.com/foo/bar/baz-0.0.2.tar.gz
-#   subdirs:
-#   - auto-update
-#   - wai
 packages:
-- .
-# Dependency packages to be pulled from upstream that are not in the resolver.
-# These entries can reference officially published versions as well as
-# forks / in-progress versions pinned to a git hash. For example:
-#
-# extra-deps:
-# - acme-missiles-0.3
-# - git: https://github.com/commercialhaskell/stack.git
-#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
-#
-# extra-deps: []
-
-# Override default flag values for local packages and extra-deps
-# flags: {}
-
-# Extra package databases containing global packages
-# extra-package-dbs: []
-
-# Control whether we use the GHC we find on the path
-# system-ghc: true
-#
-# Require a specific version of stack, using version ranges
-# require-stack-version: -any # Default
-# require-stack-version: ">=2.5"
-#
-# Override the architecture used by stack, especially useful on Windows
-# arch: i386
-# arch: x86_64
-#
-# Extra directories used by stack for building
-# extra-include-dirs: [/path/to/dir]
-# extra-lib-dirs: [/path/to/dir]
-#
-# Allow a newer minor version of GHC than the snapshot specifies
-# compiler-check: newer-minor
+- .
\ No newline at end of file
diff --git a/stack.yaml.lock b/stack.yaml.lock
index 0b2383c..2b156b1 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -6,8 +6,8 @@
 packages: []
 snapshots:
 - completed:
-    size: 563098
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
-    sha256: 395775c03e66a4286f134d50346b0b6f1432131cf542886252984b4cfa5fef69
+    size: 565720
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
+    sha256: 76bf8992ff8dfe6eda9c02f81866138c2369344d5011ab39ae403457c4448b03
   original:
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml