Check in more experiments I had locally

cubical.cabal

@@ -13,11 +13,6 @@ 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
@@ -56,7 +51,4 @@ executable cubical
   build-tool-depends:  alex:alex >= 3.2.4 && < 4.0
                     ,  happy:happy >= 1.19.12 && < 2.0
 
-  ghc-options:         -Wall -Wextra -Wno-name-shadowing -rtsopts
-
-  if flag(release)
-    ghc-options:       -XCPP -DRELEASE
+  ghc-options:         -Wall -Wextra -Wno-name-shadowing -rtsopts

intro.tt

@@ -110,8 +110,28 @@ isContr A = (x : A) * ((y : A) -> Path x y)
 -- Using the connection \i j -> y.2 (iand i j), we can prove that
 -- singletons are contracible. Together with transport later on,
 -- we get the J elimination principle of paths.
+
+dropJ : {A : Type} {x : A} {y : A} (p : Path x y)
+     -> PathP (\i -> Path (p i) (p i)) refl refl
+dropJ p i j = p i
+
+dropI : {A : Type} {x : A} {y : A} (p : Path x y)
+     -> PathP (\i -> Path x y) p p
+dropI p i j = p j
+
+and : {A : Type} {x : A} {y : A} (p : Path x y)
+   -> PathP (\i -> Path x (p i)) refl p
+and p i j = p (iand i j)
+
+or : {A : Type} {x : A} {y : A} (p : Path x y)
+  -> PathP (\i -> Path (p i) y) p refl
+or p i j = p (ior i j)
+
+
 singContr : {A : Type} {a : A} -> isContr (Singl A a)
-singContr = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))
+singContr = ((a, \i -> a), contr) where
+  contr : (y : Singl A a) -> PathP (\i -> Singl A a) (a, \i -> a) y
+  contr y i = (y.2 i, and y.2 i)
 
 -- Some more operations on paths. By rearranging parentheses we get a
 -- proof that the images of equal elements are themselves equal.
@@ -298,6 +318,22 @@ transFiller : {A : Type} {x : A} {y : A} {z : A}
            -> 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
 
+transFiller' : {A : Type} {x : A} {y : A} {z : A}
+            -> (p : Path x y) (q : Path y z)
+            -> PathP (\i -> Path (p (inot i)) z) q (trans {A} {x} {y} {z} p q)
+transFiller' p q j i = hcomp (\k [ (i = i0) -> p (inot j)
+                                 , (i = i1) -> q k
+                                 , (j = i0) -> q (iand i k) ])
+                             (inS (p (ior i (inot j))))
+
+transAssoc : {A : Type} {w : A} {x : A} {y : A} {z : A} (p : Path w x) (q : Path x y) (r : Path y z)
+          -> Path (trans p (trans q r)) (trans (trans p q) r)
+transAssoc p q r k = trans (transFiller p q k) (transFiller' q r (inot k))
+
+dubcomp : {A : Type} {a : A} {b : A} {c : A} {d : A}
+      -> Path a b -> Path b c -> Path c d -> Path a d
+dubcomp p q r i = hcomp (\j [ (i = i0) -> p (inot j), (i = i1) -> r j ]) (inS (q i))
+
 -- For instance, the filler of the previous composition square
 -- tells us that trans p refl = p:
 
@@ -697,14 +733,14 @@ trueNotFalse p = transp (\i -> if (Bool -> Bool) Bottom (p i)) id
 
 -- To be an h-Set is to have no "higher path information". Alternatively,
 --
--- isHSet A = (x : A) (y : A) -> isHProp (Path x y)
+-- isSet A = (x : A) (y : A) -> isHProp (Path x y)
 --
 
 isProp : Type -> Type
 isProp A = (x : A) (y : A) -> Path x y
 
-isHSet : Type -> Type
-isHSet A = (x : A) (y : A) -> isProp (Path x y)
+isSet : Type -> Type
+isSet A = (x : A) (y : A) -> isProp (Path x y)
 
 -- We can prove *a* contradiction (note: this is a direct proof!) by adversarially
 -- choosing two paths p, q that we know are not equal. Since "equal" paths have
@@ -714,7 +750,7 @@ isHSet A = (x : A) (y : A) -> isProp (Path x y)
 -- Since transp notp = not but transp refl = id, that's what we go with. The choice
 -- of false as the point x is just from the endpoints of trueNotFalse.
 
-universeNotSet : isHSet Type -> Bottom
+universeNotSet : isSet Type -> Bottom
 universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs Bool Bool notp refl i j) false)
 
 -- Funext is an inverse of happly
@@ -772,12 +808,13 @@ zeroNotSucc p = transp (\i -> fun (p i)) (p i0) where
     zero -> Nat
     succ x -> Bottom
 
+pred : Nat -> Nat
+pred = \case
+  zero -> zero
+  succ x -> x
+
 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
+succInj p i = pred (p i)
 
 -- The type of integers can be defined as A + B, where "pos n" means +n
 -- and "neg n" means -(n + 1).
@@ -894,8 +931,11 @@ helix = \case
 loopP : Path base base
 loopP i = loop i
 
+encode : (x : S1) -> Path base x -> helix x
+encode x p = subst helix p (pos zero)
+
 winding : Path base base -> Int
-winding p = transp (\i -> helix (p i)) (pos zero)
+winding = encode base
 
 -- For instance, going around the loop once has a winding number of +1,
 
@@ -917,17 +957,20 @@ windingBase = refl
 goAround : Int -> Path base base
 goAround =
   \case
-    pos n -> forwards n
-    neg n -> backwards n
-  where
-    forwards : Nat -> Path base base
-    forwards = \case
-      zero -> refl
-      succ n -> trans (goAround (pos n)) (\i -> loop i)
-    backwards : Nat -> Path base base
-    backwards = \case
-      zero -> \i -> loop (inot i)
-      succ n -> trans (goAround (neg n)) (\i -> loop (inot i))
+    pos n ->
+      let
+        forwards : Nat -> Path base base
+        forwards = \case
+          zero -> refl
+          succ n -> trans (goAround (pos n)) (\i -> loop i)
+      in forwards n
+    neg n ->
+      let
+        backwards : Nat -> Path base base
+        backwards = \case
+          zero -> \i -> loop (inot i)
+          succ n -> trans (goAround (neg n)) (\i -> loop (inot i))
+      in backwards n
 
 windingGoAround : (n : Int) -> Path (winding (goAround n)) n
 windingGoAround =
@@ -944,15 +987,40 @@ windingGoAround =
       zero -> refl
       succ n -> ap predZ (negCase n)
 
