Merge branch 'master' into unary-disjoint-relation

Author: jamesmckinna

CHANGELOG.md

@@ -13,6 +13,10 @@ Bug-fixes
   to `#-sym` in order to avoid overloaded projection.
   `irrefl` and `cotrans` are similarly renamed for the sake of consistency.
 
+* In `Algebra.Definitions.RawMagma` and `Relation.Binary.Construct.Interior.Symmetric`,
+  the record constructors `_,_` incorrectly had no declared fixity. They have been given
+  the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -24,6 +28,9 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
+  to its own dedicated module `Relation.Nullary.Irrelevant`.
+
 Deprecated modules
 ------------------
 
@@ -36,6 +43,12 @@ Deprecated names
   _∤∤_    ↦  _∦_
   ```
 
+* In `Algebra.Lattice.Properties.BooleanAlgebra`
+  ```agda
+  ⊥≉⊤   ↦  ¬⊥≈⊤
+  ⊤≉⊥   ↦  ¬⊤≈⊥
+  ```
+
 * In `Algebra.Module.Consequences`
   ```agda
   *ₗ-assoc+comm⇒*ᵣ-assoc      ↦  *ₗ-assoc∧comm⇒*ᵣ-assoc
@@ -44,6 +57,18 @@ Deprecated names
   *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
   ```
 
+* In `Algebra.Modules.Structures.IsLeftModule`:
+  ```agda
+  uniqueˡ‿⁻ᴹ   ↦  Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ
+  uniqueʳ‿⁻ᴹ   ↦  Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ
+  ```
+
+* In `Algebra.Modules.Structures.IsRightModule`:
+  ```agda
+  uniqueˡ‿⁻ᴹ   ↦  Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ
+  uniqueʳ‿⁻ᴹ   ↦  Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ
+  ```
+
 * In `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∣∣-sym       ↦  ∥-sym
@@ -54,18 +79,35 @@ 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 `Algebra.Structures.Group`:
+  ```agda
+  uniqueˡ-⁻¹   ↦  Algebra.Properties.Group.inverseˡ-unique
+  uniqueʳ-⁻¹   ↦  Algebra.Properties.Group.inverseʳ-unique
   ```
 
 * In `Data.List.Base`:
@@ -95,10 +137,18 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `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
 -----------------------------
 
@@ -131,6 +181,44 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Modules.Properties`:
+  ```agda
+  inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y
+  inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x
+  ```
+
+* 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
@@ -144,13 +232,28 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Relation.Binary.Construct.Add.Infimum.Strict`:
+  ```agda
+  <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋
+  <₋-accessible[_] : Acc _<_ x → Acc _<₋_ [ x ]
+  <₋-wellFounded   : WellFounded _<_ → WellFounded _<₋_
+  ```
+
+* In `Relation.Nullary.Decidable.Core`:
+  ```agda
+  ⊤-dec : Dec {a} ⊤
+  ⊥-dec : Dec {a} ⊥
+  ```
+
 * In `Relation.Unary`:
   ```agda
   _⊥_ _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
   ```
 
 * In `Relation.Unary.Properties`:
   ```agda
+  ≬-symmetric : Sym _≬_ _≬_
+  ⊥-symmetric : Sym _⊥_ _⊥_
   ≬-sym : Symmetric _≬_
   ⊥-sym : Symmetric _⊥_
   ≬⇒¬⊥ : _≬_ ⇒  (¬_ ∘₂ _⊥_)

src/Algebra/Apartness/Bundles.agda

@@ -13,7 +13,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (ApartnessRelation)
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Bundles using (CommutativeRing)
-open import Algebra.Apartness.Structures
+open import Algebra.Apartness.Structures using (IsHeytingCommutativeRing; IsHeytingField)
 
 record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 -_

src/Algebra/Bundles/Raw.agda

@@ -8,11 +8,10 @@
 
 module Algebra.Bundles.Raw where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles.Raw using (RawSetoid)
 open import Level using (suc; _⊔_)
-open import Relation.Nullary.Negation.Core using (¬_)
 
 ------------------------------------------------------------------------
 -- Raw bundles with 1 unary operation & 1 element

src/Algebra/Consequences/Base.agda

@@ -10,10 +10,11 @@
 module Algebra.Consequences.Base
   {a} {A : Set a} where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions
-open import Data.Sum.Base
-open import Relation.Binary.Core
+  using (Selective; Idempotent; SelfInverse; Involutive)
+open import Data.Sum.Base using (_⊎_; reduce)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive)
 
 module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where

src/Algebra/Consequences/Propositional.agda

@@ -19,8 +19,8 @@ open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
 open import Relation.Unary using (Pred)
+open import Algebra.Core using (Op₁; Op₂)
 
-open import Algebra.Core
 open import Algebra.Definitions {A = A} _≡_
 import Algebra.Consequences.Setoid (setoid A) as Base
 

src/Algebra/Consequences/Setoid.agda

@@ -7,7 +7,6 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions
   using (Substitutive; Symmetric; Total)
@@ -22,6 +21,7 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
 import Relation.Binary.Consequences as Bin
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Reasoning.Setoid S
 open import Relation.Unary using (Pred)
 

src/Algebra/Construct/Add/Identity.agda

