From 8b237c5b689b427421b8f8177752a21d378c99d2 Mon Sep 17 00:00:00 2001
From: matthewdaggitt <matthewdaggitt@gmail.com>
Date: Fri, 24 Nov 2023 12:32:43 +0800
Subject: [PATCH 1/2] Fix names in IsSemilattice

---
 CHANGELOG.md                                    |  3 +++
 src/Algebra/Lattice/Structures.agda             | 17 ++++++-----------
 .../Binary/Construct/NaturalOrder/Left.agda     |  6 +++---
 src/Relation/Binary/PropositionalEquality.agda  |  1 -
 4 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 51966c2176..e8366aa94d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -206,6 +206,9 @@ Non-backwards compatible changes
 
 * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice`
   which can be used to indicate meet/join-ness of the original structures.
+  
+* The field names in `IsSemilattice` have been renamed from `∧-cong` to `∙-cong`
+  to indicate the undirected nature of it.
 
 * Finally, the following auxiliary files have been moved:
   ```agda
diff --git a/src/Algebra/Lattice/Structures.agda b/src/Algebra/Lattice/Structures.agda
index fc40c0c300..116ed85271 100644
--- a/src/Algebra/Lattice/Structures.agda
+++ b/src/Algebra/Lattice/Structures.agda
@@ -37,20 +37,15 @@ record IsSemilattice (∙ : Op₂ A) : Set (a ⊔ ℓ) where
     comm   : Commutative ∙
 
   open IsBand isBand public
-    renaming
-    ( ∙-cong  to ∧-cong
-    ; ∙-congˡ to ∧-congˡ
-    ; ∙-congʳ to ∧-congʳ
-    )
 
 -- Used to bring names appropriate for a meet semilattice into scope.
 IsMeetSemilattice = IsSemilattice
 module IsMeetSemilattice {∧} (L : IsMeetSemilattice ∧) where
   open IsSemilattice L public
     renaming
-    ( ∧-cong  to ∧-cong
-    ; ∧-congˡ to ∧-congˡ
-    ; ∧-congʳ to ∧-congʳ
+    ( ∙-cong  to ∧-cong
+    ; ∙-congˡ to ∧-congˡ
+    ; ∙-congʳ to ∧-congʳ
     )
 
 -- Used to bring names appropriate for a join semilattice into scope.
@@ -58,9 +53,9 @@ IsJoinSemilattice = IsSemilattice
 module IsJoinSemilattice {∨} (L : IsJoinSemilattice ∨) where
   open IsSemilattice L public
     renaming
-    ( ∧-cong  to ∨-cong
-    ; ∧-congˡ to ∨-congˡ
-    ; ∧-congʳ to ∨-congʳ
+    ( ∙-cong  to ∨-cong
+    ; ∙-congˡ to ∨-congˡ
+    ; ∙-congʳ to ∨-congʳ
     )
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
index 22a5031d27..c4846142ec 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
@@ -99,21 +99,21 @@ module _ (semi : IsSemilattice _∙_) where
 
   x∙y≤x : ∀ x y → (x ∙ y) ≤ x
   x∙y≤x x y = begin
-    x ∙ y       ≈⟨ ∧-cong (sym (idem x)) S.refl ⟩
+    x ∙ y       ≈⟨ ∙-cong (sym (idem x)) S.refl ⟩
     (x ∙ x) ∙ y ≈⟨ assoc x x y ⟩
     x ∙ (x ∙ y) ≈⟨ comm x (x ∙ y) ⟩
     (x ∙ y) ∙ x ∎
 
   x∙y≤y : ∀ x y → (x ∙ y) ≤ y
   x∙y≤y x y = begin
-    x ∙ y        ≈⟨ ∧-cong S.refl (sym (idem y)) ⟩
+    x ∙ y        ≈⟨ ∙-cong S.refl (sym (idem y)) ⟩
     x ∙ (y ∙ y)  ≈⟨ sym (assoc x y y) ⟩
     (x ∙ y) ∙ y  ∎
 
   ∙-presʳ-≤ : ∀ {x y} z → z ≤ x → z ≤ y → z ≤ (x ∙ y)
   ∙-presʳ-≤ {x} {y} z z≤x z≤y = begin
     z            ≈⟨ z≤y ⟩
-    z ∙ y        ≈⟨ ∧-cong z≤x S.refl ⟩
+    z ∙ y        ≈⟨ ∙-cong z≤x S.refl ⟩
     (z ∙ x) ∙ y  ≈⟨ assoc z x y ⟩
     z ∙ (x ∙ y)  ∎
 
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 7ba3825e31..6c2eb19bed 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -135,4 +135,3 @@ isPropositional = Irrelevant
 Please use Relation.Nullary.Irrelevant instead. "
 #-}
 
-

From 08ac8088172a4e402733ff21e8fb322e53c348ef Mon Sep 17 00:00:00 2001
From: matthewdaggitt <matthewdaggitt@gmail.com>
Date: Sat, 25 Nov 2023 12:52:55 +0800
Subject: [PATCH 2/2] Add reference to changes to Semilattice to CHANGELOG

---
 CHANGELOG.md | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e8366aa94d..fe294d57fc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -205,10 +205,9 @@ Non-backwards compatible changes
 * Added new `IsBoundedSemilattice`/`BoundedSemilattice` records.
 
 * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice`
-  which can be used to indicate meet/join-ness of the original structures.
-  
-* The field names in `IsSemilattice` have been renamed from `∧-cong` to `∙-cong`
-  to indicate the undirected nature of it.
+  which can be used to indicate meet/join-ness of the original structures, and
+  the field names in `IsSemilattice` and `Semilattice` have been renamed from 
+  `∧-cong` to `∙-cong`to indicate their undirected nature.
 
 * Finally, the following auxiliary files have been moved:
   ```agda