-decodeSquare : (n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n)
-decodeSquare = \case
-    pos n -> posCase n
-    neg n -> \i j -> hfill (\k [ (j = i1) -> loop (inot k), (j = i0) -> base ]) (inS (goAround (neg n) j)) (inot i)
-  where
-    posCase : (n : Nat) -> PathP (\i -> Path base (loop i)) (goAround (predZ (pos n))) (goAround (pos n))
-    posCase = \case
-      zero -> \i j -> loop (ior i (inot j))
-      succ n -> \i j -> hfill (\k [ (j = i1) -> loop k, (j = i0) -> base ]) (inS (goAround (pos n) j)) i
+decode : (x : S1) -> helix x -> Path base x
+decode = go decodeSquare where
+  decodeSquare : (n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n)
+  decodeSquare =
+    \case
+      pos n -> posCase n
+      neg n -> \i j -> hfill (\k [ (j = i1) -> loop (inot k), (j = i0) -> base ]) (inS (goAround (neg n) j)) (inot i)
+    where
+      posCase : (n : Nat) -> PathP (\i -> Path base (loop i)) (goAround (predZ (pos n))) (goAround (pos n))
+      posCase = \case
+        zero -> \i j -> loop (ior i (inot j))
+        succ n -> \i j -> hfill (\k [ (j = i1) -> loop k, (j = i0) -> base ]) (inS (goAround (pos n) j)) i
+
+  go : ((n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n))
+    -> (x : S1) -> helix x -> Path base x
+  go decodeSquare = \case
+    base -> goAround
+    loop i -> \y j ->
+      let n : Int
+          n = primUnglue {Int} {ior i (inot i)} {\o -> Int} {\[ (i = i1) -> idEquiv, (i = i0) -> sucEquiv ]} y
+      in hcomp (\k [ (i = i0) -> goAround (predSucZ y k) j
+                   , (i = i1) -> goAround y j
+                   , (j = i0) -> base
+                   , (j = i1) -> loop i ])
+               (inS (decodeSquare n i j))
+
+decodeWinding : (x : S1) (p : Path base x) -> Path (decode x (encode x p)) p
+decodeWinding x p = J (\y q -> Path (decode y (encode y q)) q) (\ i -> refl) p
+
+loopS1IsoInt : Iso (Path base base) Int
+loopS1IsoInt = (winding, goAround, windingGoAround, decodeWinding base)
+
+LoopS1IsInt : Path (Path base base) Int
+LoopS1IsInt = IsoToId loopS1IsoInt
 
 -- One particularly general higher inductive type is the homotopy pushout,
 -- which can be seen as a kind of sum B + C with the extra condition that
@@ -963,8 +1031,19 @@ data Pushout {A : Type} {B : Type} {C : Type} (f : A -> B) (g : A -> C) : Type w
   inr : (y : C) -> Pushout f g
   push i : (a : A) -> Pushout f g [ (i = i0) -> inl (f a), (i = i1) -> inr (g a) ]
 
--- The name is due to the category-theoretical notion of pushout.
--- TODO: finish writing this tomorrow lol
+Coproduct : Type -> Type -> Type
+Coproduct A B = Pushout {Bottom} {A} {B} absurd absurd
+
+Pushout_rec : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : A -> C}
+           -> (P : Pushout f g -> Type)
+           -> (fc : (x : B) -> P (inl x))
+           -> (gc : (x : C) -> P (inr x))
+           -> ((a : A) -> PathP (\i -> P (push a i)) (fc (f a)) (gc (g a)))
+           -> (c : Pushout f g) -> P c
+Pushout_rec P fc gc pc = \case
+  inl x -> fc x
+  inr y -> gc y
+  push c i -> pc c i
 
 data Susp (A : Type) : Type where
   north : Susp A
@@ -980,6 +1059,11 @@ unitEta = \case tt -> refl
 unitContr : isContr Unit
 unitContr = (tt, \x -> sym (unitEta x))
 
+unitProp : isProp Unit
+unitProp = \case
+  tt -> \case
+    tt -> refl
+
 poSusp : Type -> Type
 poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt)
 
@@ -1093,6 +1177,15 @@ boolAnd = \case
     true -> false
     false -> false
 
+boolXor : Bool -> Bool -> Bool
+boolXor = \case
+  true -> \case
+    true -> false
+    false -> true
+  false -> \case
+    false -> false
+    true -> true
+
 plusNat : Nat -> Nat -> Nat
 plusNat = \case
   zero -> \x -> x
@@ -1109,7 +1202,7 @@ multNat = \case
   succ n -> \x -> plusNat x (multNat n x)
 
 multInt : Int -> Int -> Int
-multInt x y = signify (multNat (abs x) (abs y)) (boolAnd (sign x) (sign y)) where
+multInt x y = signify (multNat (abs x) (abs y)) (not (boolXor (sign x) (sign y))) where
   signify : Nat -> Bool -> Int
   signify = \case
     zero -> \x -> pos zero
@@ -1133,7 +1226,7 @@ data Sq (A : Type) : Type where
   inc : A -> Sq A
   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 : {A : Type} -> isProp A -> isSet A
 isProp_isSet h a b p q j i =
   hcomp {A}
     (\k [ (i = i0) -> h a a k
@@ -1143,9 +1236,15 @@ isProp_isSet h a b p q j i =
         ])
     (inS a)
 
+unitSet : isSet Unit
+unitSet = isProp_isSet unitProp
+
 isProp_isProp : {A : Type} -> isProp (isProp A)
 isProp_isProp f g i a b = isProp_isSet f a b (f a b) (g a b) i
 
+isSet_isProp : {A : Type} -> isProp (isSet A)
+isSet_isProp f g i x y = isProp_isProp {_} (f x y) (g x y) i
+
 isProp_isContr : {A : Type} -> isProp (isContr A)
 isProp_isContr {A} z0 z1 j =
   ( z0.2 z1.1 j
@@ -1159,6 +1258,12 @@ isProp_isContr {A} z0 z1 j =
 isContr_isProp : {A : Type} -> isContr A -> isProp A
 isContr_isProp x a b i = hcomp (\k [ (i = i0) -> x.2 a k, (i = i1) -> x.2 b k ]) (inS x.1)
 
+isSet_prod : {A : Type} {B : Type} -> isSet A -> isSet B -> isSet (A * B)
+isSet_prod a b x y p q i j = (a x.1 y.1 (\i -> (p i).1) (\i -> (q i).1) i j, b x.2 y.2 (\i -> (p i).2) (\i -> (q i).2) i j)
+
+isSet_pi : {A : Type} {B : A -> Type} -> ((x : A) -> isSet (B x)) -> isSet ((x : A) -> B x)
+isSet_pi rng a b p q i j z = rng z (a z) (b z) (happly p z) (happly q z) i j
+
 sigmaPath : {A : Type} {B : A -> Type} {s1 : (x : A) * B x} {s2 : (x : A) * B x}
          -> (p : Path s1.1 s2.1)
          -> PathP (\i -> B (p i)) s1.2 s2.2
@@ -1314,17 +1419,18 @@ pathToEqS_K p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop 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 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
-    uipRefl x p = K {x} (\q -> Path refl q) refl p
+axK_to_isSet : {A : Type} -> ({x : A} -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p) -> isSet 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
+pathToEq_isSet : {A : Type} -> ({x : A} {y : A} -> Path x y -> Eq_s x y) -> isSet A
+pathToEq_isSet p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s)
+
+Nat_isSet : isSet Nat
 Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y)
 
