diff --git a/core/lib/types/Pushout.agda b/core/lib/types/Pushout.agda index 13d563b0..8f2a7b5c 100644 --- a/core/lib/types/Pushout.agda +++ b/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 diff --git a/theorems/cohomology/SpectrumModel.agda b/theorems/cohomology/SpectrumModel.agda index 78f5db8d..0245eade 100644 --- a/theorems/cohomology/SpectrumModel.agda +++ b/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 diff --git a/theorems/cw/Attached.agda b/theorems/cw/Attached.agda index 2d722574..92ea0136 100644 --- a/theorems/cw/Attached.agda +++ b/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) diff --git a/theorems/cw/WedgeOfCells.agda b/theorems/cw/WedgeOfCells.agda index 0f595159..5f3be18a 100644 --- a/theorems/cw/WedgeOfCells.agda +++ b/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 diff --git a/theorems/groups/KernelImage.agda b/theorems/groups/KernelImage.agda index 778621ce..780b08bf 100644 --- a/theorems/groups/KernelImage.agda +++ b/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) diff --git a/theorems/index1.agda b/theorems/index1.agda index f9f2c9bd..ad78b993 100644 --- a/theorems/index1.agda +++ b/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