Remove `(φ = i0) as p` syntax + clean up proof of univalence + formalise theorems 4.7.6, 4.7.7, 7.2.2

intro.tt

@@ -367,9 +367,6 @@ invert eqv y = (eqv y) .1 .1
 retract : {A : Type} {B : Type} -> (A -> B) -> (B -> A) -> Type
 retract {A} {B} f g = (a : A) -> Path (g (f a)) a
 
-contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> A
-contr {A} {phi} p u = comp (\i -> A) {phi} (\i is1 -> p.2 (u is1) i) (inS (p.1))
-
 -- Proving that it's also a retraction is left as an exercise to the
 -- reader. We can package together a function and a proof that it's an
 -- equivalence to get a capital-E Equivalence.
@@ -379,8 +376,8 @@ Equiv A B = (f : A -> B) * isEquiv {A} {B} f
 
 -- The identity function is an equivalence between any type A and
 -- itself.
-idEquiv : {A : Type} -> isEquiv (id {A})
-idEquiv y = ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j)))
+idEquiv : {A : Type} -> Equiv A A
+idEquiv {A} = (\x -> x, \y -> ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j))))
 
 -- The glue operation expresses that "extensibility is invariant under
 -- equivalence". Less concisely, the Glue type and its constructor,
@@ -462,10 +459,10 @@ Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)
 --        B ------------ B
 --             \i → B
 --
-univalence : {A : Type} {B : Type} -> Equiv A B -> Path A B
-univalence {A} {B} equiv i =
+ua : {A : Type} {B : Type} -> Equiv A B -> Path A B
+ua {A} {B} equiv i =
   Glue B (\[ (i = i0) -> (A, equiv),
-             (i = i1) -> (B, the B, idEquiv {B}) ]) 
+             (i = i1) -> (B, idEquiv) ]) 
 
 lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)
 {-# PRIMITIVE lineToEquiv #-}
@@ -479,7 +476,7 @@ isEquivTransport A = (lineToEquiv A).2
 -- The fact that this diagram has 2 filled-in B sides explains the
 -- complication in the proof below.
 --
--- In particular, the actual behaviour of transp (\i -> univalence f i)
+-- In particular, the actual behaviour of transp (\i -> ua f i)
 -- (x : A) is not just to apply f x to get a B (the left side), it also
 -- needs to:
 --
@@ -495,11 +492,11 @@ isEquivTransport A = (lineToEquiv A).2
 -- for any composition, its filler connects either endpoints. So
 -- we need to come up with a filler for the Bottom and right faces.
 
-univalenceBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1
-univalenceBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i)
+uaBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> ua f i)) f.1
+uaBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i)
 
--- The terms univalence + univalenceBeta suffice to prove the "full"
--- univalence axiom of Voevodsky, as can be seen in the paper
+-- The terms ua + uaBeta suffice to prove the "full"
+-- ua axiom of Voevodsky, as can be seen in the paper
 --
 --   Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom.
 --
@@ -612,7 +609,7 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
   fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2
 
 IsoToId : {A : Type} {B : Type} -> Iso A B -> Path A B
-IsoToId i = univalence (IsoToEquiv i)
+IsoToId i = ua (IsoToEquiv i)
 
 -- We can prove that any involutive function is an isomorphism, since
 -- such a function is its own inverse.
@@ -620,10 +617,10 @@ IsoToId i = univalence (IsoToEquiv i)
 involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f
 involToIso {A} f inv = (f, inv, inv)
 
--- An example of univalence
+-- An example of ua
 ---------------------------
 --
--- The classic example of univalence is the equivalence
+-- The classic example of ua is the equivalence
 -- not : Bool \simeq Bool.
 --
 -- We define it here.
@@ -654,7 +651,7 @@ notInvol : (x : Bool) -> Path (not (not x)) x
 notInvol = elimBool (\b -> Path (not (not b)) b) refl refl
 
 notp : Path Bool Bool
-notp = univalence (IsoToEquiv (not, involToIso not notInvol))
+notp = ua (IsoToEquiv (not, involToIso not notInvol))
 
 -- This path actually serves to prove a simple lemma about the universes
 -- of HoTT, namely, that any univalent universe is not a 0-type. If we
@@ -741,7 +738,7 @@ pathIsHom {A} {B} {f} {g} =
   let
     theIso : Iso (Path f g) (Hom f g)
     theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