-Bool_isSet : isHSet Bool
+Bool_isSet : isSet Bool
 Bool_isSet = pathToEq_isSet {Bool} (\{x} {y} -> p x y) where
   p : (x : Bool) (y : Bool) -> Path x y -> Eq_s x y
   p = \case
@@ -1362,17 +1468,16 @@ 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 f = (f base, \i -> f (loop 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, fro, ret, sec) where
+S1_univ = IsoToId {S1 -> X} {(a : X) * Path a a} (S1Map_to_baseLoop {X}, fro, ret, sec) where
   to = S1Map_to_baseLoop
   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
+  sec : (f : S1 -> X) -> Path (fro (to f)) f
+  sec f = funext {S1} {\s -> X} {\x -> fro (to f) x} {f} h where
     h : (x : S1) -> Path (fro (to f) x) (f x)
     h = \case
       base -> refl
@@ -1462,29 +1567,32 @@ isProp_isEquiv p q i y =
                     (inS (p2 w (ior i j)))
     )
 
-isProp_EqvSq : {P : Type} (x : Equiv P (Sq P)) (y : Equiv P (Sq P)) -> Path x y
-isProp_EqvSq x y = sigmaPath x1_is_y1 (isProp_isEquiv {P} {Sq P} {y.1} (transp (\i -> isEquiv (x1_is_y1 i)) x.2) y.2) where
-  x1_is_y1 : Path x.1 y.1
-  x1_is_y1 i e = sq (x.1 e) (y.1 e) i
+-- isProp_EqvSq : {P : Type} (x : Equiv P (Sq P)) (y : Equiv P (Sq P)) -> Path x y
+-- isProp_EqvSq x y = sigmaPath x1_is_y1 (isProp_isEquiv {P} {Sq P} {y.1} (transp (\i -> isEquiv (x1_is_y1 i)) x.2) y.2) where
+--   x1_is_y1 : Path x.1 y.1
+--   x1_is_y1 i e = sq (x.1 e) (y.1 e) i
 
 equivLemma : {A : Type} {B : Type} {e : Equiv A B} {e' : Equiv A B}
           -> Path e.1 e'.1
           -> Path e e'
-equivLemma p = sigmaPath p (isProp_isEquiv {A} {B} {e'.1} (transp (\i -> isEquiv (p i)) e.2) e'.2)
+equivLemma p = sigmaPath {A -> B} {\f -> isEquiv f} p (transp (\i -> PathP_is_Path (\i -> isEquiv (p i)) e.2 e'.2 (inot i)) (isProp_isEquiv {A} {B} {e'.1} _ _))
+
+isProp_equiv : {P : Type} {Q : Type} -> Equiv P Q -> isProp P -> isProp Q
+isProp_equiv eqv = transp (\i -> isProp (ua eqv i))
 
-isProp_to_Sq_equiv : {P : Type} -> isProp P -> Equiv P (Sq P)
-isProp_to_Sq_equiv prop = propExt prop sqProp inc proj where
-  proj : Sq P -> P
-  proj = Sq_rec prop (\x -> x)
+-- isProp_to_Sq_equiv : {P : Type} -> isProp P -> Equiv P (Sq P)
+-- isProp_to_Sq_equiv prop = propExt prop sqProp inc proj where
+--   proj : Sq P -> P
+--   proj = Sq_rec prop (\x -> x)
 
-  sqProp : isProp (Sq P)
-  sqProp x y i = sq x y i
+--   sqProp : isProp (Sq P)
+--   sqProp x y i = sq x y i
 
-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)
+-- 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 = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp
+-- exercise_3_21 : {P : Type} -> Equiv (isProp P) (Equiv P (Sq P))
+-- 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)
@@ -1500,15 +1608,24 @@ isContrRetract f g h v = (g b, p) where
   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)
+contrEquivSingl = isContrRetract (f1 ua idToEquiv) (f2 ua idToEquiv) (uaretSig ua idToEquiv (uaret {A})) singContr where
+  f1 : (ua : {B : Type} -> Equiv A B -> Path A B)
+       (idToEquiv : {B : Type} -> Path A B -> Equiv A B)
+       (p : (B : Type) * Equiv A B)
+    -> (B : Type) * Path A B
+  f1 ua idtoequiv p = (p.1, ua p.2)
+
+  f2 : (ua : {B : Type} -> Equiv A B -> Path A B)
+       (idToEquiv : {B : Type} -> Path A B -> Equiv A B)
+       (p : (B : Type) * Path A B)
+    -> (B : Type) * Equiv A B
+  f2 ua idtoequiv p = (p.1, idToEquiv p.2)
+
+  uaretSig : (ua : {B : Type} -> Equiv A B -> Path A B)
+             (idtoequiv : {B : Type} -> Path A B -> Equiv A B)
+             (uaret : {B : Type} (e : Equiv A B) -> Path (idToEquiv (ua e)) e)
+          -> (a : (B : Type) * Equiv A B) -> Path (f2 ua idtoequiv (f1 ua idtoequiv a)) a
+  uaretSig ua idtoequiv ret p i = (p.1, ret {p.1} p.2 i)
 
 curry : {A : Type} {B : A -> Type} {C : (x : A) -> B x -> Type}
      -> Path ((x : A) (y : B x) -> C x y) ((p : (x : A) * B x) -> C p.1 p.2)
@@ -1606,6 +1723,10 @@ 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_fun : {A : Type} {B : Type} (P : (A : Type) -> (A -> B) -> Type)
+          -> P B id -> (e : Equiv A B) -> P A e.1
+EquivJ_fun P r e = EquivJ_domain (\A e -> P A e.1) r e
+
 EquivJ_range : {X : Type} (P : (Y : Type) -> Equiv X Y -> Type)
             -> P X idEquiv
             -> {Y : Type} (E : Equiv X Y)
@@ -1633,6 +1754,21 @@ univalence = IsoToEquiv (pathToEquiv, ua, pathToEquiv_ua, ua_pathToEquiv) where
     lemma : (A : Type) -> Path (pathToEquiv (ua idEquiv)) idEquiv
     lemma A = transp (\i -> Path (pathToEquiv (uaIdEquiv {A} (inot i))) idEquiv) pathToEquiv_refl
 
