Classical.Signatures.Magma

The signature of magmas

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

A magma is, traditionally, a carrier equipped with a single binary operation — the most minimal of the classical algebraic structures, and the right starting point for the Classical/ tree because its equational theory is empty. This module fixes the signature of magmas as a one-symbol algebraic signature with that symbol assigned arity Fin 2.

Per ADR-002 v2 §5, every concrete classical structure X is characterized by a pair (Sig-X , Th-X) — its own signature and its own complete equational theory in that signature. For Magma the theory is empty; the signature carries the whole content.

The conventions for naming established here are normative for every subsequent structure (Semigroup in M3-4, Monoid and Group in M3-6, Lattice in M3-7, Ring in M3-8); each follows the same Op-X/<symbol>-Op/ar-X/Sig-X pattern, extending or reusing as appropriate.

• Operation symbols are introduced via a one-or-more-constructor data type Op-<Structure>, with each constructor named <symbol>-Op (hyphen-separated, capital O). Reserving the bare symbol — ∙, ε, ⁻¹, +, 0, ·, 1, ∧, ∨ — for user-facing curried sugar avoids a name clash between the syntactic operation-symbol-of-the-signature and the semantic curried operation on a fixed algebra.
• Arity functions are named ar-<Structure> and defined by direct pattern matching on operation-symbol constructors (ar-Magma ∙-Op = Fin 2). Direct pattern matching is required, not optional: the Classical.Equations builders demand definitional reduction of ArityOf 𝑆 f to a concrete Fin n at use sites, which fails for indirect definitions (table lookups, conditionals).
• Signature values are named Sig-<Structure> and assembled as a Σ-pair of the operation-symbol type and the arity function. The hyphenated long form is preferred over subscripted alternatives (𝑆ₘₐ, 𝑆_Magma) per ADR-002 v2 §7; the long form survives grep, copy/paste, and rendering across plain-text channels.

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

module Classical.Signatures.Magma where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive using ()                renaming ( Set to Type )
open import Data.Fin.Base  using ( Fin )
open import Data.Product   using ( _,_ )
open import Level          using ( 0ℓ )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures using ( Signature )

The operation-symbol type

A magma has a single binary operation symbol. The constructor is named ∙-Op following the <symbol>-Op convention; the bare ∙ is reserved for the curried user-facing accessor introduced in Classical.Structures.Magma.

data Op-Magma : Type where
  ∙-Op : Op-Magma

The arity function

∙-Op is binary, so its arity is Fin 2. Direct pattern matching on the single constructor lets ArityOf Sig-Magma ∙-Op reduce definitionally to Fin 2 — this is what makes the arity-conformance evidence refl of type ArityOf Sig-Magma ∙-Op ≡ Fin 2 typecheck in Th-Semigroup (M3-4) and every subsequent theory.

ar-Magma : Op-Magma → Type
ar-Magma ∙-Op = Fin 

The signature value

Sig-Magma : Signature 0ℓ 0ℓ
Sig-Magma = Op-Magma , ar-Magma