@@ -9,17 +9,18 @@
 
 module Algebra.Construct.Add.Identity where
 
-open import Algebra.Bundles
+open import Algebra.Bundles using (Semigroup; Monoid)
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
-open import Algebra.Structures
-open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
+  using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
 open import Data.Product.Base using (_,_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary.Core
-open import Relation.Binary.Definitions
-open import Relation.Binary.Structures
-open import Relation.Nullary.Construct.Add.Point
+open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Nullary.Construct.Add.Point using (Pointed; [_]; ∙)
 
 private
   variable
@@ -101,3 +102,4 @@ monoid : Semigroup a (a ⊔ ℓ) → Monoid a (a ⊔ ℓ)
 monoid S = record
   { isMonoid = isMonoid S.isSemigroup
   } where module S = Semigroup S
+

src/Algebra/Construct/Initial.agda

@@ -21,7 +21,7 @@ open import Algebra.Bundles.Raw
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Congruent₂)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
-open import Data.Empty.Polymorphic
+open import Data.Empty.Polymorphic using (⊥)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.Definitions

src/Algebra/Construct/LiftedChoice.agda

@@ -10,7 +10,7 @@ open import Algebra
 
 module Algebra.Construct.LiftedChoice where
 
-open import Algebra.Consequences.Base
+open import Algebra.Consequences.Base using (sel⇒idem)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
 open import Data.Product.Base using (_×_; _,_)
 open import Function.Base using (const; _$_)

src/Algebra/Construct/NaturalChoice/Base.agda

@@ -7,7 +7,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
+open import Algebra.Core using (Op₂)
 open import Level as L hiding (_⊔_)
 open import Function.Base using (flip)
 open import Relation.Binary.Bundles using (TotalPreorder)

src/Algebra/Construct/NaturalChoice/Max.agda

@@ -11,9 +11,8 @@ open import Relation.Binary.Bundles using (TotalOrder)
 module Algebra.Construct.NaturalChoice.Max
   {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where
 
-open import Algebra.Core
-open import Algebra.Definitions
-open import Algebra.Construct.NaturalChoice.Base
+open import Algebra.Core using (Op₂)
+open import Algebra.Construct.NaturalChoice.Base using (MaxOperator)
 open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalOrder to flip)
 

src/Algebra/Construct/NaturalChoice/MaxOp.agda

@@ -7,21 +7,21 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
-open import Algebra.Construct.NaturalChoice.Base
-import Algebra.Construct.NaturalChoice.MinOp as MinOp
-open import Function.Base using (flip)
-open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Algebra.Construct.NaturalChoice.Base using (MaxOperator; MaxOp⇒MinOp)
 open import Relation.Binary.Bundles using (TotalPreorder)
-open import Relation.Binary.Construct.Flip.EqAndOrd using ()
-  renaming (totalPreorder to flipOrder)
 
 module Algebra.Construct.NaturalChoice.MaxOp
   {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
   where
 
-open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)
+import Algebra.Construct.NaturalChoice.MinOp as MinOp
+open import Algebra.Core using (Op₂)
+open import Function.Base using (flip)
 open MaxOperator maxOp
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.Construct.Flip.EqAndOrd using ()
+  renaming (totalPreorder to flipOrder)
+open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)
 
 -- Max is just min with a flipped order
 

src/Algebra/Construct/NaturalChoice/Min.agda

@@ -6,19 +6,18 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
-open import Algebra.Bundles
-open import Algebra.Construct.NaturalChoice.Base
-open import Data.Sum.Base using (inj₁; inj₂; [_,_])
-open import Data.Product.Base using (_,_)
-open import Function.Base using (id)
 open import Relation.Binary.Bundles using (TotalOrder)
-import Algebra.Construct.NaturalChoice.MinOp as MinOp
 
 module Algebra.Construct.NaturalChoice.Min
   {a ℓ₁ ℓ₂} (O : TotalOrder a ℓ₁ ℓ₂)
   where
 
+open import Algebra.Core using (Op₂)
+open import Algebra.Construct.NaturalChoice.Base
+import Algebra.Construct.NaturalChoice.MinOp as MinOp
+open import Data.Sum.Base using (inj₁; inj₂; [_,_])
+open import Data.Product.Base using (_,_)
+open import Function.Base using (id)
 open TotalOrder O renaming (Carrier to A)
 
 ------------------------------------------------------------------------

src/Algebra/Construct/NaturalChoice/MinMaxOp.agda

@@ -7,22 +7,20 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
-open import Algebra.Bundles
-open import Algebra.Construct.NaturalChoice.Base
-open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
-open import Data.Product.Base using (_,_)
-open import Function.Base using (id; _∘_; flip)
-open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator)
 open import Relation.Binary.Bundles using (TotalPreorder)
-open import Relation.Binary.Consequences
 
 module Algebra.Construct.NaturalChoice.MinMaxOp
   {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂}
   (minOp : MinOperator O)
   (maxOp : MaxOperator O)
   where
 
+open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
+open import Data.Product.Base using (_,_)
+open import Function.Base using (id; _∘_; flip)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+
 open TotalPreorder O renaming
   ( Carrier   to A
   ; _≲_       to _≤_