+IsoJ : {B : Type} -> (Q : {A : Type} -> (A -> B) -> (B -> A) -> Type)
+    -> Q id id
+    -> {A : Type} (f : A -> B) (g : B -> A)
+    -> Path (\x -> g (f x)) id -> Path (\x -> f (g x)) id
+    -> Q f g
+IsoJ Q h f g sfg rfg = rem1 f g sfg rfg where
+  P : (A : Type) -> (A -> B) -> Type
+  P A f = (g : B -> A) -> Path (\x -> g (f x)) id -> Path (\x -> f (g x)) id -> Q f g
+
+  rem : P B id
+  rem g sfg rfg = subst (Q id) (\i b -> sfg (inot i) b) h
+
+  rem1 : {A : Type} (f : A -> B) -> P A f
+  rem1 f g sfg rfg = EquivJ_fun P rem (IsoToEquiv (f, g, \i x -> rfg x i, \i x -> sfg x i)) g sfg rfg
+
 total : {A : Type} {P : A -> Type} {Q : A -> Type}
      -> ((x : A) -> P x -> Q x)
      -> ((x : A) * P x) -> ((x : A) * Q x)
@@ -1703,16 +1839,65 @@ contrIsEquiv cA cB f y =
 
 theorem722 : {A : Type} {R : A -> A -> Type}
           -> ((x : A) (y : A) -> isProp (R x y))
-          -> ({x : A} -> R x x)
+          -> ((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 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))
+  rContr x = ((x, rho x), \y -> sigmaPath (toId _ _ y.2) (prop _ _ _ y.2))
 
   totalEquiv : (x : A) -> isEquiv (total (toId x))
   totalEquiv x = contrIsEquiv (rContr x) singContr (total (toId x))
 
+isSet_Coproduct : {A : Type} {B : Type} -> isSet A -> isSet B -> isSet (Coproduct A B)
+isSet_Coproduct setA setB = Req_isProp where
+  T = Coproduct A B
+
+  R : T -> T -> Type
+  R = \case
+    inl x -> \case
+      inl y -> Path x y
+      inr x -> Bottom
+      push c i -> absurd c
+    inr x -> \case
+      inl x -> Bottom
+      inr y -> Path x y
+      push c i -> absurd c c
+
+  R_prop : (x : T) (y : T) -> isProp (R x y)
+  R_prop = \case
+    inl x -> \case
+      inl y -> setA x y
+      inr y -> \p q -> absurd p
+      push c i -> absurd c
+    inr x -> \case
+      inl y -> \p q -> absurd p
+      inr y -> setB x y
+      push c i -> absurd c
+
+  R_refl : (x : T) -> R x x
+  R_refl = \case
+    inl x -> refl
+    inr x -> refl
+    push c i -> absurd c
+
+  R_impliesEq : (x : T) (y : T) -> R x y -> Path x y
+  R_impliesEq = \case
+    inl x -> \case
+      inl y -> \p -> ap inl p
+      inr y -> \p -> absurd p
+      push c i -> absurd c
+    inr x -> \case
+      inl y -> \p -> absurd p
+      inr y -> \p -> ap inr p
+      push c i -> absurd c
+  
+  Req_isEquiv : {x : T} {y : T} -> Equiv (R x y) (Path x y)
+  Req_isEquiv = (R_impliesEq x y, theorem722 R_prop R_refl R_impliesEq)
+
+  Req_isProp : (x : T) (y : T) -> isProp (Path x y)
+  Req_isProp x y = isProp_equiv {R x y} {Path x y} (Req_isEquiv {x} {y}) (R_prop x y)
+
 lemma492 : {A : Type} {B : Type} {X : Type}
         -> (e : Equiv A B)
         -> isEquiv {X -> A} {X -> B} (\f x -> e.1 (f x))
@@ -1830,10 +2015,10 @@ data nTrunc (A : Type) (n : Nat) : Type where
   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 : {n : Nat} {A : Type} -> 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}
+nTrunc_rec : {n : Nat} {A : Type} {B : Type}
           -> isOfHLevel B n
           -> (A -> B)
           -> nTrunc A n -> B
@@ -1847,4 +2032,296 @@ nTrunc_rec bofhl f = go (isOfHLevel_hasSpheres n bofhl) where
   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
