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