-  in univalence (IsoToEquiv theIso)
+  in ua (IsoToEquiv theIso)
 
 -- Inductive types
 -------------------
@@ -835,7 +832,7 @@ sucEquiv = IsoToEquiv (sucZ, (predZ, sucPredZ, predSucZ))
 -- x = suc x, transp (sym intPath) x = pred x
 
 intPath : Path Int Int
-intPath = univalence sucEquiv
+intPath = ua sucEquiv
 
 -- Higher inductive types
 -------------------------
@@ -981,7 +978,7 @@ poSusp : Type -> Type
 poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt)
 
 Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A)
-Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where
+Susp_is_poSusp {A} = ua (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where
   poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A
   poSusp_to_Susp = \case
     inl x -> north
@@ -1018,7 +1015,7 @@ data T2 : Type where
     ]
 
 TorusIsTwoCircles : Path T2 (S1 * S1)
-TorusIsTwoCircles = univalence (IsoToEquiv theIso) where
+TorusIsTwoCircles = ua (IsoToEquiv theIso) where
   torusToCircs : T2 -> S1 * S1
   torusToCircs = \case
     baseT -> (base, base)
@@ -1196,7 +1193,7 @@ data S2 : Type where
   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
+S2IsSuspS1 = ua (IsoToEquiv iso) where
   toS2 : Susp S1 -> S2
   toS2 = \case { north -> base2; south -> base2; merid x i -> sphMerid x i } where
     sphMerid = \case
@@ -1232,7 +1229,7 @@ data S3 : Type where
   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
+S3IsSuspS2 = ua (IsoToEquiv iso) where
   toS3 : Susp S2 -> S3
   toS3 = \case { north -> base3; south -> base3; merid x i -> sphMerid x i } where
     sphMerid = \case
@@ -1337,7 +1334,7 @@ equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B)
 equivCtrPath e y = (e.2 y).2
 
 contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> Sub A phi u
-contr {A} {phi} p u = primComp (\i -> A) (\i [ (phi = i1) as c -> p.2 (u c) i ]) (inS p.1)
+contr {A} {phi} p u = primComp (\i -> A) (\i [ (phi = i1) -> p.2 (u itIs1) i ]) (inS p.1)
 
 contr' : {A : Type} -> ({phi : I} -> (u : Partial phi A) -> Sub A phi u) -> isContr A
 contr' {A} contr = (x, \y i -> outS (contr (\ [ (i = i0) -> x, (i = i1) -> y ])) ) where
@@ -1476,16 +1473,16 @@ isProp_to_Sq_equiv {P} prop = propExt prop sqProp inc proj where
   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 (univalence eqv (inot i))) (\x y i -> sq x y i)
+Sq_equiv_to_isProp eqv = transp (\i -> isProp (ua eqv (inot i))) (\x y i -> sq x y i)
 
 exercise_3_21 : {P : Type} -> Equiv (isProp P) (Equiv P (Sq P))
 exercise_3_21 {P} = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp
 
-uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (univalence {A} {B}) (idToEquiv {A} {B})
-uaret eqv = equivLemma (univalenceBeta eqv)
+uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (ua {A} {B}) (idToEquiv {A} {B})
+uaret eqv = equivLemma (uaBeta eqv)
 
 f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B
-f1 {A} p = (p.1, univalence p.2)
+f1 {A} p = (p.1, ua p.2)
 
 f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B
 f2 {A} p = (p.1, idToEquiv p.2)
@@ -1493,11 +1490,11 @@ f2 {A} p = (p.1, idToEquiv p.2)
 uaretSig : {A : Type} (a : (B : Type) * Equiv A B) -> Path (f2 (f1 a)) a
 uaretSig {A} p = sigmaPath (\i -> p.1) (uaret {A} {p.1} p.2)
 
-retContr : {A : Type} {B : Type}
-        -> (f : A -> B) -> (g : B -> A)
-        -> (h : retract f g)
-        -> isContr B -> isContr A
-retContr {A} {B} f g h v = (g b, p) where
+isContrRetract : {A : Type} {B : Type}
+              -> (f : A -> B) -> (g : B -> A)
+              -> (h : retract f g)
+              -> isContr B -> isContr A
+isContrRetract {A} {B} f g h v = (g b, p) where
   b = v.1
 
   p : (x : A) -> Path (g b) x