+    spoke sph cell i -> (p (\x -> work p (sph x))).2 cell i
+
+nTrunc_lift : {A : Type} {B : Type} {n : Nat} -> (A -> B) -> nTrunc A n -> nTrunc B n
+nTrunc_lift f = nTrunc_rec (nTrunc_isOfHLevel {n} {B}) (\x -> incn {B} {n} (f x))
+
+-- data W (A : Type) (B : A -> Type) : Type where
+--   sup : (a : A) -> (B a -> W A B) -> W A B
+
+-- Welim : {A : Type} {B : A -> Type} (P : W A B -> Type)
+--      -> (sup : (a : A) (f : B a -> W A B) (g : (x : B a) -> P (f x)) -> P (sup a f))
+--      -> (c : W A B) -> P c
+-- Welim P k = \case
+--   sup a f -> k a f (\x -> Welim P k (f x))
+
+-- wnat : Type
+-- wnat = W Bool (if Unit Bottom)
+
+-- wzero : wnat
+-- wzero = sup false absurd
+
+-- wsucc : wnat -> wnat
+-- wsucc n = sup true (\x -> n)
+
+-- wnat_elim : (P : wnat -> Type) (pz : P wzero) (ps : (c : wnat) -> P c -> P (wsucc c)) -> (x : wnat) -> P x
+-- wnat_elim P pz ps x = Welim P (\a f g -> helper a f g) x where
+--   A = Bool
+--   B = if Unit Bottom
+
+--   helper : (a : A) (f : B a -> W A B) (g : (x : B a) -> P (f x)) -> P (sup a f)
+--   helper = \case
+--     false -> \f g -> pz
+--     true -> \f g ->
+--       let
+--         t : P (sup true (\x -> f tt))
+--         t = ps (f tt) (g tt)
+--       in transp (\i -> P (sup true (\x -> f (unitEta x (inot i))))) t
+
+-- nat_is_wnat : Path Nat wnat
+-- nat_is_wnat = IsoToId (to, from, toFrom, fromTo) where
+--   to : Nat -> wnat
+--   to = Nat_elim (\x -> wnat) wzero (\_ x -> wsucc x)
+
+--   from : wnat -> Nat
+--   from = wnat_elim (\x -> Nat) zero (\_ x -> succ x)
+
+--   toFrom : (y : wnat) -> Path (to (from y)) y
+--   toFrom = wnat_elim (\x -> Path (to (from x)) x) refl (\x y -> ap wsucc y)
+
+--   fromTo : (x : Nat) -> Path (from (to x)) x
+--   fromTo = Nat_elim (\x -> Path (from (to x)) x) refl (\x y -> ap succ y)
+
+-- plusWnat : wnat -> wnat -> wnat
+-- plusWnat = subst (\x -> x -> x -> x) nat_is_wnat plusNat
+
+-- Pointed : Type
+-- Pointed = (X : Type) * X * isSet X
+
+-- Set : Type
+-- Set = (X : Type) * isSet X
+
+-- map : Set -> Set -> Type
+-- map A B = A.1 -> B.1
+
+-- pmap : Pointed -> Pointed -> Type
+-- pmap A B = (f : A.1 -> B.1) * Path (f A.2.1) B.2.1
+
+-- Zero : Pointed
+-- Zero = (Unit, tt, isProp_isSet l) where
+--   l : (a : Unit) (b : Unit) -> Path a b
+--   l = \case
+--     tt -> \case
+--       tt -> refl
+
+-- compose : {A : Pointed} {B : Pointed} {C : Pointed} -> pmap B C -> pmap A B -> pmap A C
+-- compose g f = (\x -> g.1 (f.1 x), subst (\x -> Path (g.1 x) C.2.1) (sym f.2) g.2)
+
+-- id : {A : Pointed} -> pmap A A
+-- id = (\x -> x, refl)
+
+-- initial : {A : Pointed} -> pmap Zero A
+-- initial = (\_ -> A.2.1, refl)
+
+-- terminal : {A : Pointed} -> pmap A Zero
+-- terminal = (\_ -> tt, refl)
+
+-- cast : {A : Pointed} {B : Pointed} -> pmap A B
+-- cast = compose {A} {Zero} {B} (initial {B}) (terminal {A})
+
+-- Product : Pointed -> Pointed -> Pointed
+-- Product A B = (A.1 * B.1, (A.2.1, B.2.1), isSet_prod A.2.2 B.2.2)
+
+-- proj1 : {A : Pointed} {B : Pointed} -> pmap (Product A B) A
+-- proj1 = (\x -> x.1, refl)
+
+-- proj2 : {A : Pointed} {B : Pointed} -> pmap (Product A B) B
+-- proj2 = (\x -> x.2, refl)
+
+-- cross : {G : Pointed} {A : Pointed} {B : Pointed} -> pmap G A -> pmap G B -> pmap G (Product A B)
+-- cross f g = (\x -> (f.1 x, g.1 x), \i -> (f.2 i, g.2 i))
+
+-- inj1 : {A : Pointed} {B : Pointed} -> pmap A (Product A B)
+-- inj1 = cross {A} {A} {B} (id {A}) (cast {A} {B})
+
+-- inj2 : {A : Pointed} {B : Pointed} -> pmap B (Product A B)
+-- inj2 = cross {B} {A} {B} (cast {B} {A}) (id {B})
+
+-- pmap_equal : {A : Pointed} {B : Pointed} (f : pmap A B) (g : pmap A B) -> Path f.1 g.1 -> Path f g
+-- pmap_equal f g p = sigmaPath {A.1 -> B.1} {\f -> Path (f A.2.1) B.2.1} p (transp (\i -> PathP_is_Path (\i -> Path (p i A.2.1) B.2.1) f.2 g.2 (inot i)) (B.2.2 _ _ _ _))
+
+-- zero_comp : {A : Pointed} {B : Pointed} {C : Pointed} (f : pmap B C)
+--          -> Path (compose {A} {B} {C} f (cast {A} {B})) (cast {A} {C})
+-- zero_comp f = pmap_equal {A} {C} _ _ (\i x -> f.2 i)
+
+-- Forget : Pointed -> Set
+-- Forget P = (P.1, P.2.2)
+
+-- Free : Set -> Pointed
+-- Free P = (Coproduct P.1 Unit, inr tt, Coproduct_isSet P.2 unitSet)
+
+Precategory : Type
+Precategory = (Ob      : Type)
+            * (Hom     : Ob -> Ob -> Type)
+            * (hset    : (A : Ob) (B : Ob) -> isSet (Hom A B))
+            * (id      : {A : Ob} -> Hom A A)
+            * (compose : {A : Ob} {B : Ob} {C : Ob} -> Hom B C -> Hom A B -> Hom A C)
+            * (idl     : {A : Ob} {B : Ob} (f : Hom A B) -> Path (compose id f) f)
+            * (idr     : {A : Ob} {B : Ob} (f : Hom A B) -> Path (compose f id) f)
+            * ({A : Ob} {B : Ob} {C : Ob} {D : Ob}
+            -> (f : Hom C D) (g : Hom B C) (h : Hom A B)
+            -> Path (compose f (compose g h)) (compose (compose f g) h))
+
+Ob : (C : Precategory) -> Type
+Ob C = C.1
+
+Hom : (C : Precategory) -> Ob C -> Ob C -> Type
+Hom C = C.2.1
+
+homSet : {C : Precategory} (A : Ob C) (B : Ob C) -> isSet (Hom C A B)
+homSet = C.2.2.1
+
+Cid : (C : Precategory) {A : Ob C} -> Hom C A A
+Cid C = C.2.2.2.1
+
+compose : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat} {C : Ob Cat}
+       -> Hom Cat B C -> Hom Cat A B -> Hom Cat A C
+compose = Cat.2.2.2.2.1
+
+leftId : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat}
+      -> (f : Hom Cat A B) -> Path (compose {Cat} (Cid Cat) f) f
+leftId = Cat.2.2.2.2.2.1
+
+rightId : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat}
+       -> (f : Hom Cat A B) -> Path (compose {Cat} f (Cid Cat)) f
+rightId = Cat.2.2.2.2.2.2.1
+
+assocCompose : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat} {C : Ob Cat} {D : Ob Cat}
+            -> (f : Hom Cat C D) (g : Hom Cat B C) (h : Hom Cat A B)
+            -> Path (compose {Cat} f (compose {Cat} g h)) (compose {Cat} (compose {Cat} f g) h)
+assocCompose = Cat.2.2.2.2.2.2.2
+
+Opposite : Precategory -> Precategory
+Opposite Cat =
+  ( Cat.1
+  , \A B -> Cat.2.1 B A
+  , \A B -> Cat.2.2.1 B A
+  , Cat.2.2.2.1
+  , \f g -> compose {Cat} g f
+  , \f -> rightId {Cat} f
+  , \f -> leftId {Cat} f
+  , \f g h i -> assocCompose {Cat} h g f (inot i)
+  )
+
+Coprod : {Cat : Precategory} -> Ob Cat -> Ob Cat -> Type
+Coprod A B = (sum : Ob Cat)
+           * (inl  : Hom Cat A sum)
+           * (inr  : Hom Cat B sum)
+           * (elim : {S : Ob Cat} -> Hom Cat A S -> Hom Cat B S -> Hom Cat sum S)
+           * (eliml : {S : Ob Cat} (f : Hom Cat A S) (g : Hom Cat B S)
+                   -> Path (compose {Cat} (elim f g) inl) f)
+           * ({S : Ob Cat} (f : Hom Cat A S) (g : Hom Cat B S)
+              -> Path (compose {Cat} (elim f g) inr) g)
+
+Product : {Cat : Precategory} -> Ob Cat -> Ob Cat -> Type
+Product = Coprod {Opposite Cat}
+
+Set : Precategory
+Set = (T, \A B -> A.1 -> B.1, homset, \x -> x, \g f x -> g (f x), \f -> refl, \f -> refl, \f g h -> refl) where
+  T = (X : Type) * isSet X
+
+  homset : (A : T) (B : T) -> isSet (A.1 -> B.1)
+  homset A B = isSet_pi (\_ -> B.2)
+
+nat : Ob Set
+nat = (Nat, Nat_isSet)
+
+setCoprod : (A : Ob Set) (B : Ob Set) -> Coprod {Set} A B
+setCoprod A B = (T, inl, inr, elim, \f g i x -> f x, \f g i x -> g x) where
+  T : Ob Set
+  T = (Coproduct A.1 B.1, isSet_Coproduct A.2 B.2)
+
+  elim : {S : Ob Set} -> Hom Set A S -> Hom Set B S -> Hom Set T S
+  elim f g = \case
+    inl x -> f x
+    inr x -> g x
+    push c i -> absurd c
+
+setProd : (A : Ob Set) (B : Ob Set) -> Product {Set} A B
+setProd A B = (T, \x -> x.1, \x -> x.2, \{S} -> cross {S}, \f g i -> f, \f g i -> g) where
+  T : Ob Set
+  T = (A.1 * B.1, isSet_prod A.2 B.2)
+
+  cross : {S : Ob Set} -> Hom Set S A -> Hom Set S B -> Hom Set S T
+  cross f g x = (f x, g x)
+
+isIsoHom : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat} -> Hom Cat A B -> Type
+isIsoHom f = (inv : Hom Cat B A) * Path (compose {Cat} f inv) (Cid Cat) * Path (compose {Cat} inv f) (Cid Cat)
+
+Isomorphism : {Cat : Precategory} -> Ob Cat -> Ob Cat -> Type
+Isomorphism A B = (f : Hom Cat A B) * isIsoHom {Cat} {A} {B} f
+
+isCategory : Precategory -> Type
+isCategory Cat = (A : Ob Cat) (B : Ob Cat) -> Equiv (Path A B) (Isomorphism {Cat} A B)
+
+-- setIsCategory : isCategory Set
+-- setIsCategory A B = IsoToEquiv (pathTo, fromIso, pathTo_fromIso, _) where
+--   pathTo : Path A B -> Isomorphism {Set} A B
+--   pathTo = J {Ob Set} {A} (\B _ -> Isomorphism {Set} A B) (id, id, refl, refl)
+-- 
+--   augment : Path A.1 B.1 -> Path A B
+--   
+--   fromIso : Isomorphism {Set} A B -> Path A B
+--   fromIso iso = augment (IsoJ (\{A} f g -> Path A B.1) refl iso.1 iso.2.1 iso.2.2.2 iso.2.2.1)
+-- 
+--   augment p = sigmaPath {Type} {isSet} p (transp (\i -> PathP_is_Path (\j -> isSet (p j)) A.2 B.2 (inot i)) (isSet_isProp {B.1} (transp (\i -> isSet (p i)) A.2) B.2))
+-- 
+--   pathTo_fromIso : (i : Isomorphism {Set} A B) -> Path (pathTo (fromIso i)) i
+--   pathTo_fromIso iso i = (iso.1, iso.2.1, iso.2.2.1, iso.2.2.2)
+
+sym_subst : {A : Type} {x : A} {y : A} -> Path x y -> Path y x
+sym_subst p = subst (\y -> Path y x) p refl
+
+trans_subst : {A : Type} {x : A} {y : A} {z : A} -> Path x y -> Path y z -> Path x z
+trans_subst p q = subst (\y -> Path y z -> Path x z) p id q
+
+data Unlist (A : Type) : Type where
+  uncons : A -> Unlist A -> Unlist A
+
+unelim : {A : Type}
+         (P : Unlist A -> Type)
+      -> ((x : A) (tail : Unlist A) -> P tail -> P (uncons x tail))
+      -> (x : Unlist A) -> P x
+unelim P c = \case
+  uncons x xs -> c x xs (unelim P c xs)
+
+contra : {A : Type} -> Unlist A -> Bottom
+contra = unelim (\x -> Bottom) (\_ _ x -> x)
+
+plusInt : Int -> Int -> Int
+plusInt x y = winding (trans (goAround x) (goAround y))
+
+add : Nat -> Nat -> Nat
+add = Nat_elim (\ _ -> Nat -> Nat) (\ x -> x) (\n k x -> succ (k x))
+
+addAssoc : (i : Nat) (j : Nat) (k : Nat) -> Path (add i (add j k)) (add (add i j) k)
+addAssoc = Nat_elim (\ i -> (j : Nat) (k : Nat) -> Path (add i (add j k)) (add (add i j) k)) (\j k -> refl) (\n assoc j k -> ap succ (assoc j k))
+
+Jsym : {A : Type} {x : A} {y : A} -> Path x y -> Path y x
+Jsym = J (\y _ -> Path y x) refl
+
+Vect : Type -> Nat -> Type
+Vect A = \case
+  zero -> Unit
+  succ n -> A * Vect A n
+
+Vect_elim : {A : Type} (P : {n : Nat} -> Vect A n -> Type)
+         -> P {zero} tt
+         -> ({n : Nat} (x : A) (xs : Vect A n) -> P {n} xs -> P {succ n} (x, xs))
+         -> {n : Nat} (x : Vect A n) -> P {n} x
+Vect_elim P nil cons {n} x = go n x where
+  go : (n : Nat) (x : Vect A n) -> P x
+  go = \case
+    zero -> \case
+      tt -> nil
+    succ n -> \xs -> cons {n} xs.1 xs.2 (go n xs.2)
+
+head : {A : Type} {n : Nat} -> Vect A (succ n) -> A
+head xs = xs.1
+
+tail : {A : Type} {n : Nat} -> Vect A (succ n) -> Vect A n
+tail xs = xs.2
+
+equivToIso : {A : Type} {B : Type} (f : A -> B) -> isEquiv f -> isIso f
+equivToIso f e = EquivJ (\X Y f -> isIso f.1) (\x -> (id, \x -> refl, \x -> refl)) (f, e)

