Examples.Classical.Magma

Worked example: (ℕ, +) as a magma

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

The natural numbers under addition form the canonical first magma to exhibit. Beyond demonstrating that the M3-3 deliverable type-checks, this module is the home for all future magma-specific worked examples: alternative magmas on ℕ (under multiplication, under truncated subtraction), small finite magmas as Cayley tables, free magmas over a generating set, magmas that fail to be semigroups, and so on. Subsequent additions should land here rather than alongside the core structure file.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Examples.Classical.Magma where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Data.Nat                               using ( ℕ ; _+_ )
open import Relation.Binary.PropositionalEquality  using ( _≡_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Bundles.Magma           using ( ⟨_⟩ᵐᵃ ; ⟪_⟫ᵐᵃ )
open import Classical.Small.Structures.Magma  using ( Magma ; opsToMagma )

import Classical.Structures.Magma as Polymorphic

The magma (ℕ, +)

ℕ-magma : Magma
ℕ-magma = opsToMagma ℕ _+_

open Polymorphic.Magma-Op ℕ-magma using ( _∙_ )

Acceptance checks

∙-Op interpreted in ℕ-magma reduces definitionally to _+_: no opacity from the opsToMagma construction, no opacity from the Curry₂ wrapping in the named accessor. Discharged by refl.

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

The bundle bridge round-trips on ℕ-magma pointwise. Both directions reduce by pair a b 0F ⇉ a and pair a b 1F ⇉ b, so propositional refl discharges the obligation at the curried form (per ADR-002 v2 §6).

open Polymorphic.Magma-Op ⟪ ⟨ ℕ-magma ⟩ᵐᵃ ⟫ᵐᵃ using () renaming ( _∙_ to _·_ )

roundtrip-ℕ-ma : ∀ (a b : ℕ) → a · b ≡ a + b
roundtrip-ℕ-ma a b = refl