diff --git a/CHANGELOG.md b/CHANGELOG.md
index 45f4560372..1d08875d31 100644
--- a/CHANGELOG.md
+++ b/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
   ```
diff --git a/src/Algebra.agda b/src/Algebra.agda
index 6f22bb061e..99cd8f6472 100644
--- a/src/Algebra.agda
+++ b/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
diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda
index 262175f438..ce2624129d 100644
--- a/src/Algebra/Properties/BooleanAlgebra.agda
+++ b/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
diff --git a/src/Algebra/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Properties/BooleanAlgebra/Expression.agda
index 48cd7d3ca2..b1e2d9cf3e 100644
--- a/src/Algebra/Properties/BooleanAlgebra/Expression.agda
+++ b/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 →
diff --git a/src/Algebra/Properties/Lattice.agda b/src/Algebra/Properties/Lattice.agda
index d7f3f2c78d..82bd425153 100644
--- a/src/Algebra/Properties/Lattice.agda
+++ b/src/Algebra/Properties/Lattice.agda
@@ -11,6 +11,7 @@ module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where
 open Lattice L
 open import Algebra.Structures
 open import Algebra.FunctionProperties _≈_
+import Algebra.Properties.Semilattice as SL
 open import Relation.Binary
 import Relation.Binary.Lattice as R
 open import Relation.Binary.EqReasoning  setoid
@@ -20,100 +21,114 @@ open import Function.Equivalence using (_⇔_; module Equivalence)
 open import Data.Product using (_,_; swap)
 
 ------------------------------------------------------------------------
--- The dual construction is also a lattice.
-
-∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
-∧-∨-isLattice = record
-  { ∨-isSemilattice = ∧-isSemilattice
-  ; ∧-isSemilattice = ∨-isSemilattice
-  ; absorptive      = swap absorptive
+-- Every lattice contains two semilattices.
+
+∧-idempotent : Idempotent _∧_
+∧-idempotent x = begin
+  x ∧ x            ≈⟨ refl ⟨ ∧-cong ⟩ sym (∨-absorbs-∧ _ _) ⟩
+  x ∧ (x ∨ x ∧ x)  ≈⟨ ∧-absorbs-∨ _ _ ⟩
+  x                ∎
+
+∨-idempotent : Idempotent _∨_
+∨-idempotent x = begin
+  x ∨ x      ≈⟨ refl ⟨ ∨-cong ⟩ sym (∧-idempotent _) ⟩
+  x ∨ x ∧ x  ≈⟨ ∨-absorbs-∧ _ _ ⟩
+  x          ∎
+
+∧-isSemilattice : IsSemilattice _≈_ _∧_
+∧-isSemilattice = record
+  { isBand = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = isEquivalence
+        ; ∙-cong        = ∧-cong
+        }
+      ; assoc         = ∧-assoc
+      }
+    ; idem = ∧-idempotent
+    }
+  ; comm   = ∧-comm
   }
 
-∧-∨-lattice : Lattice _ _
-∧-∨-lattice = record { isLattice = ∧-∨-isLattice }
+∧-semilattice : Semilattice l₁ l₂
+∧-semilattice = record { isSemilattice = ∧-isSemilattice }
 
-------------------------------------------------------------------------
--- Every lattice can be turned into a poset.
-
-poset : Poset _ _ _
-poset = record
-  { Carrier        = Carrier
-  ; _≈_            = _≈_
-  ; _≤_            = λ x y → x ≈ x ∧ y
-  ; isPartialOrder = record
-    { isPreorder = record
-      { isEquivalence = isEquivalence
-      ; reflexive     = λ {i} {j} i≈j → begin
-                          i      ≈⟨ sym $ ∧-idem _ ⟩
-                          i ∧ i  ≈⟨ ∧-cong refl i≈j ⟩
-                          i ∧ j  ∎
-      ; trans         = λ {i} {j} {k} i≈i∧j j≈j∧k → begin
-                          i            ≈⟨ i≈i∧j ⟩
-                          i ∧ j        ≈⟨ ∧-cong refl j≈j∧k ⟩
-                          i ∧ (j ∧ k)  ≈⟨ sym (∧-assoc _ _ _) ⟩
-                          (i ∧ j) ∧ k  ≈⟨ ∧-cong (sym i≈i∧j) refl ⟩
-                          i ∧ k        ∎
+∨-isSemilattice : IsSemilattice _≈_ _∨_
+∨-isSemilattice = record
+  { isBand = record
+    { isSemigroup = record
+      { isMagma = record
+        { isEquivalence = isEquivalence
+        ; ∙-cong        = ∨-cong
+        }
+      ; assoc         = ∨-assoc
       }
-    ; antisym = λ {x} {y} x≈x∧y y≈y∧x → begin
-                  x      ≈⟨ x≈x∧y ⟩
-                  x ∧ y  ≈⟨ ∧-comm _ _ ⟩
-                  y ∧ x  ≈⟨ sym y≈y∧x ⟩
-                  y      ∎
+    ; idem = ∨-idempotent
     }
+  ; comm   = ∨-comm
   }
 
+∨-semilattice : Semilattice l₁ l₂
+∨-semilattice = record { isSemilattice = ∨-isSemilattice }
+
+open SL ∧-semilattice public using (poset)
 open Poset poset using (_≤_; isPartialOrder)
 
+------------------------------------------------------------------------
+-- The dual construction is also a lattice.
+
+∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
+∧-∨-isLattice = record
+  { isEquivalence = isEquivalence
+  ; ∨-comm        = ∧-comm
+  ; ∨-assoc       = ∧-assoc
+  ; ∨-cong        = ∧-cong
+  ; ∧-comm        = ∨-comm
+  ; ∧-assoc       = ∨-assoc
+  ; ∧-cong        = ∨-cong
+  ; absorptive    = swap absorptive
+  }
+
+∧-∨-lattice : Lattice _ _
+∧-∨-lattice = record { isLattice = ∧-∨-isLattice }
+
 ------------------------------------------------------------------------
 -- Every algebraic lattice can be turned into an order-theoretic one.
 
 isOrderTheoreticLattice : R.IsLattice _≈_ _≤_ _∨_ _∧_
 isOrderTheoreticLattice = record
   { isPartialOrder = isPartialOrder
-  ; supremum       = λ x y →
-                       sym (∧-absorbs-∨ x y) ,
-                       (begin
-                         y            ≈⟨ sym (∧-absorbs-∨ y x) ⟩
-                         y ∧ (y ∨ x)  ≈⟨ ∧-cong refl (∨-comm y x) ⟩
-                         y ∧ (x ∨ y)  ∎) ,
-                       (λ z x≤z y≤z → sound (begin
-                         (x ∨ y) ∨ z  ≈⟨ ∨-assoc x y z ⟩
-                         x ∨ (y ∨ z)  ≈⟨ ∨-cong refl (complete y≤z) ⟩
-                         x ∨ z        ≈⟨ complete x≤z  ⟩
-                         z            ∎))
-  ; infimum        = λ x y →
-                       (begin
-                         x ∧ y        ≈⟨ ∧-cong (sym (∧-idem x)) refl ⟩
-                         (x ∧ x) ∧ y  ≈⟨ ∧-assoc x x y  ⟩
-                         x ∧ (x ∧ y)  ≈⟨ ∧-comm x (x ∧ y) ⟩
-                         (x ∧ y) ∧ x  ∎) ,
-                       (begin
-                         x ∧ y        ≈⟨ ∧-cong refl (sym (∧-idem y)) ⟩
-                         x ∧ (y ∧ y)  ≈⟨ sym (∧-assoc x y y) ⟩
-                         (x ∧ y) ∧ y  ∎) ,
-                       (λ z z≈z∧x z≈z∧y → begin
-                         z            ≈⟨ z≈z∧y ⟩
-                         z ∧ y        ≈⟨ ∧-cong z≈z∧x refl ⟩
-                         (z ∧ x) ∧ y  ≈⟨ ∧-assoc z x y ⟩
-                         z ∧ (x ∧ y)  ∎)
+  ; supremum       = supremum
+  ; infimum        = infimum
   }
   where
+  ∧-meetSemilattice = SL.orderTheoreticMeetSemilattice ∧-semilattice
+  ∨-joinSemilattice = SL.orderTheoreticJoinSemilattice ∨-semilattice
+  open R.MeetSemilattice ∧-meetSemilattice using (infimum)
+  open R.JoinSemilattice ∨-joinSemilattice using ()
+    renaming (supremum to supremum′; _≤_ to _≤′_)
 
   -- An alternative but equivalent interpretation of the order _≤_.
 
-  complete : ∀ {x y} → x ≤ y → x ∨ y ≈ y
-  complete {x} {y} x≈x∧y = begin
-    x ∨ y        ≈⟨ ∨-cong x≈x∧y refl ⟩
-    (x ∧ y) ∨ y  ≈⟨ ∨-cong (∧-comm x y) refl ⟩
-    (y ∧ x) ∨ y  ≈⟨ ∨-comm (y ∧ x) y ⟩
+  sound : ∀ {x y} → x ≤′ y → x ≤ y
+  sound {x} {y} y≈y∨x = sym $ begin
+    x ∧ y        ≈⟨ ∧-cong refl y≈y∨x ⟩
+    x ∧ (y ∨ x)  ≈⟨ ∧-cong refl (∨-comm y x) ⟩
+    x ∧ (x ∨ y)  ≈⟨ ∧-absorbs-∨ x y ⟩
+    x            ∎
+
+  complete : ∀ {x y} → x ≤ y → x ≤′ y
+  complete {x} {y} x≈x∧y = sym $ begin
+    y ∨ x        ≈⟨ ∨-cong refl x≈x∧y ⟩
+    y ∨ (x ∧ y)  ≈⟨ ∨-cong refl (∧-comm x y) ⟩
     y ∨ (y ∧ x)  ≈⟨ ∨-absorbs-∧ y x ⟩
     y            ∎
 
-  sound : ∀ {x y} → x ∨ y ≈ y → x ≤ y
-  sound {x} {y} x∨y≈y = begin
-    x            ≈⟨ sym (∧-absorbs-∨ x y) ⟩
-    x ∧ (x ∨ y)  ≈⟨ ∧-cong refl x∨y≈y ⟩
-    x ∧ y        ∎
+  supremum : R.Supremum _≤_ _∨_
+  supremum x y =
+    let x∨y≥x , x∨y≥y , greatest = supremum′ x y
+    in sound x∨y≥x , sound x∨y≥y ,
+       λ z x≤z y≤z → sound (greatest z (complete x≤z) (complete y≤z))
 
 orderTheoreticLattice : R.Lattice _ _ _
 orderTheoreticLattice = record { isLattice = isOrderTheoreticLattice }
@@ -128,60 +143,18 @@ replace-equality {_≈′_} ≈⇔≈′ = record
   ; _∧_       = _∧_
   ; _∨_       = _∨_
   ; isLattice = record
-    { ∨-isSemilattice = record
-      { isBand = record
-        { isSemigroup = record
-          { isMagma = record
-            { isEquivalence = isEq
-            ; ∙-cong        = λ x≈y u≈v → to ⟨$⟩ ∨-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
-            }
-          ; assoc   = λ x y z → to ⟨$⟩ ∨-assoc x y z
-          }
-        ; idem = λ x → to ⟨$⟩ ∨-idem x
-        }
-      ; comm = λ x y → to ⟨$⟩ ∨-comm x y
-      }
-    ; ∧-isSemilattice = record
-      { isBand = record
-        { isSemigroup = record
-          { isMagma = record
-            { isEquivalence = isEq
-            ; ∙-cong        = λ x≈y u≈v → to ⟨$⟩ ∧-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
-            }
-          ; assoc   = λ x y z → to ⟨$⟩ ∧-assoc x y z
-          }
-        ; idem = λ x → to ⟨$⟩ ∧-idem x
-        }
-      ; comm = λ x y → to ⟨$⟩ ∧-comm x y
+    { isEquivalence = record
+      { refl  = to ⟨$⟩ refl
+      ; sym   = λ x≈y → to ⟨$⟩ sym (from ⟨$⟩ x≈y)
+      ; trans = λ x≈y y≈z → to ⟨$⟩ trans (from ⟨$⟩ x≈y) (from ⟨$⟩ y≈z)
       }
-    ; absorptive      = (λ x y → to ⟨$⟩ ∨-absorbs-∧ x y)
-                      , (λ x y → to ⟨$⟩ ∧-absorbs-∨ x y)
-    }
-  }
-  where
-  open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
-
-  isEq = record
-    { refl  = to ⟨$⟩ refl
-    ; sym   = λ x≈y → to ⟨$⟩ sym (from ⟨$⟩ x≈y)
-    ; trans = λ x≈y y≈z → to ⟨$⟩ trans (from ⟨$⟩ x≈y) (from ⟨$⟩ y≈z)
+    ; ∨-comm     = λ x y → to ⟨$⟩ ∨-comm x y
+    ; ∨-assoc    = λ x y z → to ⟨$⟩ ∨-assoc x y z
+    ; ∨-cong     = λ x≈y u≈v → to ⟨$⟩ ∨-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
+    ; ∧-comm     = λ x y → to ⟨$⟩ ∧-comm x y
+    ; ∧-assoc    = λ x y z → to ⟨$⟩ ∧-assoc x y z
+    ; ∧-cong     = λ x≈y u≈v → to ⟨$⟩ ∧-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
+    ; absorptive = (λ x y → to ⟨$⟩ ∨-absorbs-∧ x y)
+                 , (λ x y → to ⟨$⟩ ∧-absorbs-∨ x y)
     }
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 0.18
-
-∨-idempotent = ∨-idem
-{-# WARNING_ON_USAGE ∨-idempotent
-"Warning: ∨-idempotent was deprecated in v0.14.
-Instead please use `∨-idem` from the `Lattice` record."
-#-}
-∧-idempotent = ∧-idem
-{-# WARNING_ON_USAGE ∧-idempotent
-"Warning: ∧-idempotent was deprecated in v0.14.
-Instead please use `∧-idem` from the `Lattice` record."
-#-}
+  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
diff --git a/src/Algebra/Properties/Semilattice.agda b/src/Algebra/Properties/Semilattice.agda
new file mode 100644
index 0000000000..385daea637
--- /dev/null
+++ b/src/Algebra/Properties/Semilattice.agda
@@ -0,0 +1,86 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some derivable properties
+------------------------------------------------------------------------
+
+open import Algebra
+
+module Algebra.Properties.Semilattice {l₁ l₂} (L : Semilattice l₁ l₂) where
+
+open Semilattice L
+open import Algebra.Structures
+open import Relation.Binary
+import Relation.Binary.Lattice as R
+import Relation.Binary.Properties.Poset as R
+import Relation.Binary.EqReasoning as EqR; open EqR setoid
+open import Function
+open import Data.Product
+
+-- Every semilattice can be turned into a poset.
+
+poset : Poset _ _ _
+poset = record
+  { Carrier        = Carrier
+  ; _≈_            = _≈_
+  ; _≤_            = λ x y → x ≈ x ∧ y
+  ; isPartialOrder = record
+    { isPreorder = record
+      { isEquivalence = isEquivalence
+      ; reflexive     = λ {i} {j} i≈j → begin
+                          i      ≈⟨ sym $ idem _ ⟩
+                          i ∧ i  ≈⟨ ∧-cong refl i≈j ⟩
+                          i ∧ j  ∎
+      ; trans         = λ {i} {j} {k} i≈i∧j j≈j∧k → begin
+                          i            ≈⟨ i≈i∧j ⟩
+                          i ∧ j        ≈⟨ ∧-cong refl j≈j∧k ⟩
+                          i ∧ (j ∧ k)  ≈⟨ sym (assoc _ _ _) ⟩
+                          (i ∧ j) ∧ k  ≈⟨ ∧-cong (sym i≈i∧j) refl ⟩
+                          i ∧ k        ∎
+      }
+    ; antisym = λ {x} {y} x≈x∧y y≈y∧x → begin
+                  x      ≈⟨ x≈x∧y ⟩
+                  x ∧ y  ≈⟨ comm _ _ ⟩
+                  y ∧ x  ≈⟨ sym y≈y∧x ⟩
+                  y      ∎
+    }
+  }
+
+open Poset poset using (_≤_; isPartialOrder)
+
+-- Every algebraic semilattice can be turned into an order-theoretic one.
+
+isOrderTheoreticMeetSemilattice : R.IsMeetSemilattice _≈_ _≤_ _∧_
+isOrderTheoreticMeetSemilattice = record
+  { isPartialOrder = isPartialOrder
+  ; infimum        = λ x y →
+                       (begin
+                         x ∧ y        ≈⟨ ∧-cong (sym (idem x)) refl ⟩
+                         (x ∧ x) ∧ y  ≈⟨ assoc x x y  ⟩
+                         x ∧ (x ∧ y)  ≈⟨ comm x (x ∧ y) ⟩
+                         (x ∧ y) ∧ x  ∎) ,
+                       (begin
+                         x ∧ y        ≈⟨ ∧-cong refl (sym (idem y)) ⟩
+                         x ∧ (y ∧ y)  ≈⟨ sym (assoc x y y) ⟩
+                         (x ∧ y) ∧ y  ∎) ,
+                       λ z z≈z∧x z≈z∧y → begin
+                         z            ≈⟨ z≈z∧y ⟩
+                         z ∧ y        ≈⟨ ∧-cong z≈z∧x refl ⟩
+                         (z ∧ x) ∧ y  ≈⟨ assoc z x y ⟩
+                         z ∧ (x ∧ y)  ∎
+  }
+
+orderTheoreticMeetSemilattice : R.MeetSemilattice _ _ _
+orderTheoreticMeetSemilattice = record
+  { isMeetSemilattice = isOrderTheoreticMeetSemilattice }
+
+isOrderTheoreticJoinSemilattice : R.IsJoinSemilattice _≈_ (flip _≤_) _∧_
+isOrderTheoreticJoinSemilattice = record
+  { isPartialOrder = R.invIsPartialOrder poset
+  ; supremum       = R.IsMeetSemilattice.infimum
+                       isOrderTheoreticMeetSemilattice
+  }
+
+orderTheoreticJoinSemilattice : R.JoinSemilattice _ _ _
+orderTheoreticJoinSemilattice = record
+  { isJoinSemilattice = isOrderTheoreticJoinSemilattice }
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 29bf247b08..73ef316088 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -48,7 +48,7 @@ record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where
     isBand : IsBand ∧
     comm   : Commutative ∧
 
-  open IsBand isBand public
+  open IsBand isBand public renaming (∙-cong to ∧-cong)
 
 ------------------------------------------------------------------------
 -- Monoids
@@ -426,9 +426,21 @@ record IsCommutativeRing
 
 record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
   field
-    ∨-isSemilattice : IsSemilattice ∨
-    ∧-isSemilattice : IsSemilattice ∧
-    absorptive      : Absorptive ∨ ∧
+    isEquivalence : IsEquivalence _≈_
+    ∨-comm        : Commutative ∨
+    ∨-assoc       : Associative ∨
+    ∨-cong        : Congruent₂ ∨
+    ∧-comm        : Commutative ∧
+    ∧-assoc       : Associative ∧
+    ∧-cong        : Congruent₂ ∧
+    absorptive    : Absorptive ∨ ∧
+
+  -- Note that this record is not defined in terms of IsSemilattice
+  -- because the idempotence laws of ∨ and ∧ can be derived from the
+  -- absorption laws, which makes the corresponding "idem" fields
+  -- redundant.  The derived idempotence laws are stated and proved in
+  -- Algebra.Properties.Lattice along with the fact that every lattice
+  -- consists of two semilattices.
 
   ∨-absorbs-∧ : ∨ Absorbs ∧
   ∨-absorbs-∧ = proj₁ absorptive
@@ -436,28 +448,7 @@ record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
   ∧-absorbs-∨ : ∧ Absorbs ∨
   ∧-absorbs-∨ = proj₂ absorptive
 
-  open IsSemilattice ∨-isSemilattice public
-    renaming
-    ( ∙-cong      to ∨-cong
-    ; assoc       to ∨-assoc
-    ; comm        to ∨-comm
-    ; idem        to ∨-idem
-    ; isMagma     to ∨-isMagma
-    ; isSemigroup to ∨-isSemigroup
-    ; isBand      to ∨-isBand
-    )
-
-  open IsSemilattice ∧-isSemilattice public
-    renaming
-    ( ∙-cong      to ∧-cong
-    ; assoc       to ∧-assoc
-    ; comm        to ∧-comm
-    ; idem        to ∧-idem
-    ; isMagma     to ∧-isMagma
-    ; isSemigroup to ∧-isSemigroup
-    ; isBand      to ∧-isBand
-    )
-    hiding (refl; reflexive; sym; trans; isEquivalence; setoid)
+  open IsEquivalence isEquivalence public
 
 record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
   field
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 1ad0028244..7a4b9a226e 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -352,9 +352,14 @@ false ≟ true  = no λ()
 
 ∨-∧-isLattice : IsLattice _∨_ _∧_
 ∨-∧-isLattice = record
-  { ∨-isSemilattice = ∨-isSemilattice
-  ; ∧-isSemilattice = ∧-isSemilattice
-  ; absorptive      = ∨-∧-absorptive
+  { isEquivalence = isEquivalence
+  ; ∨-comm        = ∨-comm
+  ; ∨-assoc       = ∨-assoc
+  ; ∨-cong        = cong₂ _∨_
+  ; ∧-comm        = ∧-comm
+  ; ∧-assoc       = ∧-assoc
+  ; ∧-cong        = cong₂ _∧_
+  ; absorptive    = ∨-∧-absorptive
   }
 
 ∨-∧-lattice : Lattice 0ℓ 0ℓ
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index acb3718efb..f878330aa0 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -490,9 +490,14 @@ module _ (n : ℕ) where
 
   ∪-∩-isLattice : IsLattice _∪_ _∩_
   ∪-∩-isLattice = record
-    { ∨-isSemilattice = ∪-isSemilattice
-    ; ∧-isSemilattice = ∩-isSemilattice n
-    ; absorptive      = ∪-abs-∩ , ∩-abs-∪
+    { isEquivalence = isEquivalence
+    ; ∨-comm        = ∪-comm
+    ; ∨-assoc       = ∪-assoc
+    ; ∨-cong        = cong₂ _∪_
+    ; ∧-comm        = ∩-comm
+    ; ∧-assoc       = ∩-assoc
+    ; ∧-cong        = cong₂ _∩_
+    ; absorptive    = ∪-abs-∩ , ∩-abs-∪
     }
 
   ∪-∩-lattice : Lattice _ _
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 23c747e842..1691402223 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -1027,9 +1027,14 @@ i^j≡1⇒j≡0∨i≡1 i (suc j) eq = inj₂ (i*j≡1⇒i≡1 i (i ^ j) eq)
 
 ⊓-⊔-isLattice : IsLattice _⊓_ _⊔_
 ⊓-⊔-isLattice = record
-  { ∨-isSemilattice = ⊓-isSemilattice
-  ; ∧-isSemilattice = ⊔-isSemilattice
-  ; absorptive      = ⊓-⊔-absorptive
+  { isEquivalence = isEquivalence
+  ; ∨-comm        = ⊓-comm
+  ; ∨-assoc       = ⊓-assoc
+  ; ∨-cong        = cong₂ _⊓_
+  ; ∧-comm        = ⊔-comm
+  ; ∧-assoc       = ⊔-assoc
+  ; ∧-cong        = cong₂ _⊔_
+  ; absorptive    = ⊓-⊔-absorptive
   }
 
 ⊓-⊔-lattice : Lattice 0ℓ 0ℓ
diff --git a/src/Relation/Binary/Properties/JoinSemilattice.agda b/src/Relation/Binary/Properties/JoinSemilattice.agda
index f6e4d67b91..618ba0a056 100644
--- a/src/Relation/Binary/Properties/JoinSemilattice.agda
+++ b/src/Relation/Binary/Properties/JoinSemilattice.agda
@@ -11,6 +11,8 @@ module Relation.Binary.Properties.JoinSemilattice
 
 open JoinSemilattice J
 
+import Algebra as Alg
+import Algebra.Structures as Alg
 import Algebra.FunctionProperties as P; open P _≈_
 open import Data.Product
 open import Function using (_∘_; flip)
@@ -64,6 +66,26 @@ x≤y⇒x∨y≈y {x} {y} x≤y = antisym
   (y≤x∨y _ _)
   where open PoR poset
 
+-- Every order-theoretic semilattice can be turned into an algebraic one.
+
+isAlgSemilattice : Alg.IsSemilattice _≈_ _∨_
+isAlgSemilattice = record
+  { isBand = record
+    { isSemigroup = record
+      { isMagma   = record
+        { isEquivalence = isEquivalence
+        ; ∙-cong        = ∨-cong
+        }
+      ; assoc  = ∨-assoc
+      }
+    ; idem     = ∨-idempotent
+    }
+  ; comm       = ∨-comm
+  }
+
+algSemilattice : Alg.Semilattice c ℓ₁
+algSemilattice = record { isSemilattice = isAlgSemilattice }
+
 -- The dual construction is a meet semilattice.
 
 dualIsMeetSemilattice : IsMeetSemilattice _≈_ (flip _≤_) _∨_
diff --git a/src/Relation/Binary/Properties/Lattice.agda b/src/Relation/Binary/Properties/Lattice.agda
index 426dbec9c8..8ceebc786c 100644
--- a/src/Relation/Binary/Properties/Lattice.agda
+++ b/src/Relation/Binary/Properties/Lattice.agda
@@ -111,36 +111,15 @@ collapse₂ {x} {y} ∨≤∧ = antisym
 
 isAlgLattice : Alg.IsLattice _≈_ _∨_ _∧_
 isAlgLattice = record
-  { ∨-isSemilattice = record
-    { isBand = record
-      { isSemigroup = record
-        { isMagma = record
-          { isEquivalence = isEquivalence
-          ; ∙-cong        = J.∨-cong
-          }
-        ; assoc = J.∨-assoc
-        }
-      ; idem = J.∨-idempotent
-      }
-    ; comm = J.∨-comm
-    }
-  ; ∧-isSemilattice = record
-    { isBand = record
-      { isSemigroup = record
-        { isMagma = record
-          { isEquivalence = isEquivalence
-          ; ∙-cong        = M.∧-cong
-          }
-        ; assoc = M.∧-assoc
-        }
-      ; idem = M.∧-idempotent
-      }
-    ; comm = M.∧-comm
-    }
+  { isEquivalence = isEquivalence
+  ; ∨-comm        = J.∨-comm
+  ; ∨-assoc       = J.∨-assoc
+  ; ∨-cong        = J.∨-cong
+  ; ∧-comm        = M.∧-comm
+  ; ∧-assoc       = M.∧-assoc
+  ; ∧-cong        = M.∧-cong
   ; absorptive    = absorptive
   }
 
 algLattice : Alg.Lattice c ℓ₁
-algLattice = record
-  { isLattice = isAlgLattice
-  }
+algLattice = record { isLattice = isAlgLattice }
diff --git a/src/Relation/Binary/Properties/MeetSemilattice.agda b/src/Relation/Binary/Properties/MeetSemilattice.agda
index 5d85151e7c..dd07d93b38 100644
--- a/src/Relation/Binary/Properties/MeetSemilattice.agda
+++ b/src/Relation/Binary/Properties/MeetSemilattice.agda
@@ -32,11 +32,13 @@ dualJoinSemilattice = record
   ; isJoinSemilattice = dualIsJoinSemilattice
   }
 
-open J dualJoinSemilattice public using () renaming
-  ( ∨-monotonic  to ∧-monotonic
-  ; ∨-cong       to ∧-cong
-  ; ∨-comm       to ∧-comm
-  ; ∨-assoc      to ∧-assoc
-  ; ∨-idempotent to ∧-idempotent
-  ; x≤y⇒x∨y≈y    to y≤x⇒x∧y≈y
-  )
+open J dualJoinSemilattice public
+  using (isAlgSemilattice; algSemilattice)
+  renaming
+    ( ∨-monotonic  to ∧-monotonic
+    ; ∨-cong       to ∧-cong
+    ; ∨-comm       to ∧-comm
+    ; ∨-assoc      to ∧-assoc
+    ; ∨-idempotent to ∧-idempotent
+    ; x≤y⇒x∨y≈y    to y≤x⇒x∧y≈y
+    )