src/Elab/Eval.hs

@@ -208,11 +208,11 @@ evalCase env rng (VHComp a φ u u0) cases =
 
 evalCase env _ sc ((Ref _, _, k):_) = eval' env k @@ sc
 
-evalCase env rng (val@(VNe (HCon _ x) sp)) ((Con x', _, k):xs)
+evalCase env rng (force -> val@(VNe (HCon _ x) sp)) ((Con x', _, k):xs)
   | x == x'   = foldl applProj (eval' env k) sp
   | otherwise = evalCase env rng val xs
 
-evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
+evalCase env rng (force -> val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
   | x == x'   = foldl applProj (eval' env k) sp
   | otherwise = evalCase env rng val xs
 
@@ -490,6 +490,10 @@ _nameCounter = unsafePerformIO $ newIORef 0
 solveMeta :: MV -> Seq Projection -> Value -> ElabM ()
 solveMeta m Seq.Empty (VNe (HMeta m') Seq.Empty) | m == m' = pure ()
 solveMeta m@(mvCell -> cell) sp rhs = do
+  when (mvName m == T.pack "2801") do
+    traceM (VNe (HMeta m) sp)
+    traceM rhs
+
   env <- ask
   names <- tryElab $ checkSpine Set.empty sp
   case names of
@@ -600,11 +604,6 @@ substituteIO sub = substituteIO . force where
   substituteIO (VNe hd sp) = do
     sp' <- traverse (substituteSp sub) sp
     case hd of
-      HMeta (mvCell -> cell) -> do
-        solved <- liftIO $ readIORef cell
-        case solved of
-          Just vl -> substituteIO $ foldl applProj vl sp'
-          Nothing -> pure $ VNe hd sp'
       HVar v ->
         case Map.lookup v sub of
           Just vl -> substituteIO $ foldl applProj vl sp'
@@ -706,6 +705,7 @@ applProj fun PProj2           = vProj2 fun
 
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
 vApp _ (VLam _ k) arg = clCont k arg
+vApp p (VNe (HData True n) _) _ | T.unpack (getNameText n) == "S1" = undefined
 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 = mkVSystem (fmap (flip (vApp p) arg) fs)
@@ -727,7 +727,7 @@ vProj1 (VSystem fs) = VSystem (fmap vProj1 fs)
 vProj1 (VInc (VSigma a _) b c) = incS a b (vProj1 c)
 vProj1 (VCase env rng sc branches) =
   VCase env rng sc (map (projIntoCase Proj1) branches)
-vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x))
+vProj1 x = error $ "can't proj1 " ++ show x
 
 vProj2 :: HasCallStack => Value -> Value
 vProj2 (VPair _ b) = b

src/Elab/WiredIn.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE KindSignatures #-}
+{-# OPTIONS_GHC -fno-full-laziness #-}
 module Elab.WiredIn
        ( wiType
        , wiValue
@@ -54,7 +55,7 @@ import qualified Presyntax.Presyntax as P
 import Syntax.Pretty (prettyTm, prettyVl)
 import Syntax
 
-import System.IO.Unsafe
+import System.IO.Unsafe ( unsafePerformIO )
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -342,11 +343,11 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
         ts isone = mkVSystem . Map.fromList $ [(del, t1'), (psi, (b @@ VI1 @@ isone))]
         ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))]
 
-        a1 = gcomp
+        a1 = comp
               (fun (const (base VI1)))
               (del `ior` psi)
               (system \j _u -> mkVSystem (Map.fromList [ (del, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)
-                                                       , (psi, a VI1 (VReflStrict VI VI1))
+                                                       , (psi, a psi _u)
                                                        ]))
               (incS (base VI1) (phi VI1 `ior` psi) a1')
         b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) (incS (base VI1) (ior (del `ior` psi) (inot del `iand` inot psi)) a1)
@@ -367,17 +368,13 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
     _ -> VComp a phi u (incS (a @@ VI0) phi a0)
   where
     {-# NOINLINE name #-}
+    name :: Name
     name = unsafePerformIO newName
 
     {-# NOINLINE equivVar #-}
+    equivVar :: Name
     equivVar = unsafePerformIO newName
 
-gcomp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
-gcomp a phi u a0 =
-  comp a (ior phi (inot phi))
-         (system \i is1 -> mkVSystem $ Map.fromList [ (phi, u @@ i @@ is1)
-                                                    , (inot phi, outS (a @@ VI0) phi (u @@ VI0) a0) ])
-         a0
 
 mapVSystem :: (Value -> Value) -> Value -> Value
 mapVSystem f (VSystem fs) = VSystem (fmap f fs)

src/Main.hs

@@ -215,9 +215,9 @@ displayExceptions lines =
         endp = case ep of
           VI0 -> Lt.pack "left"
           VI1 -> Lt.pack "right"
-          _ -> render . prettyTm $ quote ep
-        left = render (prettyTm (quote le))
-        right = render (prettyTm (quote ri))
+          _ -> render . prettyTm $ quoteWith False mempty ep
+        left = render (prettyTm (quoteWith False mempty le))
+        right = render (prettyTm (quoteWith False mempty ri))
       Lt.putStrLn . Lt.unlines $
         [ "\n\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram <<"
         , "\t " <> redact left <> " " <> Lt.replicate 7 (Lt.singleton '\x2500') <> " " <> redact right

src/Presyntax/Lexer.x

@@ -183,4 +183,4 @@ laidOut x l c = do
   mapUserState $ \s -> s { leastColumn = c }
   pure (Token x l c)
 
-}
+}

src/Syntax.hs

@@ -193,8 +193,8 @@ data Value
 pattern VVar :: Name -> Value
 pattern VVar x = VNe (HVar x) Seq.Empty
 
-quoteWith :: Set Name -> Value -> Term
-quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
+quoteWith :: Bool -> Set Name -> Value -> Term
+quoteWith short names (VNe h sp) = foldl goSpine (goHead h) sp where
   goHead (HVar v)    = Ref v
   goHead (HMeta m)   = Meta m
   goHead (HCon _ v)  = Con v
@@ -208,7 +208,7 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
       s -> constantly (length sp) s
   goHead (HData x v) = Data x v
 
-  goSpine t (PApp p v) = App p t (quoteWith names v)
+  goSpine t (PApp p v) = App p t (quoteWith short 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
@@ -216,69 +216,69 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
   goSpine t PProj2 = Proj2 t
   goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t
 
-  constantly 0 n = quoteWith names n
+  constantly 0 n = quoteWith short names n
   constantly k x = Lam Ex (Bound (T.pack "x") (negate 1)) $ constantly (k - 1) x
 
-quoteWith names (GluedVl _ Seq.Empty x) = quoteWith names x
+quoteWith short names (GluedVl _ Seq.Empty x) = quoteWith short names x
 
-quoteWith names (GluedVl h sp (VLam p (Closure n k))) =
-  quoteWith names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a))))
+quoteWith short names (GluedVl h sp (VLam p (Closure n k))) =
+  quoteWith short names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a))))
 
