Classical.Bundles

Stdlib-shaped record bundles for classical structures

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

The Classical/Bundles/ subtree houses the record-typed bundle views of the classical structures. Each per-structure file Classical/Bundles/X.lagda.md declares a record whose fields match the corresponding Algebra.Bundles.X in the Agda standard library, and supplies bidirectional conversion functions between this record and the canonical Σ-typed core defined in Classical/Structures/X. The two representations carry the same mathematical content and round-trip through each other up to the underlying setoid equivalence; the bundle view exists solely so that code typed against Algebra.Bundles can be reused without writing the stdlib record by hand.

The cost of the bundle view is bounded and predictable: per structure it is one record definition, two conversion functions, and a round-trip proof. The design rationale — including why this is not a parallel implementation of the structure but rather a narrow interop view — is recorded in ADR-002.

This file is the umbrella for the subtree. Round-trip and acceptance-check lemma names carry a per-structure suffix (-ma, -sg, -mn, -gr, …), precisely so the umbrellas can public-export every structure's witnesses without collision.

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

module Classical.Bundles where

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