Fix typechecking

JetBrains · Feb 21, 2024 · 5cd3179 · 5cd3179
1 parent cbb33d5
commit 5cd3179
Showing 1 changed file with 7 additions and 9 deletions.
diff --git a/src/Homotopy/Localization/BlakersMassey.ard b/src/Homotopy/Localization/BlakersMassey.ard
@@ -10,7 +10,6 @@
 \import HLevel
 \import Homotopy.Fibration
 \import Homotopy.Join
-\import Homotopy.Localization.Accessible
 \import Homotopy.Localization.Connected
 \import Homotopy.Localization.Universe
 \import Homotopy.Pushout
@@ -27,14 +26,13 @@
     \lemma surjective {d : Data} {x0 : X} {y0 : Y} (q : TruncP (\Sigma (y : Y) (Q x0 y))) : isConnectedMap (pbMap {d} {x0} {y0}) \elim q
       | inP (y,q0) => \lam p => contr=>isConnected (Fib pbMap p) (DataExt.code-contr {\new DataExt { | Data => d | x0 => x0 | y0 => y | q0 => q0 }} p)
 
-    \class EquivData \noclassifying
-      (A B : \hType)
-      (M : A -> Connected) (N : B -> Connected)
-      (f : \Sigma (a : A) (M a) -> \Sigma (b : B) (N b))
-      (g : \Sigma (b : B) (N b) -> \Sigma (a : A) (M a))
-      (p : \Pi (a : A) (m : M a) -> (g (f (a,m))).1 = a)
-      (q : \Pi (b : B) (n : N b) -> (f (g (b,n))).1 = b)
-    \extends ReflUniverse {
+    \class EquivData \noclassifying (A B : \hType) \extends ReflUniverse {
+      | M : A -> Connected
+      | N : B -> Connected
+      | f : \Sigma (a : A) (M a) -> \Sigma (b : B) (N b)
+      | g : \Sigma (b : B) (N b) -> \Sigma (a : A) (M a)
+      | p : \Pi (a : A) (m : M a) -> (g (f (a,m))).1 = a
+      | q : \Pi (b : B) (n : N b) -> (f (g (b,n))).1 = b
 
       \func eval (a : A) (m : M a) : lift (\lam a => sec {Connected.equiv {M a} (LType B)} (\lam m => lEta (f (a,m)).1)) (lEta a) = lEta (f (a,m)).1 =>
         lift-prop (\lam a => sec {Connected.equiv {M a} (LType B)} (\lam m => lEta (f (a,m)).1)) a *> path (\lam i => (f_sec {Connected.equiv {M a} (LType B)} (\lam m => lEta (f (a,m)).1) @ i) m)