Skip to content

Classical.Equations

Equations of Classical Structures

This is the Classical.Equations module of the Agda Universal Algebra Library. It is the syntactic dual of the standard library's Algebra.Definitions module.

The standard library's Algebra.Definitions provides a uniform inventory of equation predicates at the evaluated level.

For example, given a carrier A, an equivalence _β‰ˆ_, and an operation, Associative _β‰ˆ_ _βˆ™_ is the type βˆ€ x y z β†’ (x βˆ™ y) βˆ™ z β‰ˆ x βˆ™ (y βˆ™ z). This is what stdlib's IsSemigroup.assoc returns and what users prove for concrete algebras.

This module is the syntactic dual; given a signature 𝑆 and operation symbols within it (with arity proofs), Associative βˆ™-Op refl returns a function from three variables to a pair of Sig-𝑆-terms β€” the LHS (β„Š x βˆ™ β„Š y) βˆ™ β„Š z and the RHS β„Š x βˆ™ (β„Š y βˆ™ β„Š z). This is what Th-X : Eq-X β†’ Term (Fin n) Γ— Term (Fin n) is built from, and is what feeds the equational-logic core (Modα΅—) for every concrete theory under Classical/Theories/.

Both views are needed; neither subsumes the other. Algebra.Definitions is what you prove a specific algebra satisfies; Classical.Equations is what you state as part of a variety's defining theory, before any algebra is in the picture. The distinction is the same as the distinction between an equation (x Β· y) Β· z = x Β· (y Β· z) as a formula (a string of symbols) versus the same equation as a proposition about a particular algebraic structure (a thing that can be proved).

The universal-algebra meta-theory operates on the formula view; the user proving things about a specific algebra operates on the proposition view. The relationship between the two is mediated by interpretation: Modα΅— Th-X 𝑨 says "for every equation (s, t) in Th-X, the formula s β‰ˆ t interpreted in 𝑨 holds for all environments."

The motivation for distinguishing the two views formally β€” beyond cleanliness β€” comes from results like Bryant's The laws of finite pointed groups (Bull. LMS 14 (1982), 119–123), which is a stark illustration of the fact that the equational theory of a structure can depend substantively on the signature it lives over, not just on the carrier and operations. A formal account of equations as syntactic objects, distinct from their evaluations in particular algebras, is what makes that distinction expressible.

See ADR-002 v2 Β§3 for more details about the design rationale.

Note for per-structure-theory authors. The arity-conformance evidence refl typechecks only when the signature's arity function reduces definitionally to Fin n on the operation symbol in question. Define arity functions by direct pattern matching on operation-symbol constructors (ar-X βˆ™-Op = Fin 2); avoid indirect definitions (table lookups, conditionals) that would leave the arity opaque to the type checker.

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

module Classical.Equations where

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Agda.Primitive renaming ( Set to Type )  using ()
open import Data.Fin.Base                            using ( Fin )
open import Data.Product                             using ( _Γ—_ ; _,_ )
open import Level                                    using ( Level ; 0β„“)
open import Relation.Binary.PropositionalEquality    using ( _≑_ ; sym ; subst )

-- Imports from agda-algebras -----------------------------------------------------
open import Classical.Operations  using ( pair )
open import Overture.Signatures   using ( Signature ; OperationSymbolsOf ; ArityOf )

private variable
  π“ž Ο‡ : Level

The equation-builder API is parameterized over a fixed signature 𝑆. Each builder takes operation symbols from 𝑆 together with evidence that the symbols' arities match the equation's shape; given that, the builder returns a function from however-many-variables-the-equation-needs to a pair of terms over the signature.

