Add properties of algebraic semilattices

CHANGELOG.md

@@ -58,17 +58,14 @@ Splitting up `Data.Maybe` into the standard hierarchy.
 * The fields `isEquivalence` and `∙-cong` in `IsSemigroup` have been
   replaced with `isMagma`.
 
-* The fields `isEquivalence`, `∨-cong`, `∨-assoc`, `∨-comm`, `∧-cong`,
-  `∧-assoc`  and `∧-comm` in `IsLattice` have been replaced with
-  `∨-isSemilattice` and `∧-isSemilattice`.
-
-* The record `Lattice` now exports proofs of `∨-idem` and `∧-idem` directly.
-  Therefore `∨-idempotence` and `∧-idempotence` in `Algebra.Properties.Lattice`
-  have been deprecated.
-
 * The record `BooleanAlgebra` now exports `∨-isSemigroup`, `∧-isSemigroup`
   directly  so `Algebra.Properties.BooleanAlgebra` no longer does so.
 
+* The proof that every algebraic lattice induces a partial order has been
+  moved from `Algebra.Properties.Lattice` to
+  `Algebra.Properties.Semilattice`.  The corresponding `poset` instance is
+  re-exported in `Algebra.Properties.Lattice`.
+
 #### Relaxation of ring solvers requirements
 
 * In the ring solvers below, the assumption that equality is `Decidable`
@@ -98,6 +95,8 @@ Splitting up `Data.Maybe` into the standard hierarchy.
 Other major changes
 -------------------
 
+* Added new module `Algebra.Properties.Semilattice`
+
 * Added new module `Algebra.FunctionProperties.Consequences.Propositional`
 
 * Added new module `Codata.Cowriter`
@@ -131,6 +130,14 @@ Other minor additions
   wlog : Commutative f → Total _R_ → (∀ a b → a R b → P (f a b)) → ∀ a b → P (f a b)
   ```
 
+* Added new proofs to `Algebra.Properties.Lattice`:
+  ```agda
+  ∧-isSemilattice : IsSemilattice _≈_ _∧_
+  ∧-semilattice : Semilattice l₁ l₂
+  ∨-isSemilattice : IsSemilattice _≈_ _∨_
+  ∨-semilattice : Semilattice l₁ l₂
+  ```
+
 * Added new operator to `Algebra.Solver.Ring`.
   ```agda
   _:×_
@@ -430,7 +437,7 @@ Other minor additions
   weak-lem     : ¬ ¬ (¬ x ∨ x) ≈ ⊤
   ```
 
-* Added new proofs to `Relation.Binary.Properties.JoinLattice`:
+* Added new proofs to `Relation.Binary.Properties.JoinSemilattice`:
   ```agda
   x≤y⇒x∨y≈y : x ≤ y → x ∨ y ≈ y
   ```
@@ -444,7 +451,7 @@ Other minor additions
   collapse₂      : x ∨ y ≤ x ∧ y → x ≈ y
   ```
 
-* Added new proofs to `Relation.Binary.Properties.MeetLattice`:
+* Added new proofs to `Relation.Binary.Properties.MeetSemilattice`:
   ```agda
   y≤x⇒x∧y≈y : y ≤ x → x ∧ y ≈ y
   ```

src/Algebra.agda

@@ -73,7 +73,6 @@ record Band c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semigroup semigroup public using (magma; rawMagma)
 
-
 record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
   infix  4 _≈_
@@ -566,27 +565,8 @@ record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open IsLattice isLattice public
 
-  ∨-semilattice : Semilattice c ℓ
-  ∨-semilattice = record { isSemilattice = ∨-isSemilattice }
-
-  open Semilattice ∨-semilattice public
-    using () renaming
-    ( rawMagma  to ∨-rawMagma
-    ; magma     to ∨-magma
-    ; semigroup to ∨-semigroup
-    ; band      to ∨-band
-    )
-
-  ∧-semilattice : Semilattice c ℓ
-  ∧-semilattice = record { isSemilattice = ∧-isSemilattice }
-
-  open Semilattice ∧-semilattice public
-    using () renaming
-    ( rawMagma  to ∧-rawMagma
-    ; magma     to ∧-magma
-    ; semigroup to ∧-semigroup
-    ; band      to ∧-band
-    )
+  setoid : Setoid _ _
+  setoid = record { isEquivalence = isEquivalence }
 
 record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
@@ -604,11 +584,7 @@ record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   lattice : Lattice _ _
   lattice = record { isLattice = isLattice }
 
-  open Lattice lattice public
-    using
-    ( ∧-rawMagma; ∧-magma; ∧-semigroup; ∧-band; ∧-semilattice
-    ; ∨-rawMagma; ∨-magma; ∨-semigroup; ∨-band; ∨-semilattice
-    )
+  open Lattice lattice public using (setoid)
 
 record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 ¬_
@@ -631,11 +607,8 @@ record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
   distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
 
   open DistributiveLattice distributiveLattice public
