Merge branch 'master' into import43

Author: jamesmckinna

CHANGELOG.md

@@ -58,18 +58,29 @@ Deprecated names
   ∤∤-respˡ-≈    ↦  ∦-respˡ-≈
   ∤∤-respʳ-≈    ↦  ∦-respʳ-≈
   ∤∤-resp-≈     ↦  ∦-resp-≈
+  ∣-respʳ-≈    ↦ ∣ʳ-respʳ-≈
+  ∣-respˡ-≈    ↦ ∣ʳ-respˡ-≈
+  ∣-resp-≈     ↦ ∣ʳ-resp-≈
+  x∣yx         ↦ x∣ʳyx
+  xy≈z⇒y∣z     ↦ xy≈z⇒y∣ʳz
   ```
 
 * In `Algebra.Properties.Monoid.Divisibility`:
   ```agda
   ∣∣-refl            ↦  ∥-refl
   ∣∣-reflexive       ↦  ∥-reflexive
   ∣∣-isEquivalence   ↦  ∥-isEquivalence
+  ε∣_                ↦ ε∣ʳ_
+  ∣-refl             ↦ ∣ʳ-refl
+  ∣-reflexive        ↦ ∣ʳ-reflexive
+  ∣-isPreorder       ↦ ∣ʳ-isPreorder
+  ∣-preorder         ↦ ∣ʳ-preorder
   ```
 
 * In `Algebra.Properties.Semigroup.Divisibility`:
   ```agda
   ∣∣-trans   ↦  ∥-trans
+  ∣-trans    ↦  ∣ʳ-trans
   ```
 
 * In `Data.List.Base`:
@@ -103,6 +114,10 @@ New modules
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
 
+* `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid.
+
+* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid.
+
 * `Data.Sign.Show` to show a sign
 
 Additions to existing modules
@@ -137,6 +152,38 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Properties.Magma.Divisibility`:
+  ```agda
+  ∣ˡ-respʳ-≈  : _∣ˡ_ Respectsʳ _≈_
+  ∣ˡ-respˡ-≈  : _∣ˡ_ Respectsˡ _≈_
+  ∣ˡ-resp-≈   : _∣ˡ_ Respects₂ _≈_
+  x∣ˡxy       : ∀ x y → x ∣ˡ x ∙ y
+  xy≈z⇒x∣ˡz   : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z
+  ```
+
+* In `Algebra.Properties.Monoid.Divisibility`:
+  ```agda
+  ε∣ˡ_          : ∀ x → ε ∣ˡ x
+  ∣ˡ-refl       : Reflexive _∣ˡ_
+  ∣ˡ-reflexive  : _≈_ ⇒ _∣ˡ_
+  ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_
+  ∣ˡ-preorder   : Preorder a ℓ _
+  ```
+
+* In `Algebra.Properties.Semigroup.Divisibility`:
+  ```agda
+  ∣ˡ-trans     : Transitive _∣ˡ_
+  x∣ʳy⇒x∣ʳzy   : x ∣ʳ y → x ∣ʳ z ∙ y
+  x∣ʳy⇒xz∣ʳyz  : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z
+  x∣ˡy⇒zx∣ˡzy  : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y
+  x∣ˡy⇒x∣ˡyz   : x ∣ˡ y → x ∣ˡ y ∙ z
+  ```
+
+* In `Algebra.Properties.CommutativeSemigroup.Divisibility`:
+  ```agda
+  ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
@@ -149,3 +196,9 @@ Additions to existing modules
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
+
+* In `Relation.Nullary.Decidable.Core`:
+  ```agda
+  ⊤-dec : Dec {a} ⊤
+  ⊥-dec : Dec {a} ⊥
+  ```

src/Algebra/Lattice/Bundles.agda

@@ -15,11 +15,14 @@
 
 module Algebra.Lattice.Bundles where
 
-open import Algebra.Core
-open import Algebra.Bundles
-open import Algebra.Structures
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Bundles using (Band)
 import Algebra.Lattice.Bundles.Raw as Raw
 open import Algebra.Lattice.Structures
+  using ( IsSemilattice; IsMeetSemilattice; IsJoinSemilattice
+        ; IsBoundedSemilattice; IsBoundedMeetSemilattice
+        ; IsBoundedJoinSemilattice; IsLattice; IsDistributiveLattice
+        ; IsBooleanAlgebra)
 open import Level using (suc; _⊔_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Core using (Rel)

src/Algebra/Lattice/Structures.agda

@@ -13,7 +13,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)