@@ -1512,41 +1509,6 @@ curry {A} {B} {C} = IsoToId (to, from, \f -> refl, \g -> refl) where
   from : ((p : (x : A) * B x) -> C p.1 p.2) -> (x : A) (y : B x) -> C x y
   from f x y = f (x, y)
 
-ft2 : {A : Type} -> Path (T2 -> A) (S1 -> S1 -> A)
-ft2 {A} = transp (\i -> Path (T2 -> A) (curry {S1} {\x -> S1} {\x y -> A} (inot i))) p where
-  p : Path (T2 -> A) ((S1 * S1) -> A)
-  p i = TorusIsTwoCircles i -> A
-
-data coeq {A : Type} {B : Type} (f : B -> A) (g : B -> A) : Type where
-  c   : A -> coeq {A} {B} f g
-  p i : (b : B) -> coeq {A} {B} f g [ (i = i0) -> c (f b), (i = i1) -> c (g b) ]
-
-coeq_S1 : Type
-coeq_S1 = coeq {Unit} {Unit} id id
-
-coeq_base : coeq_S1
-coeq_base = c tt
-
-coeq_loop : Path coeq_base coeq_base
-coeq_loop i = p tt i
-
-coeq_S1_elim : (P : coeq_S1 -> Type) (base : P coeq_base)
-            -> PathP (\i -> P (coeq_loop i)) base base
-            -> (x : coeq_S1)
-            -> P x
-coeq_S1_elim P base loop =
-  \case
-    c x -> baseCase x
-    p x i -> loopCase x i
-  where
-    baseCase : (x : Unit) -> P (c x)
-    baseCase = \case
-      tt -> base
-
-    loopCase : (x : Unit) -> PathP (\i -> P (p x i)) (baseCase x) (baseCase x)
-    loopCase = \case
-      tt -> loop
-
 ContractibleIfInhabited : {A : Type} -> Path (A -> isContr A) (isProp A)
 ContractibleIfInhabited {A} = IsoToId (to, from, toFrom, fromTo) where
   to : (A -> isContr A) -> isProp A
@@ -1578,7 +1540,7 @@ ConeA_contr {A} = (point, contr) where
 contrSinglEquiv : {B : Type} -> isContr ((A : Type) * Equiv A B)
 contrSinglEquiv {B} = (center, contract) where
   center : (A : Type) * Equiv A B
-  center = (B, the B, idEquiv {B})
+  center = (B, idEquiv)
 
   contract : (p : (A : Type) * Equiv A B) -> Path center p
   contract w i =
@@ -1619,35 +1581,110 @@ contrSinglEquiv {B} = (center, contract) where
         in (ctr, contr)
     in (GlueB, unglueB, unglueEquiv)
 
-uaIdEquiv : {A : Type} -> Path (univalence (the A, idEquiv {A})) (\i -> A)
-uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, the A, idEquiv {A}))
+uaIdEquiv : {A : Type} -> Path (ua idEquiv) (\i -> A)
+uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, idEquiv))
 
-EquivJ : {X : Type}
-         (P : (Y : Type) -> Equiv Y X -> Type)
-         (d : P X (the X, idEquiv {X}))
-         {Y : Type} (E : Equiv Y X)
-      -> P Y E
-EquivJ {X} P d {Y} e = subst {(Y : Type) * Equiv Y X} (\x -> P x.1 x.2) path d where
-  path : Path {(Y : Type) * Equiv Y X} (X, the X, idEquiv {X}) (Y, e)
-  path = isContr_isProp {(Y : Type) * Equiv Y X} contrSinglEquiv (X, the X, idEquiv {X}) (Y, e)
+EquivJ : (P : (X : Type) (Y : Type) -> Equiv X Y -> Type)
+      -> ((X : Type) -> P X X idEquiv)
+      -> {X : Type} {Y : Type} (E : Equiv X Y)
+      -> P X Y E
+EquivJ P p {X} {Y} E =
+  subst {(X : Type) * Equiv X Y}
+        (\x -> P x.1 Y x.2)
+        (\i -> isContr_isProp contrSinglEquiv (Y, idEquiv) (X, E) i)
+        (p Y)
 
 pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
-pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A})
-
-uaIso : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B)
-uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where
-  pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) (the A, idEquiv {A})
-  pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A})
-
-  univalence_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (univalence (pathToEquiv p)) p
-  univalence_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (univalence {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where
-    lemma : Path (univalence (pathToEquiv (\i -> A))) (\i -> A)
-    lemma = transp (\i -> Path (univalence (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv
-
-  pathToEquiv_univalence : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (univalence p)) p
-  pathToEquiv_univalence {A} {B} p = EquivJ {B} (\A e -> Path (pathToEquiv (univalence e)) e) lemma p where
-    lemma : Path (pathToEquiv (univalence (the B, idEquiv {B}))) (the B, idEquiv {B})
-    lemma = transp (\i -> Path (pathToEquiv (uaIdEquiv {B} (inot i))) (the B, idEquiv {B})) pathToEquiv_refl
-
-uaEquiv : {A : Type} {B : Type} -> isEquiv (pathToEquiv {A} {B})
-uaEquiv {A} {B} = (IsoToEquiv (uaIso {A} {B})).2
+pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) idEquiv
+
+univalence : {A : Type} {B : Type} -> Equiv (Path A B) (Equiv A B)
+univalence = IsoToEquiv (pathToEquiv, ua, pathToEquiv_ua, ua_pathToEquiv) where
+  pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) idEquiv
+  pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) idEquiv
+
+  ua_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (ua (pathToEquiv p)) p
+  ua_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (ua {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where
+    lemma : Path (ua (pathToEquiv (\i -> A))) (\i -> A)
+    lemma = transp (\i -> Path (ua (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv
+
+  pathToEquiv_ua : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (ua p)) p
+  pathToEquiv_ua {A} {B} p = EquivJ (\A B e -> Path (pathToEquiv (ua e)) e) lemma p where
+    lemma : (A : Type) -> Path (pathToEquiv (ua idEquiv)) idEquiv
+    lemma A = transp (\i -> Path (pathToEquiv (uaIdEquiv {A} (inot i))) idEquiv) pathToEquiv_refl
+
+total : {A : Type} {P : A -> Type} {Q : A -> Type}
+     -> ((x : A) -> P x -> Q x)
+     -> ((x : A) * P x) -> ((x : A) * Q x)
+total f p = (p.1, f p.1 p.2)
+
+total_fibers : {A : Type} {P : A -> Type} {Q : A -> Type}
+            -> {xv : (a : A) * Q a}
+            -> (f : (el : A) -> P el -> Q el)
+            -> Iso (fiber (total f) xv) (fiber (f xv.1) xv.2)
+total_fibers {A} {P} {Q} {xv} f = (to, fro, toFro {xv}, froTo) where
+  to : {xv : (a : A) * Q a} -> fiber (total f) xv -> fiber (f xv.1) xv.2
+  to peq = J {(a : A) * Q a} {_} (\xv eq -> fiber (f xv.1) xv.2) (peq.1.2, refl) (sym peq.2)
+
+  fro : {xv : (a : A) * Q a} -> fiber (f xv.1) xv.2 -> fiber (total f) xv
+  fro peq = ((xv.1, peq.1), \i -> (_, peq.2 i))
+
+  toFro : {xv : (a : A) * Q a} -> (y : fiber (f xv.1) xv.2) -> Path (to (fro y)) y
+  toFro {xv} peq =
+    J {Q xv.1} {f xv.1 p}
+      (\xv1 eq1 -> Path (to {(xv.1, xv1)} (fro (p, sym eq1))) (p, sym eq1))
+      (JRefl {(a : A) * Q a} {(xv.1, f xv.1 peq.1)}
+        (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl))
+      (sym eq)
+    where p : P xv.1
+          p = peq.1
+
+          eq : Path {Q xv.1} xv.2 (f xv.1 p)
+          eq = peq.2
+
+  froTo : {xv : (a : A) * Q a} -> (y : fiber (total f) xv) -> Path (fro {xv} (to {xv} y)) y
+  froTo {xv} apeq =
+    J {(a : A) * Q a} {total f (a, p)}
+      (\xv1 eq1 -> Path (fro {_} (to {_} ((a, p), sym eq1))) ((a, p), sym eq1))
+      (ap fro (JRefl {(a : A) * Q a} {(a, _)}
+                (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl)))
+      (sym eq)
+    where a : A
+          a = apeq.1.1
+
+          p : P a
+          p = apeq.1.2
+
+          eq : Path xv (total f (a, p))
+          eq = apeq.2
+
+fiberEquiv : {A : Type} {P : A -> Type} {Q : A -> Type}
+          -> (f : (el : A) -> P el -> Q el)
+          -> isEquiv (total f)
+          -> (x : A) -> isEquiv (f x)
+fiberEquiv f iseqv x y = isContrRetract {fiber (f x) y} {fiber (total f) (x, y)} eqv.2.1 eqv.1 eqv.2.2.1 (iseqv (x, y)) where
+  eqv : Iso (fiber (total f) (x, y)) (fiber (f x) y)
+  eqv = total_fibers f
+
+totalEquiv : {A : Type} {P : A -> Type} {Q : A -> Type}
+          -> (f : (el : A) -> P el -> Q el)
+          -> ((x : A) -> isEquiv (f x))
+          -> isEquiv (total f)
+totalEquiv f iseqv xv = isContrRetract {fiber (total f) xv} {fiber (f xv.1) xv.2} eqv.1 eqv.2.1 eqv.2.2.2 (iseqv xv.1 xv.2) where
+  eqv : Iso (fiber (total f) xv) (fiber (f xv.1) xv.2)
+  eqv = total_fibers f
+
+contrIsEquiv : {A : Type} {B : Type} -> isContr A -> isContr B
+            -> (f : A -> B) -> isEquiv f
+contrIsEquiv cA cB f y = ((cA.1, isContr_isProp cB _ _), \v -> sigmaPath (isContr_isProp cA _ _) (isProp_isSet (isContr_isProp cB) _ _ _ v.2))
+
+theorem722 : {A : Type} {R : A -> A -> Type}
+          -> ((x : A) (y : A) -> isProp (R x y))
+          -> ({x : A} -> R x x)
+          -> (f : (x : A) (y : A) -> R x y -> Path x y)
+          -> {x : A} {y : A} -> isEquiv {R x y} {Path x y} (f x y)
+theorem722 {A} {R} prop rho toId {x} {y} = fiberEquiv {A} {R x} {Path x} (toId x) (totalEquiv x) y where
+  rContr : (x : A) -> isContr ((y : A) * R x y)
+  rContr x = ((x, rho {x}), \y -> sigmaPath (toId _ _ y.2) (prop _ _ _ y.2))
+
+  totalEquiv : (x : A) -> isEquiv (total {A} {R x} {Path x} (toId x))
+  totalEquiv x = contrIsEquiv (rContr x) singContr (total {A} {R x} {Path x} (toId x))

src/Elab.hs

@@ -33,6 +33,7 @@ import Prettyprinter
 
 import Syntax.Pretty
 import Syntax
+import Debug (traceM, traceDocM)
 
 infer :: P.Expr -> ElabM (Term, NFType)
 infer (P.Span ex a b) = withSpan a b $ infer ex
@@ -145,24 +146,14 @@ check (P.Let items body) ty = do
 
 check (P.LamSystem bs) ty = do
   (extent, dom) <- isPartialType ty
-  let dom_q x = quote (dom x)
   eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
-    phi <- checkFormula (P.condF formula)
-    rhses <-
-      case P.condV formula of
-        Just t -> assume (Bound t 0) (VEqStrict VI phi VI1) $ \var -> do
-          env <- ask
-          for (truthAssignments phi (getEnv env)) $ \e -> do
-            let env' = env{ getEnv = e }
-            local (const env') $
-              (Just var,) <$> check rhs (eval' env' (dom_q (VVar var)))
-        Nothing -> do
-          env <- ask
-          n <- newName
-          for (truthAssignments phi (getEnv env)) $ \e -> do
-            let env' = env{ getEnv = e }
-            local (const env') $
-              (Nothing,) <$> check rhs (eval' env' (dom_q (VVar n)))
+    (phi, fv) <- checkFormula formula
+    env <- ask
+    n <- newName
+    rhses <- for (truthAssignments phi (getEnv env)) $ \e -> do
+      let env' = env{ getEnv = e }
+      local (const env') $
+        (Nothing,) <$> check rhs (substitute (snd <$> Map.restrictKeys e fv) (dom (VVar n)))
     pure (n, (phi, head rhses))
 
   unify extent (foldl ior VI0 (map (fst . snd) eqns))
@@ -364,21 +355,27 @@ checkLetItems map (P.LetBind name rhs:xs) cont = do
         checkLetItems (Map.insert (getNameText name) Nothing map) xs \xs ->
           cont ((name, quote ty_nf, rhs):xs)
 
-checkFormula :: P.Formula -> ElabM Value
-checkFormula P.FTop = pure VI1
-checkFormula P.FBot = pure VI0
-checkFormula (P.FAnd x y) = iand <$> checkFormula x <*> checkFormula y
-checkFormula (P.FOr x y) = ior <$> checkFormula x <*> checkFormula y
+checkFormula :: P.Formula -> ElabM (Value, Set.Set Name)
+checkFormula P.FTop = pure (VI1, mempty)
+checkFormula P.FBot = pure (VI0, mempty)
+checkFormula (P.FAnd x y) = do
+  (x, f) <- checkFormula x
+  (y, f') <- checkFormula y
+  pure (iand x y, f <> f')
+checkFormula (P.FOr x y) = do
+  (x, f) <- checkFormula x
+  (y, f') <- checkFormula y
+  pure (ior x y, f <> f')
 checkFormula (P.FIs0 x) = do
   nm <- getNameFor x
   ty <- getNfType nm
   unify ty VI
-  pure (inot (VVar nm))
+  pure (inot (VVar nm), Set.singleton nm)
 checkFormula (P.FIs1 x) = do
   nm <- getNameFor x
   ty <- getNfType nm
   unify ty VI
-  pure (VVar nm)
+  pure (VVar nm, Set.singleton nm)
 
 isSort :: NFType -> ElabM ()
 isSort t = isSort (force t) where
@@ -576,7 +573,7 @@ checkStatement (P.Data name tele retk constrs) k =
         unify ret' ret
 
         faces <- envArgs args $ for faces \(f, t) -> do
-          phi <- checkFormula f
+          (phi, _) <- checkFormula f
           t <- check t ret
           pure (phi, (quote phi, t))
 

src/Presyntax/Parser.y

@@ -81,7 +81,7 @@ import Debug.Trace
 Exp :: { Expr }
 Exp
   : '\\' LambdaList '->' Exp             { span $1 $4 $ makeLams $2 $4 }
-  | '\\' MaybeLambdaList '[' System ']'  { span $1 $5 $ makeLams $2 $ LamSystem $4 }
+  | '\\' MaybeLambdaList '[' Faces ']'   { span $1 $5 $ makeLams $2 $ LamSystem $4 }
   | '\\' 'case' Block(CaseList)          { span $1 $3 $ LamCase (thd $3) }
   | '(' var ':' Exp ')' ProdTail         { span $1 $6 $ Pi Ex (getVar $2) $4 $6 }
   | '{' var ':' Exp '}' ProdTail         { span $1 $6 $ Pi Im (getVar $2) $4 $6 }
@@ -219,18 +219,6 @@ Pragma :: { Statement }
   : 'PRIMITIVE' var var { Builtin (getVar $2) (getVar $3) }
   | 'PRIMITIVE' var     { Builtin (getVar $2) (getVar $2) }
 
-System :: { [(Condition, Expr)] }
-  : {- empty system -}            { [] }
-  | NeSystem                      { $1 }
-
-NeSystem :: { [(Condition, Expr) ]}
-  : SystemLhs '->' Exp              { [($1, $3)] }
-  | SystemLhs '->' Exp ',' NeSystem { ($1, $3):$5 }
-
-SystemLhs :: { Condition }
-  : Formula 'as' var { Condition $1 (Just (getVar $3)) }
-  | Formula          { Condition $1 Nothing }
-
 Faces :: { [(Formula, Expr)] }
   : {- empty system -}            { [] }
   | NeFaces                       { $1 }

src/Presyntax/Presyntax.hs

@@ -21,7 +21,7 @@ data Expr
   | Proj1 Expr
   | Proj2 Expr
 
-  | LamSystem [(Condition, Expr)]
+  | LamSystem [(Formula, Expr)]
   | LamCase [(Pattern, Expr)]
   | Let [LetItem] Expr
 
@@ -33,10 +33,6 @@ data LetItem
   | LetBind { leIName :: Text, leIVal :: Expr }
   deriving (Eq, Show, Ord)
 
-data Condition
-  = Condition { condF :: Formula, condV :: Maybe Text }
-  deriving (Eq, Show, Ord)
-
 data Formula
   = FIs1 Text
   | FIs0 Text

src/Syntax.hs

@@ -228,7 +228,7 @@ quoteWith names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) =
 
 quoteWith names (GluedVl h sp vl)
   | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
-  | True || alwaysShort vl = quoteWith names vl
+  | alwaysShort vl = quoteWith names vl
   | _ Seq.:|> PIElim _ x y i <- sp =
     case i of
       VI0 -> quoteWith names x