Skip to content

Classical.Structures

Ī£-typed cores of classical structures

This is the Classical.Structures module of the Agda Universal Algebra Library.

The Classical/Structures/ subtree houses the Ī£-typed cores ā€” the canonical library-internal representation of each classical structure. For each concrete X with signature š‘†ā‚“ (from Classical/Signatures/X) and equational theory Eā‚“ (from Classical/Theories/X), the core is

X : (Ī± Ļ : Level) ā†’ Type _
X Ī± Ļ = Ī£[ š‘Ø āˆˆ Algebra Ī± Ļ ] š‘Ø āŠØ Eā‚“

which means X is an algebra equipped with a proof that it satisfies the X-theory. The Ī£ formulation is natural and robust under the eventual cubical port: no theorem in this subtree depends on setoid-specific machinery, so substituting the path-type equivalence for the setoid equivalence is a search-and-replace operation rather than a rewrite. The full rationale is recorded in ADR-002.

Each per-structure file Classical/Structures/X.lagda.md also ships named convenience accessors (Domain, Signature, equations) that offset the use-site ergonomic cost of Ī£-projection against the named-field projection a record would have provided. Bidirectional bridges to a stdlib-shaped record view are provided in the parallel Classical/Bundles/ subtree.

This file is the umbrella for the subtree. The concrete Magma and Semigroup submodules are the initial, pattern-setting structures.

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

module Classical.Structures where

open import Classical.Structures.CommutativeMonoid public
open import Classical.Structures.CommutativeSemigroup public
open import Classical.Structures.AbelianGroup public
open import Classical.Structures.CommutativeRing public
open import Classical.Structures.DistributiveLattice public
open import Classical.Structures.Group public
open import Classical.Structures.Interpret public
open import Classical.Structures.Lattice public
open import Classical.Structures.Magma public
open import Classical.Structures.Monoid public
open import Classical.Structures.Ring public
open import Classical.Structures.Semigroup public
open import Classical.Structures.Semilattice public