-quoteWith names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) =
-  quoteWith names (VLine ty x y (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PIElim ty x y a) (k a)))))
+quoteWith short names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) =
+  quoteWith short names (VLine ty x y (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PIElim ty x y a) (k a)))))
 
-quoteWith names (GluedVl h sp vl)
-  | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
-  | True || alwaysShort vl = quoteWith names vl
+quoteWith short names (GluedVl h sp vl)
+  | GluedVl _ _ inner <- vl = quoteWith short names (GluedVl h sp inner)
+  | short || alwaysShort vl = quoteWith short names vl
   | _ Seq.:|> PIElim _ x y i <- sp =
     case i of
-      VI0 -> quoteWith names x
-      VI1 -> quoteWith names y
-      _ -> quoteWith names (VNe h sp)
-  | otherwise = quoteWith names (VNe h sp)
+      VI0 -> quoteWith short names x
+      VI1 -> quoteWith short names y
+      _ -> quoteWith short names (VNe h sp)
+  | otherwise = quoteWith short names (VNe h sp)
 
-quoteWith names (VLam p (Closure n k)) =
+quoteWith short names (VLam p (Closure n k)) =
   let n' = refresh Nothing names n
-   in Lam p n' (quoteWith (Set.insert n' names) (k (VVar n')))
+   in Lam p n' (quoteWith short (Set.insert n' names) (k (VVar n')))
 
-quoteWith names (VPi p d (Closure n k)) =
+quoteWith short names (VPi p d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
+   in Pi p n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
 
-quoteWith names (VSigma d (Closure n k)) =
+quoteWith short names (VSigma d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
+   in Sigma n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
 
-quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
-quoteWith _ VType = Type
-quoteWith _ VTypeω = Typeω
+quoteWith short names (VPair a b) = Pair (quoteWith short names a) (quoteWith short names b)
+quoteWith _ _ VType = Type
+quoteWith _ _ VTypeω = Typeω
 
-quoteWith _ VI     = I
-quoteWith _ VI0    = I0
-quoteWith _ VI1    = I1
-quoteWith names (VIAnd x y) = IAnd (quoteWith names x) (quoteWith names y)
-quoteWith names (VIOr x y) = IOr (quoteWith names x) (quoteWith names y)
-quoteWith names (VINot x) = INot (quoteWith names x)
+quoteWith _ _ VI     = I
+quoteWith _ _ VI0    = I0
+quoteWith _ _ VI1    = I1
+quoteWith short names (VIAnd x y) = IAnd (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VIOr x y) = IOr (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VINot x) = INot (quoteWith short names x)
 
-quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
-quoteWith names (VLine p x y f)  = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
+quoteWith short names (VPath line x y) = PathP (quoteWith short names line) (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VLine p x y f)  = PathIntro (quoteWith short names p) (quoteWith short names x) (quoteWith short names y) (quoteWith short names f)
 
-quoteWith names (VPartial x y)  = Partial (quoteWith names x) (quoteWith names y)
-quoteWith names (VPartialP x y) = PartialP (quoteWith names x) (quoteWith names y)
-quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))
-quoteWith names (VSub a b c) = Sub (quoteWith names a) (quoteWith names b) (quoteWith names c)
-quoteWith names (VInc a b c) = Inc (quoteWith names a) (quoteWith names b) (quoteWith names c)
-quoteWith names (VComp a phi u a0) = Comp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
-quoteWith names (VHComp a phi u a0) = HComp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
+quoteWith short names (VPartial x y)  = Partial (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VPartialP x y) = PartialP (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith short names x, quoteWith short names y)) (Map.toList fs)))
+quoteWith short names (VSub a b c) = Sub (quoteWith short names a) (quoteWith short names b) (quoteWith short names c)
+quoteWith short names (VInc a b c) = Inc (quoteWith short names a) (quoteWith short names b) (quoteWith short names c)
+quoteWith short names (VComp a phi u a0) = Comp (quoteWith short names a) (quoteWith short names phi) (quoteWith short names u) (quoteWith short names a0)
+quoteWith short names (VHComp a phi u a0) = HComp (quoteWith short names a) (quoteWith short names phi) (quoteWith short names u) (quoteWith short names a0)
 
