[WIP] Add support for Agda 2.5.4

core/lib/types/Pushout.agda

@@ -43,14 +43,23 @@ module PushoutRec {i j k} {d : Span {i} {j} {k}} {l} {D : Type l}
   (left* : Span.A d → D) (right* : Span.B d → D)
   (glue* : (c : Span.C d) → left* (Span.f d c) == right* (Span.g d c)) where
 
-  private
-    module M = PushoutElim left* right* (λ c → ↓-cst-in (glue* c))
+  abstract
+    private
+      module M = PushoutElim left* right* (λ c → ↓-cst-in (glue* c))
 
-  f : Pushout d → D
-  f = M.f
+    f : Pushout d → D
+    f = M.f
 
-  glue-β : (c : Span.C d) → ap f (glue c) == glue* c
-  glue-β c = apd=cst-in {f = f} (M.glue-β c)
+    left-β : ∀ a → f (left a) ↦ left* a
+    left-β a = M.left-β a
+    {-# REWRITE left-β #-}
+
+    right-β : ∀ b → f (right b) ↦ right* b
+    right-β b = M.right-β b
+    {-# REWRITE right-β #-}
+
+    glue-β : (c : Span.C d) → ap f (glue c) == glue* c
+    glue-β c = apd=cst-in {f = f} (M.glue-β c)
 
 Pushout-rec = PushoutRec.f
 

theorems/cohomology/SpectrumModel.agda

@@ -224,11 +224,12 @@ module SpectrumModel where
 
     abstract
       C-additive-is-equiv : is-equiv (GroupHom.f (Πᴳ-fanout (C-fmap n ∘ ⊙bwin {X = X})))
-      C-additive-is-equiv = transport is-equiv
-        (λ= $ Trunc-elim
-          (λ _ → idp))
-        ((ac (uCEl n ∘ X)) ∘ise (is-eq into out into-out out-into))
-
+      C-additive-is-equiv =
+        transport is-equiv
+          {x = unchoose ∘ into}
+          {y = GroupHom.f (Πᴳ-fanout (C-fmap n ∘ ⊙bwin {X = X}))}
+          (λ= $ Trunc-elim (λ _ → idp))
+          (ac (uCEl n ∘ X) ∘ise (is-eq into out into-out out-into))
 
 open SpectrumModel
 

theorems/cw/Attached.agda

@@ -36,12 +36,24 @@ module _ {A : Type i} {B : Type j} {C : Type k} {attaching : Attaching A B C} wh
     (spoke* : (b : B) (c : C)
       → incl* (attaching b c) == hub* b [ P ↓ spoke b c ]) where
 
-    module P = PushoutElim
-      {d = attached-span attaching} {P = P}
-      incl* hub* (uncurry spoke*)
+    abstract
+      module P = PushoutElim
+        {d = attached-span attaching} {P = P}
+        incl* hub* (uncurry spoke*)
 
-    f = P.f
-    spoke-β = curry P.glue-β
+      f : (x : Attached attaching) → P x
+      f = P.f
+
+      incl-β : ∀ a → f (incl a) ↦ incl* a
+      incl-β a = P.left-β a
+      {-# REWRITE incl-β #-}
+
+      hub-β : ∀ b → f (hub b) ↦ hub* b
+      hub-β b = P.right-β b
+      {-# REWRITE hub-β #-}
+
+      spoke-β : ∀ b c → apd f (spoke b c) == spoke* b c
+      spoke-β = curry P.glue-β
 
   open AttachedElim public using () renaming (f to Attached-elim)
 
@@ -50,12 +62,23 @@ module _ {A : Type i} {B : Type j} {C : Type k} {attaching : Attaching A B C} wh
     (hub* : (b : B) → D)
     (spoke* : (b : B) (c : C) → incl* (attaching b c) == hub* b) where
 
-    module P = PushoutRec
-      {d = attached-span attaching} {D = D}
-      incl* hub* (uncurry spoke*)
+    abstract
+      module P = PushoutRec
+        {d = attached-span attaching} {D = D}
+        incl* hub* (uncurry spoke*)
 
-    f = P.f
-    spoke-β = curry P.glue-β
+      f : Attached attaching → D
+      f = P.f
 
-  open AttachedRec public using () renaming (f to Attached-rec)
+      incl-β : ∀ a → f (incl a) ↦ incl* a
+      incl-β a = P.left-β a
+      {-# REWRITE incl-β #-}
 
+      hub-β : ∀ b → f (hub b) ↦ hub* b
+      hub-β b = P.right-β b
+      {-# REWRITE hub-β #-}
+
+      spoke-β : ∀ b c → ap f (spoke b c) == spoke* b c
+      spoke-β = curry P.glue-β
+
+  open AttachedRec public using () renaming (f to Attached-rec)

theorems/cw/WedgeOfCells.agda

@@ -35,7 +35,7 @@ private
   module BouquetToBigWedgeSusp =
     BigWedgeRec {A = cells} {X = Bouquet-family cells (S n)}
     cfbase SphereToBigWedgeSusp.f (λ _ → idp)
-  
+
   module BigWedgeSuspEquivQuotient = PushoutLSplit (uncurry attaching) (λ _ → unit) fst
 
 Bouquet-to-Xₙ/Xₙ₋₁ : Bouquet cells (S n) → Xₙ/Xₙ₋₁
@@ -50,10 +50,10 @@ abstract
     ∙ ap (ap BigWedgeSuspEquivQuotient.split) (SphereToBigWedgeSusp.merid-β a x)
     ∙ BigWedgeSuspEquivQuotient.split-glue-β (a , x)
 
-private  
+private
   Bouquet-to-BigWedgeSusp-is-equiv : is-equiv BouquetToBigWedgeSusp.f
   Bouquet-to-BigWedgeSusp-is-equiv = is-eq to from to-from from-to
-    where 
+    where
     to = BouquetToBigWedgeSusp.f
 
     module From = AttachedRec {A = ⊤}
@@ -70,7 +70,7 @@ private
             ( ap-∘ from (SphereToBigWedgeSusp.f a) (merid s)
             ∙ ap (ap from) (SphereToBigWedgeSusp.merid-β a s)
             ∙ From.spoke-β a s)
-            ∙v⊡ (tl-square (bwglue a) ⊡h vid-square)))
+            ∙v⊡ tl-square (bwglue a) ⊡h vid-square))
         (λ a → ↓-∘=idf-from-square from to $
           ap (ap from) (BouquetToBigWedgeSusp.glue-β a) ∙v⊡ br-square (bwglue a))
 
@@ -83,7 +83,7 @@ private
           ∙ ap2 _∙_ (BouquetToBigWedgeSusp.glue-β a)
                     ( ∘-ap to (bwin a) (merid s)
                     ∙ SphereToBigWedgeSusp.merid-β a s))
-  
+
   Bouquet-equiv-BigWedgeSusp : Bouquet cells (S n) ≃ BigWedgeSusp
   Bouquet-equiv-BigWedgeSusp = BouquetToBigWedgeSusp.f , Bouquet-to-BigWedgeSusp-is-equiv
 

theorems/groups/KernelImage.agda

@@ -24,7 +24,7 @@ module groups.KernelImage {i j k}
   ker/im-rel' h₁ h₂ = Trunc -1 (hfiber φ.f (H.diff h₁ h₂))
 
   ker/im-rel : Rel Kerψ.El (lmax i j)
-  ker/im-rel (h₁ , _) (h₂ , _) = Trunc -1 (hfiber φ.f (H.diff h₁ h₂))
+  ker/im-rel ker₁ ker₂ = Trunc -1 (hfiber φ.f (H.diff (fst ker₁) (fst ker₂)))
 
   private
     ker/im-El : Type (lmax (lmax i j) k)

theorems/index1.agda

@@ -48,7 +48,7 @@ import homotopy.SpaceFromGroups
 -- import homotopy.JoinAssoc3x3 -- commented out because this does not run on travis.
 
 {- covering spaces -}
-import homotopy.GroupSetsRepresentCovers
+-- import homotopy.GroupSetsRepresentCovers -- FIXME (broken by Agda 2.5.3 to 2.5.4 update)
 import homotopy.AnyUniversalCoverIsPathSet
 import homotopy.PathSetIsInitalCover
 import homotopy.CircleCover