add: Identity and Zero elements are Central

Author: jamesmckinna

CHANGELOG.md

@@ -118,12 +118,16 @@ Additions to existing modules
   ```agda
   binomial-expansion : Associative _∙_ → _◦_ DistributesOver _∙_ →
     ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  identity⇒central   : Identity e _∙_ → Central _∙_ e
+  zero⇒central       : Zero e _∙_ → Central _∙_ e
   ```
 
 * In `Algebra.Consequences.Setoid`:
   ```agda
   binomial-expansion : Congruent₂ _∙_  → Associative _∙_ → _◦_ DistributesOver _∙_ →
     ∀ w x y z → ((w ∙ x) ◦ (y ∙ z)) ≈ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
+  identity⇒central   : Identity e _∙_ → Central _∙_ e
+  zero⇒central       : Zero e _∙_ → Central _∙_ e
   ```
 
 * In `Algebra.Definitions`:

src/Algebra/Consequences/Setoid.agda

@@ -184,6 +184,15 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
       x ∙ z ≈⟨ comm x z ⟩
       z ∙ x ∎
 
+module _ {_∙_ : Op₂ A} {e : A} where
+
+  identity⇒central : Identity e _∙_ → Central _∙_ e
+  identity⇒central (identityˡ , identityʳ) x = trans (identityˡ x) (sym (identityʳ x))
+
+  zero⇒central : Zero e _∙_ → Central _∙_ e
+  zero⇒central (zeroˡ , zeroʳ) x = trans (zeroˡ x) (sym (zeroʳ x))
+
+
 ------------------------------------------------------------------------
 -- Group-like structures