Fixes #2166 by fixing names in IsSemilattice (#2211)

* Fix names in IsSemilattice

* Add reference to changes to Semilattice to CHANGELOG

CHANGELOG.md

@@ -205,7 +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.
+  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

src/Algebra/Lattice/Structures.agda

@@ -37,30 +37,25 @@ 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.
 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ʳ
     )
 
 ------------------------------------------------------------------------

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)  ∎