-    using
-    ( ∧-rawMagma; ∧-magma; ∧-semigroup; ∧-band; ∧-semilattice
-    ; ∨-rawMagma; ∨-magma; ∨-semigroup; ∨-band; ∨-semilattice
-    ; lattice
-    )
+    using (setoid; lattice)
+
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Algebra/Properties/BooleanAlgebra.agda

@@ -116,6 +116,30 @@ open import Data.Product
 ∨-zero : Zero ⊤ _∨_
 ∨-zero = ∨-zeroˡ , ∨-zeroʳ
 
+∨-isMagma : IsMagma _∨_
+∨-isMagma = record
+  { isEquivalence = isEquivalence
+  ; ∙-cong        = ∨-cong
+  }
+
+∧-isMagma : IsMagma _∧_
+∧-isMagma = record
+  { isEquivalence = isEquivalence
+  ; ∙-cong        = ∧-cong
+  }
+
+∨-isSemigroup : IsSemigroup _∨_
+∨-isSemigroup = record
+  { isMagma = ∨-isMagma
+  ; assoc   = ∨-assoc
+  }
+
+∧-isSemigroup : IsSemigroup _∧_
+∧-isSemigroup = record
+  { isMagma = ∧-isMagma
+  ; assoc   = ∧-assoc
+  }
+
 ∨-⊥-isMonoid : IsMonoid _∨_ ⊥
 ∨-⊥-isMonoid = record
   { isSemigroup = ∨-isSemigroup

src/Algebra/Properties/BooleanAlgebra/Expression.agda

@@ -116,56 +116,33 @@ lift n = record
   ; isBooleanAlgebra = record
     { isDistributiveLattice = record
       { isLattice = record
-        { ∨-isSemilattice = record
-          { isBand = record
-            { isSemigroup = record
-              { isMagma = record
-                { isEquivalence = PW.isEquivalence isEquivalence
-                ; ∙-cong        = λ xs≈us ys≈vs → ext λ i →
-                                    solve₁ i 4 (λ x y u v → x or y , u or v)
-                                      _ _ _ _
-                                      (∨-cong (Pointwise.app xs≈us i)
-                                        (Pointwise.app ys≈vs i))
-                }
-              ; assoc = λ _ _ _ → ext λ i →
-                          solve i 3
-                            (λ x y z → (x or y) or z , x or (y or z))
-                            (∨-assoc _ _ _) _ _ _
-              }
-            ; idem = λ _ → ext λ i →
-                          solve i 1
-                            (λ x → x or x , x) (∨-idem _) _
-            }
-          ; comm   = λ _ _ → ext λ i →
-                       solve i 2 (λ x y → x or y , y or x)
-                       (∨-comm _ _) _ _
-          }
-        ; ∧-isSemilattice = record
-          { isBand = record
-            { isSemigroup = record
-              { isMagma = record
-                { isEquivalence = PW.isEquivalence isEquivalence
-                ; ∙-cong        = λ xs≈ys us≈vs → ext λ i →
-                                    solve₁ i 4 (λ x y u v → x and y , u and v)
-                                      _ _ _ _
-                                      (∧-cong (Pointwise.app xs≈ys i)
-                                        (Pointwise.app us≈vs i))
-                }
-              ; assoc   = λ _ _ _ → ext λ i →
+        { isEquivalence = PW.isEquivalence isEquivalence
+        ; ∨-comm        = λ _ _ → ext λ i →
+                            solve i 2 (λ x y → x or y , y or x)
+                                  (∨-comm _ _) _ _
+        ; ∨-assoc       = λ _ _ _ → ext λ i →
+                            solve i 3
+                              (λ x y z → (x or y) or z , x or (y or z))
+                              (∨-assoc _ _ _) _ _ _
+        ; ∨-cong        = λ xs≈us ys≈vs → ext λ i →
+                            solve₁ i 4 (λ x y u v → x or y , u or v)
+                                   _ _ _ _
+                                   (∨-cong (Pointwise.app xs≈us i)
+                                           (Pointwise.app ys≈vs i))
+        ; ∧-comm        = λ _ _ → ext λ i →
+                            solve i 2 (λ x y → x and y , y and x)
+                                  (∧-comm _ _) _ _
+        ; ∧-assoc       = λ _ _ _ → ext λ i →
                             solve i 3
                               (λ x y z → (x and y) and z ,
                                          x and (y and z))
                               (∧-assoc _ _ _) _ _ _
-              }
-            ; idem        =  λ _ → ext λ i →
-                              solve i 1
-                                (λ x → x and x , x) (∧-idem _) _
-            }
-          ; comm   = λ _ _ → ext λ i →
-                       solve i 2 (λ x y → x and y , y and x)
-                       (∧-comm _ _) _ _
-          }
-        ; absorptive      =
+        ; ∧-cong        = λ xs≈ys us≈vs → ext λ i →
+                            solve₁ i 4 (λ x y u v → x and y , u and v)
+                                   _ _ _ _
+                                   (∧-cong (Pointwise.app xs≈ys i)
+                                           (Pointwise.app us≈vs i))
+        ; absorptive    =
           (λ _ _ → ext λ i →
             solve i 2 (λ x y → x or (x and y) , x) (∨-absorbs-∧ _ _) _ _) ,
           (λ _ _ → ext λ i →