Examples.Classical.CommutativeMonoid

Worked example: (ℕ, +, 0) as a commutative monoid

This is the Examples.Classical.CommutativeMonoid module of the Agda Universal Algebra Library.

The natural numbers under addition and zero form the canonical commutative monoid; the contrast case is the deliberately non-commutative Examples.Classical.Monoid on lists. The construction is one line because eqsToCommutativeMonoid asks for exactly the four stdlib lemmas named below.

{-# OPTIONS --without-K --exact-split --safe #-}

module Examples.Classical.CommutativeMonoid where

-- Imports from the Agda Standard Library -------------------------------------
open import Data.Nat                               using  ( ℕ ; _+_ ; zero )
open import Data.Nat.Properties                    using  ( +-assoc ; +-identityˡ
                                                          ; +-identityʳ ; +-comm )
open import Relation.Binary.PropositionalEquality  using  ( _≡_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Small.Structures.CommutativeMonoid
  using  ( CommutativeMonoid ; eqsToCommutativeMonoid )

import Classical.Structures.CommutativeMonoid as Polymorphic

We construct (ℕ, +, 0) from stdlib's +-assoc, +-identityˡ, +-identityʳ, +-comm.

ℕ-commutativeMonoid : CommutativeMonoid
ℕ-commutativeMonoid =
  eqsToCommutativeMonoid ℕ _+_ zero +-assoc +-identityˡ +-identityʳ +-comm

open Polymorphic.CommutativeMonoid-Op ℕ-commutativeMonoid using ( _∙_ ; ε )

∙-is-+-cmn : ∀ (a b : ℕ) → a ∙ b ≡ a + b
∙-is-+-cmn a b = refl

ε-is-0-cmn : ε ≡ zero
ε-is-0-cmn = refl