---
layout: default
file: "src/Examples/Classical/CommutativeSemigroup.lagda.md"
title: "Examples.Classical.CommutativeSemigroup module"
date: "2026-05-24"
author: "the agda-algebras development team"
---

### 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`][Examples.Classical.Semigroup]: the same carrier and
operation, now additionally witnessing commutativity via stdlib's `+-comm`.

<!--
```agda
{-# 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`.

```agda
ℕ-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
```