Examples.Classical.CommutativeSemigroup

Worked example: (ℕ, +) as a commutative semigroup

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

The natural numbers under addition, one theory up from Examples.Classical.Semigroup: the same carrier and operation, now additionally witnessing commutativity via stdlib's +-comm.

{-# OPTIONS --without-K --exact-split --safe #-}
module Examples.Classical.CommutativeSemigroup where

open import Data.Nat                               using ( ℕ ; _+_ )
open import Data.Nat.Properties                    using ( +-assoc ; +-comm )
open import Relation.Binary.PropositionalEquality  using ( _≡_ ; refl )

open import Classical.Small.Structures.CommutativeSemigroup
  using ( CommutativeSemigroup ; eqsToCommutativeSemigroup )

import Classical.Structures.CommutativeSemigroup as Polymorphic

ℕ-commutativeSemigroup hands eqsToCommutativeSemigroup the carrier, the operation, and the two laws +-assoc and +-comm. The acceptance check ∙-is-+-cs records that the accessor's curried _∙_ interprets to _+_ on the nose, discharged by refl.

ℕ-commutativeSemigroup : CommutativeSemigroup
ℕ-commutativeSemigroup = eqsToCommutativeSemigroup ℕ _+_ +-assoc +-comm

open Polymorphic.CommutativeSemigroup-Op ℕ-commutativeSemigroup using ( _∙_ )

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