update

Author: jmougeot

CHANGELOG.md

@@ -113,6 +113,8 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Properties.Monoid` adding consequences for identity for monoids
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
@@ -123,9 +125,11 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
-* `Algebra.Properties.Semigroup` adding consequences for associatvity for semigroups
+Additions to existing modules
 -----------------------------
 
+* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →

src/Algebra/Properties/Monoid/Reasoning.agda renamed to src/Algebra/Properties/Monoid.agda

@@ -8,8 +8,9 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Monoid)
+open import Function using (_∘_)
 
-module Algebra.Properties.Monoid.Reasoning {o ℓ} (M : Monoid o ℓ) where
+module Algebra.Properties.Monoid {o ℓ} (M : Monoid o ℓ) where
 
 open Monoid M
   using (Carrier; _∙_; _≈_; setoid; isMagma; semigroup; ε; sym; identityˡ
@@ -22,33 +23,32 @@ private
     variable
         a b c d : Carrier
 
-module _ where
-    id-unique : ∀ a → (∀ b → b ∙ a ≈ b) → a ≈ ε
-    id-unique a b∙a≈b = trans (sym (identityˡ a)) (b∙a≈b ε)
+id-unique : ∀ a → (∀ b → b ∙ a ≈ b) → a ≈ ε
+id-unique a b∙a≈b = trans (sym (identityˡ a)) (b∙a≈b ε)
 
-    id-comm : ∀ a → a ∙ ε ≈ ε ∙ a
-    id-comm a = trans (identityʳ a) (sym (identityˡ a))
+id-comm : ∀ a → a ∙ ε ≈ ε ∙ a
+id-comm a = trans (identityʳ a) (sym (identityˡ a))
 
-    id-comm-sym : ∀ a → ε ∙ a ≈ a ∙ ε
-    id-comm-sym a = sym (id-comm a)
+id-comm-sym : ∀ a → ε ∙ a ≈ a ∙ ε
+id-comm-sym = sym ∘ id-comm
 
-module _ {a b : Carrier} (a≈ε : a ≈ ε) where
+module _ (a≈ε : a ≈ ε) where
     elimʳ : ∀ b → b ∙ a ≈ b
-    elimʳ b = trans (∙-congˡ a≈ε) (identityʳ b)
+    elimʳ = trans (∙-congˡ a≈ε) ∘ identityʳ
 
     elimˡ : ∀ b → a ∙ b ≈ b
-    elimˡ b = trans (∙-congʳ a≈ε) (identityˡ b)
+    elimˡ = trans (∙-congʳ a≈ε) ∘ identityˡ
 
     introʳ : ∀ b → b ≈ b ∙ a
-    introʳ b = sym (elimʳ b)
+    introʳ = sym ∘ elimʳ
 
     introˡ : ∀ b → b ≈ a ∙ b
-    introˡ b = sym (elimˡ b)
+    introˡ = sym ∘ elimˡ
 
     introcenter : ∀ c → b ∙ c ≈ b ∙ (a ∙ c)
     introcenter c = trans (∙-congˡ (sym (identityˡ c))) (∙-congˡ (∙-congʳ (sym a≈ε)))
 
-module _ {a c : Carrier} (inv : a ∙ c ≈ ε) where
+module _ (inv : a ∙ c ≈ ε) where
 
   cancelʳ : ∀ b → (b ∙ a) ∙ c ≈ b
   cancelʳ b = trans (assoc b a c) (trans (∙-congˡ inv) (identityʳ b))
@@ -57,14 +57,14 @@ module _ {a c : Carrier} (inv : a ∙ c ≈ ε) where
   cancelˡ b = trans (sym (assoc a c b)) (trans (∙-congʳ inv) (identityˡ b))
 
   insertˡ : ∀ b → b ≈ a ∙ (c ∙ b)
-  insertˡ b = sym (cancelˡ b)
+  insertˡ = sym ∘ cancelˡ
 
   insertʳ : ∀ b → b ≈ (b ∙ a) ∙ c
-  insertʳ b = sym (cancelʳ b)
+  insertʳ = sym ∘ cancelʳ
 
   cancelInner : ∀ b d → (b ∙ a) ∙ (c ∙ d) ≈ b ∙ d
   cancelInner b d = trans (uv≈w⇒xu∙vy≈x∙wy inv b d) (∙-congˡ (identityˡ d))
 
   insertInner : ∀ b d → b ∙ d ≈ (b ∙ a) ∙ (c ∙ d)
-  insertInner b d = sym (cancelInner b d)
+  insertInner = λ b d → sym (cancelInner b d)