-quoteWith names (VGlueTy a phi t e)    = GlueTy (quoteWith names a) (quoteWith names phi) (quoteWith names t) (quoteWith names e)
-quoteWith names (VGlue a phi ty e t x) = Glue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names t) (quoteWith names x)
-quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names x)
+quoteWith short names (VGlueTy a phi t e)    = GlueTy (quoteWith short names a) (quoteWith short names phi) (quoteWith short names t) (quoteWith short names e)
+quoteWith short names (VGlue a phi ty e t x) = Glue (quoteWith short names a) (quoteWith short names phi) (quoteWith short names ty) (quoteWith short names e) (quoteWith short names t) (quoteWith short names x)
+quoteWith short names (VUnglue a phi ty e x) = Unglue (quoteWith short names a) (quoteWith short names phi) (quoteWith short names ty) (quoteWith short names e) (quoteWith short names x)
 
-quoteWith names (VCase _ rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs
+quoteWith short names (VCase _ rng v xs) = Case (quoteWith short names rng) (quoteWith short 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)
+quoteWith short names (VEqStrict a x y) = EqS (quoteWith short names a) (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VReflStrict a x) = Syntax.Refl (quoteWith short names a) (quoteWith short names x)
 
 alwaysShort :: Value -> Bool
 alwaysShort (VNe HCon{} _) = True
@@ -297,7 +297,7 @@ refresh x s n
   | otherwise = refresh x s (Bound (getNameText n <> T.singleton '\'') 0)
 
 quote :: Value -> Term
-quote = quoteWith mempty
+quote = quoteWith True mempty
 
 data Closure
   = Closure

src/Syntax/Pretty.hs

@@ -132,7 +132,7 @@ prettyTm' implicits = go True 0 where
 
       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)]
+      Unglue _a _phi _ty _e t -> apps (con "unglue") [(Im, _a), (Im, _phi), (Im, _ty), (Im, _e), (Ex, t)]
 
       Comp a phi u a0 -> apps (con "comp") [(Ex, a), (Im, phi), (Ex, u), (Ex, a0)]
       HComp a phi u a0 -> apps (con "hcomp") [(Im, a), (Im, phi), (Ex, u), (Ex, a0)]
@@ -192,10 +192,10 @@ prettyBinds imp ((x, ty, tm):bs) =
 
 showFace :: Bool -> Map Head Bool -> Doc AnsiStyle
 showFace imp = hsep . map go . Map.toList where
-  go (h, b) = parens $ prettyTm' imp (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
+  go (h, b) = parens $ prettyTm' imp (quoteWith False mempty (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
 
 prettyVl' :: Bool -> Value -> Doc AnsiStyle
-prettyVl' b = prettyTm' b . quote
+prettyVl' b = prettyTm' b . quoteWith True mempty
 
 instance Pretty Term where
   pretty = unAnnotate . prettyTm