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.CommutativeRing       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
open import Classical.Structures.Unary                 public