module _ {𝑆 : Signature π“ž 0β„“} {X : Type Ο‡} where
  open import Overture.Terms.Basic {𝑆 = 𝑆} using ( Term ; β„Š ; node )
  -- Apply an operation symbol of known arity to its term arguments.  Each helper
  -- takes the symbol and the arity-conformance evidence; `subst` is what bridges
  -- the abstract `ArityOf 𝑆 f` (an opaque type that depends on the abstract
  -- signature) to the concrete `Fin n` the term-building code wants to use.  At
  -- a call site with concrete signature, `ArityOf 𝑆 f` reduces to `Fin n`,
  -- the arity-conformance becomes `refl`, and `subst P refl` is definitionally
  -- the identity β€” so the helpers carry no runtime overhead at use sites.


  -- The following helpers are public in case users want to defining custom equation
  -- builders downstream; use of standard identities defined below is preferred.
  appβ‚€ : {e : OperationSymbolsOf 𝑆} β†’ ArityOf 𝑆 e ≑ Fin 0 β†’ Term X
  appβ‚€ {e} e-nul = node e (subst (Ξ» I β†’ I β†’ Term X) (sym e-nul) Ξ» ())

  app₁ : {i : OperationSymbolsOf 𝑆} β†’ ArityOf 𝑆 i ≑ Fin 1 β†’ Term X β†’ Term X
  app₁ {i} i-un s = node i (subst (Ξ» I β†’ I β†’ Term X) (sym i-un) (Ξ» _ β†’ s))

  appβ‚‚ : {f : OperationSymbolsOf 𝑆} β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ Term X β†’ Term X β†’ Term X
  appβ‚‚ {f} f-bin s t = node f (subst (Ξ» I β†’ I β†’ Term X) (sym f-bin) (pair s t))

