WIP: agda#396, enforce rules for imports

felixwellen · May 4, 2022 · 171c134 · 171c134
1 parent aa2ada9
commit 171c134
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 13 deletions.
diff --git a/Cubical/Algebra/AbGroup/TensorProduct.agda b/Cubical/Algebra/AbGroup/TensorProduct.agda
@@ -21,7 +21,7 @@ open import Cubical.Data.Sum hiding (map)
 open import Cubical.HITs.PropositionalTruncation
   renaming (map to pMap ; rec to pRec ; elim to pElim ; elim2 to pElim2)
 
-open import Cubical.Algebra.Group hiding (ℤ)
+open import Cubical.Algebra.Group
 open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.Group.MorphismProperties
 open import Cubical.Algebra.Monoid

diff --git a/Cubical/Algebra/Polynomials/Univariate/Base.agda b/Cubical/Algebra/Polynomials/Univariate/Base.agda
@@ -18,7 +18,7 @@ open import Cubical.Data.Nat.Order
 open import Cubical.Data.Empty.Base renaming (rec to ⊥rec )
 open import Cubical.Data.Bool hiding (_≤_)
 
-open import Cubical.Algebra.Group hiding (Bool)
+open import Cubical.Algebra.Group
 open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
 

diff --git a/Cubical/ZCohomology/Properties.agda b/Cubical/ZCohomology/Properties.agda
@@ -15,11 +15,6 @@ This module contains:
 -}
 
 
-open import Cubical.ZCohomology.Base
-open import Cubical.ZCohomology.GroupStructure
-
-open import Cubical.HITs.S1 hiding (encode ; decode ; _·_)
-open import Cubical.HITs.Sn
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Function
@@ -30,21 +25,33 @@ open import Cubical.Foundations.Pointed.Homogeneous
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.GroupoidLaws renaming (assoc to assoc∙)
 open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Equiv.HalfAdjoint
+
+open import Cubical.Functions.Morphism
+
 open import Cubical.HITs.Susp
 open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim ; elim2 to sElim2 ; isSetSetTrunc to §)
+open import Cubical.HITs.S1 hiding (encode ; decode ; _·_)
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; map2 to trMap2; rec to trRec ; elim3 to trElim3)
+
+open import Cubical.Data.Sum.Base hiding (map)
 open import Cubical.Data.Int renaming (_+_ to _ℤ+_) hiding (-_)
 open import Cubical.Data.Nat
-open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; map2 to trMap2; rec to trRec ; elim3 to trElim3)
+open import Cubical.Data.Sigma
+
 open import Cubical.Homotopy.Loopspace
 open import Cubical.Homotopy.Connected
-open import Cubical.Algebra.Group hiding (ℤ)
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
 open import Cubical.Algebra.AbGroup
 open import Cubical.Algebra.Semigroup
 open import Cubical.Algebra.Monoid
-open import Cubical.Foundations.Equiv.HalfAdjoint
-open import Cubical.Data.Sum.Base hiding (map)
-open import Cubical.Functions.Morphism
-open import Cubical.Data.Sigma
+
+open import Cubical.ZCohomology.Base
+open import Cubical.ZCohomology.GroupStructure
 
 open Iso renaming (inv to inv')