[ refactor ] Algebra.Properties.Semiring.Divisibility and friends

src/Algebra/Properties/Magma/Divisibility.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Magma)
+open import Algebra.Bundles using (Magma)
 
 module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where
 

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -6,16 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Monoid)
+open import Algebra.Bundles using (Monoid)
+
+module Algebra.Properties.Monoid.Divisibility
+  {a ℓ} (M : Monoid a ℓ) where
+
 open import Data.Product.Base using (_,_)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles using (Preorder)
 open import Relation.Binary.Structures using (IsPreorder; IsEquivalence)
 open import Relation.Binary.Definitions using (Reflexive)
 
-module Algebra.Properties.Monoid.Divisibility
-  {a ℓ} (M : Monoid a ℓ) where
-
 open Monoid M
 
 ------------------------------------------------------------------------
@@ -60,9 +61,9 @@ infix 4 ε∣_
 
 ∥-isEquivalence : IsEquivalence _∥_
 ∥-isEquivalence = record
-  { refl  = λ {x} → ∥-refl {x}
-  ; sym   = λ {x} {y} → ∥-sym {x} {y}
-  ; trans = λ {x} {y} {z} → ∥-trans {x} {y} {z}
+  { refl  = ∥-refl
+  ; sym   = ∥-sym
+  ; trans = ∥-trans
   }
 
 

src/Algebra/Properties/Semigroup/Divisibility.agda

@@ -6,13 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Semigroup)
-open import Data.Product.Base using (_,_)
-open import Relation.Binary.Definitions using (Transitive)
+open import Algebra.Bundles using (Semigroup)
 
 module Algebra.Properties.Semigroup.Divisibility
   {a ℓ} (S : Semigroup a ℓ) where
 
+open import Data.Product.Base using (_,_)
+open import Relation.Binary.Definitions using (Transitive)
+
 open Semigroup S
 
 ------------------------------------------------------------------------

src/Algebra/Properties/Semiring/Divisibility.agda

@@ -6,10 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Semiring)
-import Algebra.Properties.Monoid.Divisibility as MonoidDivisibility
-open import Data.Product.Base using (_,_)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Algebra.Bundles using (Semiring)
 
 module Algebra.Properties.Semiring.Divisibility
   {a ℓ} (R : Semiring a ℓ) where
@@ -19,7 +16,7 @@ open Semiring R
 ------------------------------------------------------------------------
 -- Re-exporting divisibility over monoids
 
-open MonoidDivisibility *-monoid public
+open import Algebra.Properties.Monoid.Divisibility *-monoid public
   renaming (ε∣_ to 1∣_)
 
 ------------------------------------------------------------------------
@@ -37,4 +34,4 @@ x∣y∧y≉0⇒x≉0 : ∀ {x y} → x ∣ y → y ≉ 0# → x ≉ 0#
 x∣y∧y≉0⇒x≉0 x∣y y≉0 x≈0 = y≉0 (0∣x⇒x≈0 (∣-respˡ x≈0 x∣y))
 
 0∤1 : 0# ≉ 1# → 0# ∤ 1#
-0∤1 0≉1 (q , q*0≈1) = 0≉1 (trans (sym (zeroʳ q)) q*0≈1)
+0∤1 0≉1 0∣1 = 0≉1 (sym (0∣x⇒x≈0 0∣1))

src/Algebra/Properties/Semiring/Primality.agda

@@ -1,22 +1,29 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some theory for CancellativeCommutativeSemiring.
+-- Properties of Coprimality and Irreducibility for Semiring.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (Semiring)
-open import Data.Sum.Base using (reduce)
-open import Function.Base using (flip)
-open import Relation.Binary.Definitions using (Symmetric)
+open import Algebra.Bundles using (Semiring)
 
 module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)
   where
 
+open import Data.Sum.Base using (reduce)
+open import Function.Base using (flip)
+open import Relation.Binary.Definitions using (Symmetric)
+
 open Semiring R renaming (Carrier to A)
 open import Algebra.Properties.Semiring.Divisibility R
+  using (_∣_; ∣-trans; 0∤1)
+
+private
+  variable
+    x p : A
+
 
 ------------------------------------------------------------------------
 -- Re-export primality definitions
@@ -30,12 +37,12 @@ open import Algebra.Definitions.RawSemiring rawSemiring public
 Coprime-sym : Symmetric Coprime
 Coprime-sym coprime = flip coprime
 
-∣1⇒Coprime : ∀ {x} y → x ∣ 1# → Coprime x y
-∣1⇒Coprime {x} y x∣1 z∣x _ = ∣-trans z∣x x∣1
+∣1⇒Coprime : ∀ y → x ∣ 1# → Coprime x y
+∣1⇒Coprime _ x∣1 z∣x _ = ∣-trans z∣x x∣1
 
 ------------------------------------------------------------------------
 -- Properties of Irreducible
 
-Irreducible⇒≉0 : 0# ≉ 1# → ∀ {p} → Irreducible p → p ≉ 0#
+Irreducible⇒≉0 : 0# ≉ 1# → Irreducible p → p ≉ 0#
 Irreducible⇒≉0 0≉1 (mkIrred _ chooseInvertible) p≈0 =
   0∤1 0≉1 (reduce (chooseInvertible (trans p≈0 (sym (zeroˡ 0#)))))