fixes

Author: aljungstrom

Cubical/Algebra/AbGroup/FinitePresentation.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --safe #-}
 module Cubical.Algebra.AbGroup.FinitePresentation where
 
 open import Cubical.Foundations.Prelude
@@ -26,8 +25,7 @@ record FinitePresentation (A : AbGroup ℓ) : Type ℓ where
     nGens : ℕ
     nRels : ℕ
     rels : AbGroupHom ℤ[Fin nRels ] ℤ[Fin nGens ]
-    fpiso : GroupIso (AbGroup→Group A)
-                     (ℤ[Fin nGens ] /Im rels)
+    fpiso : AbGroupIso A (ℤ[Fin nGens ] /Im rels)
 
 isFinitelyPresented : AbGroup ℓ → Type ℓ
 isFinitelyPresented G = ∥ FinitePresentation G ∥₁

Cubical/Algebra/AbGroup/Properties.agda

@@ -61,14 +61,15 @@ subtrGroupHom : (A : AbGroup ℓ) (B : AbGroup ℓ') (ϕ ψ : AbGroupHom A B) 
 subtrGroupHom A B ϕ ψ = addGroupHom A B ϕ (negGroupHom A B ψ)
 
 -- Abelian groups quotiented by image of a map
-_/Im_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → Group ℓ
-G /Im ϕ = AbGroup→Group G
-        / (imSubgroup ϕ , isNormalIm ϕ λ _ _ → AbGroupStr.+Comm (snd G) _ _)
-
-_/ᵃᵇIm_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → AbGroup ℓ
-G /ᵃᵇIm ϕ =
-  Group→AbGroup (G /Im ϕ)
+_/Im_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → AbGroup ℓ
+G /Im ϕ =
+  Group→AbGroup (G /' ϕ)
     (elimProp2 (λ _ _ → squash/ _ _) λ a b → cong [_] (AbGroupStr.+Comm (snd G) _ _))
+  where
+  _/'_ : {H : Group ℓ} (G : AbGroup ℓ) (ϕ : GroupHom H (AbGroup→Group G)) → Group ℓ
+  G /' ϕ = AbGroup→Group G
+          / (imSubgroup ϕ , isNormalIm ϕ λ _ _ → AbGroupStr.+Comm (snd G) _ _)
+
 
 -- ℤ-multiplication defines a homomorphism for abelian groups
 private module _ (G : AbGroup ℓ) where
@@ -112,7 +113,7 @@ snd (multₗHom G n) = makeIsGroupHom (ℤ·isHom n G)
 
 -- Abelian groups quotiented by a natural number
 _/^_ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ
-G /^ n = G /ᵃᵇIm multₗHom G (pos n)
+G /^ n = G /Im multₗHom G (pos n)
 
 -- Torsion subgrous
 _[_]ₜ : (G : AbGroup ℓ) (n : ℕ) → AbGroup ℓ

Cubical/CW/Homology/Groups/CofibFinSphereBouquetMap.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --lossy-unification #-}
+{-# OPTIONS --lossy-unification #-}
 {-
 File contains : a proof that Hₙ₊₁(cofib α) ≅ ℤ[e]/Im(deg α) for
 α : ⋁ₐ Sⁿ → ⋁ₑ Sⁿ (with a and e finite sets)

Cubical/CW/Homology/Groups/Sn.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --lossy-unification #-}
+{-# OPTIONS --lossy-unification #-}
 module Cubical.CW.Homology.Groups.Sn where
 
 open import Cubical.Foundations.Prelude

Cubical/CW/Homology/Groups/Subcomplex.agda

@@ -1,17 +1,17 @@
-{-# OPTIONS --safe --lossy-unification #-}
+{-# OPTIONS --lossy-unification #-}
 
 {-
 This file contains a definition of a notion of (strict)
-subcomplexes of a CW complex. Here, a subomplex of a complex
+subcomplexes of a CW complex. Here, a subcomplex of a complex
 C = colim ( C₀ → C₁ → ...)
 is simply the complex
 C⁽ⁿ⁾ := colim (C₀ → ... → Cₙ = Cₙ = ...)
 
 This file contains.
 1. Definition of above
 2. A `strictification' of finite CW complexes in terms of above
-3. An elmination principle for finite CW complexes
-4. A proof that C and C⁽ⁿ⁾ has the same homolog in appropriate dimensions.
+3. An elimination principle for finite CW complexes
+4. A proof that C and C⁽ⁿ⁾ has the same homology in appropriate dimensions.
 -}
 
 module Cubical.CW.Homology.Groups.Subcomplex where

Cubical/CW/HurewiczTheorem.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --lossy-unification #-}
+{-# OPTIONS --lossy-unification #-}
 {-
 This file contains
 1. a construction of the Hurewicz map πₙᵃᵇ(X) → H̃ᶜʷₙ(X),

Cubical/CW/Instances/Empty.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --safe #-}
 {-
 The empty type as a CW complex
 -}

Cubical/CW/Instances/Join.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --safe #-}
 {-
 CW structure on joins
 -}

Cubical/CW/Instances/Lift.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --safe #-}
 {-
 Universe lifts of CW complexes
 -}

Cubical/CW/Instances/Pushout.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --safe #-}
 module Cubical.CW.Instances.Pushout where
 
 open import Cubical.Foundations.Prelude