src/Algebra/Module/Bundles/Raw.agda

@@ -8,10 +8,10 @@
 
 module Algebra.Module.Bundles.Raw where
 
-open import Algebra.Bundles.Raw
-open import Algebra.Core
-open import Algebra.Module.Core
-open import Level
+open import Algebra.Bundles.Raw using (RawMonoid; RawGroup)
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Module.Core using (Opₗ; Opᵣ)
+open import Level using (Level; _⊔_; suc)
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.Core using (Rel)
 

src/Algebra/Module/Construct/DirectProduct.agda

@@ -12,11 +12,12 @@
 module Algebra.Module.Construct.DirectProduct where
 
 open import Algebra.Bundles
-open import Algebra.Construct.DirectProduct
+open import Algebra.Construct.DirectProduct using (commutativeMonoid)
 open import Algebra.Module.Bundles
 open import Data.Product.Base using (map; zip; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-open import Level
+  using (Pointwise)
+open import Level using (Level; _⊔_)
 
 private
   variable

src/Algebra/Module/Construct/Idealization.agda

@@ -37,11 +37,13 @@ open import Algebra.Module.Bundles using (Bimodule)
 module Algebra.Module.Construct.Idealization
   {r ℓr m ℓm} (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where
 
-open import Algebra.Core
-import Algebra.Consequences.Setoid as Consequences
+open import Algebra.Core using (Op₂)
+import Algebra.Consequences.Setoid as Consequences using (comm∧assoc⇒middleFour)
 import Algebra.Definitions as Definitions
-import Algebra.Module.Construct.DirectProduct as DirectProduct
-import Algebra.Module.Construct.TensorUnit as TensorUnit
+  using (Congruent₂; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_
+        ; LeftIdentity; RightIdentity; Identity; Associative)
+import Algebra.Module.Construct.DirectProduct as DirectProduct using (bimodule)
+import Algebra.Module.Construct.TensorUnit as TensorUnit using (bimodule)
 open import Algebra.Structures using (IsAbelianGroup; IsRing)
 open import Data.Product.Base using (_,_; ∃-syntax)
 open import Level using (Level; _⊔_)

src/Algebra/Module/Construct/TensorUnit.agda

@@ -12,8 +12,14 @@
 module Algebra.Module.Construct.TensorUnit where
 
 open import Algebra.Bundles
+  using (RawSemiring; RawRing; Semiring; Ring; CommutativeSemiring
+        ; CommutativeRing)
 open import Algebra.Module.Bundles
-open import Level
+  using (RawSemimodule; RawLeftSemimodule; RawRightSemimodule; RawBisemimodule
+        ; RawLeftModule; RawRightModule; RawBimodule; RawModule; LeftSemimodule
+        ; RightSemimodule; Bisemimodule; Semimodule; LeftModule; RightModule; Bimodule
+        ; Module)
+open import Level  using (Level; _⊔_)
 
 private
   variable

src/Algebra/Module/Construct/Zero.agda

@@ -10,13 +10,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Level
+open import Level using (Level)
 
 module Algebra.Module.Construct.Zero {c ℓ : Level} where
 
-open import Algebra.Bundles
+open import Algebra.Bundles using (RawSemiring; Semiring; Ring; CommutativeSemiring; CommutativeRing)
 open import Algebra.Module.Bundles
-open import Data.Unit.Polymorphic
+open import Data.Unit.Polymorphic using (⊤)
 open import Relation.Binary.Core using (Rel)
 
 private

src/Algebra/Properties/AbelianGroup.agda

@@ -6,13 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (AbelianGroup)
 
 module Algebra.Properties.AbelianGroup
   {a ℓ} (G : AbelianGroup a ℓ) where
 
-open AbelianGroup G
 open import Function.Base using (_$_)
+
+open AbelianGroup G
 open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -6,17 +6,18 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra using (CancellativeCommutativeSemiring)
+open import Algebra.Bundles using (CancellativeCommutativeSemiring)
+
+module Algebra.Properties.CancellativeCommutativeSemiring
+  {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
+  where
+
 open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 
-module Algebra.Properties.CancellativeCommutativeSemiring
-  {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)
-  where
-
 open CancellativeCommutativeSemiring R
 open import Algebra.Consequences.Setoid setoid
 open import Relation.Binary.Reasoning.Setoid setoid