system shouldn'y be empty

lib/foundations/univalent/path.anders

@@ -118,8 +118,8 @@ def partial-app-test (A : U) (a : A) (φ : I) (p : 1= φ) : A := [(φ = 1) → a
 def 0-is-min (i : I) : ≤ 0 i := ref 0
 def 1-is-max (i : I) : ≤ i 1 := ref i
 def ε (A : U) : Partial A 0 := []
-def I-nontriv (p : Id I 0 1) : 𝟎 := ε 𝟎 (rev I 0 1 p)
-def 0≥1-impl-absurd : (≥ 0 1) → 𝟎 := I-nontriv
+-- def I-nontriv (p : Id I 0 1) : 𝟎 := ε 𝟎 (rev I 0 1 p)
+-- def 0≥1-impl-absurd : (≥ 0 1) → 𝟎 := I-nontriv
 
 def ≤-asymm (i j : I) (p : ≤ i j) (q : ≤ j i) : Id I i j := comp-Id I i (i ∧ j) j (rev I (i ∧ j) i p) q
 def ≤-refl (i : I) : ≤ i i := ref i

lib/mathematics/analysis/topology.anders

@@ -5,7 +5,7 @@ module topology where
 
 def Path₁ (A : U₁) (x y : A) := PathP (<_> A) x y
 def isProp₁ (A : U₁) := Π (a b : A), Path₁ A a b
-def isSet₁ (A : U₁) := Π (a b : A) (a0 b0 : Path₁ A a b), Path₁ (Path₁ A a b) a0 b0
+def isSet₁ (A : U₁) := Π (a b : A) (x y : Path₁ A a b), Path₁ (Path₁ A a b) x y
 def Ω := U → 𝟐
 def ℙ (X: U₁) := X → Ω
 axiom isSet-ℙ (X: U₁) : isSet₁ (ℙ X)

src/kernel/check.ml

@@ -557,7 +557,7 @@ and conv v1 v2 : bool = traceConv v1 v2;
 
 and convWithSystem = function
   | v, VApp (VSystem ts, _) | VApp (VSystem ts, _), v ->
-    System.for_all (fun mu -> conv (upd mu v)) ts
+    not (System.is_empty ts) && System.for_all (fun mu -> conv (upd mu v)) ts
   | _, _ -> false
 
 and convProofIrrel v1 v2 =