Level polymorphism for Algebra.Construct.Zero and Algebra.Module.Construct.Zero (#1323)

Author: conal

CHANGELOG.md

@@ -20,6 +20,7 @@ Non-backwards compatible changes
 * The internal build utilities package `lib.cabal` has been renamed
   `agda-stdlib-utils.cabal` to avoid potential conflict or confusion.
   Please note that the package is not intended for external use.
+* The module `Algebra.Construct.Zero` and `Algebra.Module.Construct.Zero` are now level-polymorphic, each taking two implicit level parameters.
 
 Deprecated modules
 ------------------

src/Algebra/Construct/Zero.agda

@@ -13,53 +13,54 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Algebra.Construct.Zero where
+open import Level using (Level)
+
+module Algebra.Construct.Zero {c ℓ : Level} where
 
 open import Algebra.Bundles
-open import Data.Unit
-open import Level using (Level; 0ℓ)
+open import Data.Unit.Polymorphic
 
 ------------------------------------------------------------------------
 -- Raw bundles
 
-rawMagma : RawMagma 0ℓ 0ℓ
+rawMagma : RawMagma c ℓ
 rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-rawMonoid : RawMonoid 0ℓ 0ℓ
+rawMonoid : RawMonoid c ℓ
 rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-rawGroup : RawGroup 0ℓ 0ℓ
+rawGroup : RawGroup c ℓ
 rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
 ------------------------------------------------------------------------
 -- Bundles
 
-magma : Magma 0ℓ 0ℓ
+magma : Magma c ℓ
 magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-semigroup : Semigroup 0ℓ 0ℓ
+semigroup : Semigroup c ℓ
 semigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-band : Band 0ℓ 0ℓ
+band : Band c ℓ
 band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+commutativeSemigroup : CommutativeSemigroup c ℓ
 commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-semilattice : Semilattice 0ℓ 0ℓ
+semilattice : Semilattice c ℓ
 semilattice = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-monoid : Monoid 0ℓ 0ℓ
+monoid : Monoid c ℓ
 monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+commutativeMonoid : CommutativeMonoid c ℓ
 commutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
+idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
 idempotentCommutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-group : Group 0ℓ 0ℓ
+group : Group c ℓ
 group = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
 
-abelianGroup : AbelianGroup 0ℓ 0ℓ
+abelianGroup : AbelianGroup c ℓ
 abelianGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }

src/Algebra/Module/Construct/Zero.agda

@@ -10,61 +10,62 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Algebra.Module.Construct.Zero where
+open import Level
+
+module Algebra.Module.Construct.Zero {c ℓ : Level} where
 
 open import Algebra.Bundles
 open import Algebra.Module.Bundles
-open import Data.Unit
-open import Level
+open import Data.Unit.Polymorphic
 
 private
   variable
     r s ℓr ℓs : Level
 
-leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R 0ℓ 0ℓ
+leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R c ℓ
 leftSemimodule = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤
   }
 
-rightSemimodule : {S : Semiring s ℓs} → RightSemimodule S 0ℓ 0ℓ
+rightSemimodule : {S : Semiring s ℓs} → RightSemimodule S c ℓ
 rightSemimodule = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤
   }
 
 bisemimodule :
-  {R : Semiring r ℓr} {S : Semiring s ℓs} → Bisemimodule R S 0ℓ 0ℓ
+  {R : Semiring r ℓr} {S : Semiring s ℓs} → Bisemimodule R S c ℓ
 bisemimodule = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤
   }
 
-semimodule : {R : CommutativeSemiring r ℓr} → Semimodule R 0ℓ 0ℓ
+semimodule : {R : CommutativeSemiring r ℓr} → Semimodule R c ℓ
 semimodule = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤
   }
 
-leftModule : {R : Ring r ℓr} → LeftModule R 0ℓ 0ℓ
+leftModule : {R : Ring r ℓr} → LeftModule R c ℓ
 leftModule = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤
   }
 
-rightModule : {S : Ring s ℓs} → RightModule S 0ℓ 0ℓ
+rightModule : {S : Ring s ℓs} → RightModule S c ℓ
 rightModule = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤
   }
 
-bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S 0ℓ 0ℓ
+bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S c ℓ
 bimodule = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤
   }
 
-⟨module⟩ : {R : CommutativeRing r ℓr} → Module R 0ℓ 0ℓ
+⟨module⟩ : {R : CommutativeRing r ℓr} → Module R c ℓ
 ⟨module⟩ = record
   { Carrierᴹ = ⊤
   ; _≈ᴹ_ = λ _ _ → ⊤