Associative, Commutative, and Idempotent Laws

  -- f (f x y) z β‰ˆ f x (f y z)
  Associative : (f : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ X β†’ X β†’ X β†’ Term X Γ— Term X
  Associative _ f-bin x y z =
    appβ‚‚ f-bin (appβ‚‚ f-bin (β„Š x) (β„Š y)) (β„Š z)
    , appβ‚‚ f-bin (β„Š x) (appβ‚‚ f-bin (β„Š y) (β„Š z))

  -- f x y β‰ˆ f y x
  Commutative : (f : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ X β†’ X β†’ Term X Γ— Term X

  Commutative _ f-bin x y = appβ‚‚ f-bin (β„Š x) (β„Š y) , appβ‚‚ f-bin (β„Š y) (β„Š x)

  -- f x x β‰ˆ x
  Idempotent : (f : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ X β†’ Term X Γ— Term X
  Idempotent _ f-bin x = appβ‚‚ f-bin (β„Š x) (β„Š x) , β„Š x

Identity laws

These take a binary operation f together with a nullary "identity element" symbol e. The arity-conformance evidence for e is ArityOf e ≑ Fin 0, consistent with the Op (Fin 0) A representation of nullary operations in Classical.Operations.

  -- f e x β‰ˆ x
  LeftIdentity :  (f e : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ ArityOf 𝑆 e ≑ Fin 0
    β†’ X β†’ Term X Γ— Term X
  LeftIdentity _ _ f-bin e-nul x = appβ‚‚ f-bin (appβ‚€ e-nul) (β„Š x) , β„Š x

  -- f x e β‰ˆ x
  RightIdentity : (f e : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ ArityOf 𝑆 e ≑ Fin 0
    β†’ X β†’ Term X Γ— Term X
  RightIdentity _ _ f-bin e-nul x = appβ‚‚ f-bin (β„Š x) (appβ‚€ e-nul) , β„Š x

Inverse laws

These take a binary f, a nullary identity e, and a unary inverse i. The arity evidence for i is ArityOf i ≑ Fin 1.

  -- f (i x) x β‰ˆ e
  LeftInverse : (f i e : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ ArityOf 𝑆 i ≑ Fin 1 β†’ ArityOf 𝑆 e ≑ Fin 0
    β†’ X β†’ Term X Γ— Term X
  LeftInverse _ _ _ f-bin i-un e-nul x =
    appβ‚‚ f-bin (app₁ i-un (β„Š x)) (β„Š x) , appβ‚€ e-nul

  -- f x (i x) β‰ˆ e
  RightInverse : (f i e : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 f ≑ Fin 2 β†’ ArityOf 𝑆 i ≑ Fin 1 β†’ ArityOf 𝑆 e ≑ Fin 0
    β†’ X β†’ Term X Γ— Term X
  RightInverse _ _ _ f-bin i-un e-nul x =
    appβ‚‚ f-bin (β„Š x) (app₁ i-un (β„Š x)) , appβ‚€ e-nul

Distributive laws

  -- x Β· (y + z) β‰ˆ (x Β· y) + (x Β· z)
  DistributesOverΛ‘ : (Β· + : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 Β· ≑ Fin 2 β†’ ArityOf 𝑆 + ≑ Fin 2
    β†’ X β†’ X β†’ X β†’ Term X Γ— Term X
  DistributesOverΛ‘ _ _ Β·-bin +-bin x y z =
      appβ‚‚ Β·-bin (β„Š x) (appβ‚‚ +-bin (β„Š y) (β„Š z))
    , appβ‚‚ +-bin (appβ‚‚ Β·-bin (β„Š x) (β„Š y)) (appβ‚‚ Β·-bin (β„Š x) (β„Š z))

  -- (y + z) Β· x β‰ˆ (y Β· x) + (z Β· x)
  DistributesOverΚ³ : (Β· + : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 Β· ≑ Fin 2 β†’ ArityOf 𝑆 + ≑ Fin 2
    β†’ X β†’ X β†’ X β†’ Term X Γ— Term X
  DistributesOverΚ³ _ _ Β·-bin +-bin x y z =
      appβ‚‚ Β·-bin (appβ‚‚ +-bin (β„Š y) (β„Š z)) (β„Š x)
    , appβ‚‚ +-bin (appβ‚‚ Β·-bin (β„Š y) (β„Š x)) (appβ‚‚ Β·-bin (β„Š z) (β„Š x))

Absorption laws

These take two binary operations f and g; each builder expresses one direction of the absorption between them. In a lattice, f and g are typically ∧ and ∨, and both directions appear in the theory.

  -- x ∨ (x ∧ y) β‰ˆ x
  AbsorbsLeft : (∨ ∧ : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 ∨ ≑ Fin 2 β†’ ArityOf 𝑆 ∧ ≑ Fin 2
    β†’ X β†’ X β†’ Term X Γ— Term X
  AbsorbsLeft _ _ ∨-bin ∧-bin x y =
    appβ‚‚ ∨-bin (β„Š x) (appβ‚‚ ∧-bin (β„Š x) (β„Š y)) , β„Š x

  -- (x ∨ y) ∧ x β‰ˆ x
  AbsorbsRight : (∨ ∧ : OperationSymbolsOf 𝑆)
    β†’ ArityOf 𝑆 ∨ ≑ Fin 2 β†’ ArityOf 𝑆 ∧ ≑ Fin 2
    β†’ X β†’ X β†’ Term X Γ— Term X
  AbsorbsRight _ _ ∨-bin ∧-bin x y =
    appβ‚‚ ∧-bin (appβ‚‚ ∨-bin (β„Š x) (β„Š y)) (β„Š x) , β„Š x

In Th-Lattice, both AbsorbsLeft ∧-Op ∨-Op refl refl and AbsorbsRight ... appear as separate entries in Eq-Lattice.

This inventory covers every equation in Th-Magma (none), Th-Semigroup (associativity), Th-Monoid (associativity, left/right identity), Th-Group (the monoid equations + left/right inverse), Th-CommutativeMonoid (monoid + commutativity), Th-Semilattice (associativity + commutativity + idempotency), Th-Lattice (two associative + two commutative + two idempotent + two absorption), Th-Semiring and Th-Ring (the additive and multiplicative components + the two distributivity laws + ring-specific identities). Builders for less-uniform equations (the medial law, semigroup-with-identity-element-of-arity-two, etc.) are added per-need.