Skip to content

CHANGELOG

All notable changes to agda-algebras are documented in this file.

The format follows Keep a Changelog and this project aspires to Semantic Versioning.

[Unreleased] — 3.0 development

The 3.0 release is a major reconstruction of agda-algebras building on the Setoid-based redevelopment that shipped in v2.0.1 (December 2021). Work is organized into milestones tracked in docs/GITHUB_PROJECT.md.

Added

  • ADR-001 — Setoid/ as canonical development tree. docs/adr/001-setoid-as-canonical.md records the architectural decision and the alternatives considered.
  • src/Legacy/Base/DEPRECATED.md. Three-category inventory of legacy content (deprecated-with-replacement, pending-port, no-replacement-planned) with migration guidance.
  • Setoid-canonical tree. src/Setoid/ is the canonical development tree for 3.0.
  • Nix flake at the repo root pinning Agda 2.8.0 and standard-library 2.3, so nix develop provides a reproducible development environment.
  • INSTALL.md as the canonical installation guide.
  • GitHub Actions CI (.github/workflows/ci.yml) that type-checks the library on every push and pull request.
  • Community-health files: CONTRIBUTING.md, CODE_OF_CONDUCT.md, issue templates, pull-request template.
  • Dual license: Apache 2.0 for source code under src/, CC BY 4.0 for documentation under docs/.

  • Three new Overture/ submodules (M2-6, #303):

  • Overture.Terms (the W-type Term over a signature, with constructors ℊ and node);

  • Overture.Relations (the Equivalence Σ-bundle, the identity relation 0[_] with its IsEquivalence/Equivalence bundles, raw-function kernels kerRel / kernelRel / kerRelOfEquiv, the bare-types image-containment Im_⊆_, the compatibility relations _preserves_ and _|:_, and the lifting helpers eval-rel / eval-pred);
  • Overture.Functions (the bare-types image-and-inverse infrastructure Image_∋_ / Inv / InvIsInverseʳ, surjectivity IsSurjective with its right-inverse SurjInv and the composition law epic-factor, and the coordinate-projection cluster proj / projIsOnto).

These house the foundational definitions that the canonical Setoid/ tree had been importing from Legacy.Base.* since the M2-1 freeze; relocating them to Overture/ makes Setoid/ self-sufficient and lets Classical/ (M3-1, #260) build on a clean canonical foundation without inheriting a Legacy.Base dependency. See ADR-001 §Consequences "Setoid/ is not yet self-sufficient" for the motivation and src/Legacy/Base/DEPRECATED.md for the per-symbol relocation table. + Classical.Semigroup — first equation-bearing classical structure (M3-4, #261). Adds Semigroup as the first concrete classical structure with a non-empty equational theory, over the magma signature Sig-Magma (semigroups are precisely those magmas whose binary operation is associative — there is no Sig-Semigroup). Five files land: the equational theory (src/Classical/Theories/Semigroup.lagda.md), with singleton index enum Eq-Semigroup and theory map Th-Semigroup assoc = Associative ∙-Op refl 0F 1F 2F; the Σ-typed core (src/Classical/Structures/Semigroup.lagda.md), Semigroup α ρ = Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ Th-Semigroup, with the semigroup→magma forgetful projection, the Semigroup-Op named accessor module, and the eqsTo constructor; the bidirectional bundle bridge to Algebra.Bundles.Semigroup with a pointwise round-trip lemma (src/Classical/Bundles/Semigroup.lagda.md); the level-fixed 0ℓ–0ℓ veneer (src/Classical/Small/Structures/Semigroup.lagda.md); and (ℕ, +) as the canonical first worked example, constructed via eqsToSemigroup from stdlib's +-assoc (src/Examples/Classical/Semigroup.lagda.md). The module-header prose of Classical.Structures.Semigroup is normative for every subsequent equation-bearing structure's mechanics: theory representation (Eq-X index enum + Th-X builder composition), the explicit-codomain _⊨_ alias, the <Structure>-Op named module additively re-exporting the predecessor's accessors through the forgetful and adding equation-witness accessors, the <structure>→<weaker> forgetful projection, and the eqsTo<Structure>-family constructor factoring through the predecessor's opsTo<Weaker>. Subsequent structures (Monoid and Group in M3-6, Lattice in M3-7, Ring in M3-8) consume this template; deviations require their own ADR. See ADR-002 v2 §2, §3, §4, §5, §6 for the rationale. + Classical bundle-bridge naming convention: superscripts (M3-4, #261). The bundle-bridge conversion functions across the Classical/ tree use superscript-mnemonic names (⟨_⟩ᵐᵃ/⟪_⟫ᵐᵃ for Magma, ⟨_⟩ˢᵍ/⟪_⟫ˢᵍ for Semigroup, and analogously for later structures), rather than the subscript form used in the original M3-3 landing. The motivation is a uniform two-letter mnemonic per structure: the natural abbreviation for Semigroup is "sg", and g has no Unicode subscript, so the whole hierarchy moves to superscripts. The M3-3 Magma bridge is renamed accordingly (src/Classical/Bundles/Magma.lagda.md) along with its sole downstream consumer (src/Examples/Classical/Magma.lagda.md).

  • Classical.Magma — pattern-setting first concrete classical structure (M3-3, #331). Introduces the magma signature (src/Classical/Signatures/Magma.lagda.md), the Σ-typed core that degenerates to a type alias for the empty-theory base case Magma α ρ = Algebra α ρ in the module instance where Sig-Magma has already been fixed (src/Classical/Structures/Magma.lagda.md), the bidirectional bundle bridge to Algebra.Bundles.Magma with a pointwise round-trip lemma (src/Classical/Bundles/Magma.lagda.md), the level-fixed 0ℓ–0ℓ veneer (src/Classical/Small/Structures/Magma.lagda.md), and (ℕ, +) as the canonical first worked example (src/Examples/Classical/Magma.lagda.md). The module-header prose of Classical.Structures.Magma is normative for every subsequent classical structure's signature mechanics: hyphen-separated <symbol>-Op constructor naming, ar-<Structure> arity-function naming, Sig-<Structure> signature-value naming, ASCII ^ for operation-symbol interpretation, a named <Structure>-Op module housing curried user-facing accessors (so that downstream code can open <Structure>-Op 𝑿 once and use the binary operation in infix form a ∙ b, matching the open Magma M idiom of Algebra.Bundles), the curried-accessor body _∙_ = Curry₂ (<symbol>-Op ^ _), and the fromOp-family constructor pattern. Subsequent structures (Semigroup in M3-4, Monoid and Group in M3-6, Lattice in M3-7, Ring in M3-8) consume this template; deviations require their own ADR. See ADR-002 v2 §1, §5, §6, §7, §8 for the rationale.
  • Classical.Small.Structures and Examples.Classical aggregators (M3-3, #331). Two new umbrella files seeded by M3-3 (src/Classical/Small/Structures.lagda.md and src/Examples/Classical.lagda.md) re-export the per-structure level-fixed veneers and worked examples respectively. Each grows by one re-export line per subsequent M3-N issue.
  • Classical/ tree scaffold (M3-1, #260; M3-1a, #326). Six umbrella files introduce the directory layout for the classical-structures tree: top-level src/Classical.lagda.md plus subtree aggregators src/Classical/Signatures.lagda.md, src/Classical/Theories.lagda.md, src/Classical/Structures.lagda.md, src/Classical/Bundles.lagda.md, and src/Classical/Small.lagda.md. Each concrete structure will ship as a quintuple across these five subtrees (Signatures + Theories + Structures + Bundles + Small), per ADR-002. This issue ships scaffolding only — no concrete structure (Magma, Semigroup, Monoid, Group, Lattice, Ring) lands here; those are M3-2 onward. The library aggregator src/agda-algebras.lagda.md now re-exports Classical and the README.md library-structure description is updated to reflect the activation.
  • ADR-002 — Classical structures as Σ-typed cores with record-typed bundle views. docs/adr/002-classical-layer-design.md records the architectural decision: each classical structure X is Σ-typed at the core as X α ρ = Σ[ 𝑨 ∈ Algebra 𝑆ₓ α ρ ] 𝑨 ⊨ Eₓ (matching the mathematical reading "an X is an algebra equipped with a proof that it satisfies the X-theory"), with a parallel record-typed bundle view at Classical/Bundles/X for stdlib interop, equations stated purely in terms of the Algebra.Domain setoid equivalence for cubical portability, and a level-fixed Classical/Small/Structures/X veneer for the common ℓ₀–ℓ₀ case. The Classical/ tree builds on the canonical Setoid/ foundation (per ADR-001) and is designed for mechanical migration to Cubical/ (per ADR-003).
  • Canonical designation of Birkhoff's HSP theorem (M2-4, #259). Setoid.Varieties.HSP is now formally designated as the canonical home of Birkhoff's HSP theorem in agda-algebras. Cross-references added from Examples.Demos.HSP (the self-contained pedagogical companion for the TYPES 2021 paper) and from Legacy.Base.Varieties.FreeAlgebras (the frozen pre-3.0 bare-types proof). See ADR-001 for the broader Setoid-as-canonical rationale; the canonical proof is fully constructive, setoid-typed, and cubical-portable, which the legacy bare-types proof is not.
  • Classical.Operations and Classical.Equations infrastructure (M3-2, #330). Two new shared-infrastructure modules that every concrete Classical/X structure will depend on. src/Classical/Operations.lagda.md provides the per-arity Curry/Uncurry helpers that bridge the foundational tuple-indexed operation form (I → A) → A (used in Setoid.Algebras and the universal-algebra meta-theory) with the curried user-facing form A → A → A (used at every classical-structure use site). The Fin 2 η-failure under --cubical-compatible is contained here in Uncurry₂ / Curry₂; per-structure files do not write pair-style argument wrappers inline. src/Classical/Equations.lagda.md provides generic equation builders parametric in a signature and operation symbols within it (Associative, Commutative, Idempotent, LeftIdentity, RightIdentity, LeftInverse, RightInverse, DistributesOverˡ, DistributesOverʳ, AbsorbsLeft, AbsorbsRight). This module is the syntactic dual of stdlib's Algebra.Definitions, which provides the same inventory at the evaluated level; together with Classical.Operations, this is the concrete answer — beyond pedagogy — for why Classical/ exists as a parallel hierarchy rather than as a stdlib shim. Per-structure Classical/Theories/X.lagda.md files consume these builders in one-line compositions rather than re-deriving each equation. See ADR-002 §1, §3 for the rationale.
  • Self-documenting OperationSymbolsOf and ArityOf aliases (M3-2, #330). Added to src/Overture/Signatures.lagda.md, definitionally identical to the existing bracket notation ∣_∣ and ∥_∥. Per ADR-002 v2 §1, the long forms are preferred in new Classical/ code; the bracket forms remain available everywhere and are retained in Setoid/-tree code.
  • Operation-symbol-interpretation notation rename ̂ → ^ (M3-2, #330). The ASCII _^_ is introduced as the new canonical infix; the existing _̂_ is retained with a WARNING_ON_USAGE pragma and scheduled for removal in v3.1. See ADR-002 v2 §7.

Changed

  • Hard-wrapping prose is now allowed (docs/STYLE_GUIDE.md § "Wrapping prose", formerly § "Don't hard-wrap prose"). The guide previously required one paragraph per source line; both the wrapped and the unwrapped form are now acceptable, chosen per file and never mixed within one file. The reversal ratifies what the corpus already does — the Setoid.Algebras.Basic exemplar of #538 and most of the library are wrapped — and the section now also records the three wraps that damage the rendered page (between a code span and its attr_list braces, inside a reference-link label at a point with no space, and inside an inline code span), together with the standing exception that GitHub pull request, issue, and comment bodies must not be wrapped, since GitHub renders every newline there as a line break.

Changed (BREAKING)

  • Documentation rendering pipeline modernized to MkDocs (Material) (M10-1, #295). The Jekyll machinery that produced ualib.org is replaced by a MkDocs + Material site built from the .lagda.md sources. Code blocks get full agda --html token highlighting with per-token hyperlinks to definitions; inline prose terms are highlighted from their kramdown attribute spans (`Algebra`{.AgdaRecord}) via attr_list + docs/stylesheets/custom.css. See ADR-007 for the full rationale (architecture, domain, plugin set, URL scheme). Highlights:

  • New tooling. mkdocs.yml; scripts/python/mkdocs_gen_library.py mounts src/**/*.lagda.md as clean-URL pages and generates the navigation (mkdocs-gen-files + literate-nav + section-index); scripts/python/mkdocs_hooks.py rewrites repo-relative prose links to site URLs; scripts/python/gen_links.py generates the shared reference-link library docs/_links.md. flake.nix gains a pinned mkdocs-material + plugins Python environment, so nix develop --command make site reproduces the CI build.

  • Rendering. make site is the fast no-agda preview build; make site-full (CI) adds make agda-md (agda --html --html-highlight=code, embedded in the pages) and make html (the classic clickable-HTML site, restored — Everything.html index, published at /classic/). make serve previews locally.
  • New CI. .github/workflows/docs.yml runs make site-full and deploys to gh-pages on every push to master.
  • Build logging. The gen-files and render passes log per module/page (🛠/🖋 with status + a summary), so the build is no longer silent.
  • Visual identity. A modern theme: the Aurora indigo→violet palette (with Cobalt blue-led and Ultraviolet violet-led alternates documented in docs/site-guide.md), Space Grotesk display headings via a single --ualib-display variable, and Inter body text — all self-hosted under docs/assets/fonts/ (no font CDN). The Agda token palette is classic-vivid in light mode and the bespoke "Aurora Deep" (deep-indigo, orange keywords) in dark mode — shared by code blocks and inline prose terms — with "Tokyo Night" and "Nord" alternates documented in the site guide. A bespoke landing page (hero, by-the-numbers strip, an auto-advancing Featured-results portrait carousel with clickable dots, structures×properties coverage matrix), a module-dependency constellation (a d3 force-directed graph over the import graph), and a copy button on every highlighted <pre class="Agda"> block (docs/assets/js/agda-copy.js). Dark mode is the default on first landing.
  • URL scheme change. Rendered pages move from flat Module.Submodule.html to directory URLs /Module/Submodule/. mkdocs-redirects is wired in (empty map) to absorb the legacy URLs at the ualib.org cutover.
  • Link includes retired. The per-module Jekyll {% include UALib.Links.md %} directive is removed from every source; the shared link library is auto-appended to every page by pymdownx.snippets. Reference targets are root-relative so cross-references work under mkdocs serve and at ualib.org alike.
  • Legacy prose rebranded. Across src/Legacy/Base/**, front-matter titles and [Base.X.Y][] reference links are rebranded to Legacy.Base.X.Y, and the hand-rolled bottom-of-page navigation (superseded by Material's automatic footer) is removed.
  • Removed. admin/generate-html, admin/generate-tex, admin/illiterator/, and _config.yml (the Jekyll machinery).

Pointing GitHub Pages at gh-pages, attaching the ualib.org custom domain, and the registrar DNS change are deferred to the maintainer as a documented cutover checklist; the currently-live site is untouched by this change.

  • Demos/ folded into Examples/Demos/ (M4-18, #436). The demos were always worked examples of the library in use, so the top-level Demos/ tree now lives under the single Examples/ umbrella. The three modules are renamed accordingly — Demos.HSP → Examples.Demos.HSP, Demos.ContraX → Examples.Demos.ContraX, Demos.GeneralOperationsAndRelations → Examples.Demos.GeneralOperationsAndRelations, and the Demos barrel becomes Examples.Demos (re-exported by the Examples barrel). This is a breaking change for any downstream import Demos.*; update to import Examples.Demos.*. The Examples.Demos.HSP TYPES 2021 paper artifact is relocated but otherwise frozen: its internal notation and source self-citations are untouched, and its heading anchors remain exempt from the anchor sweep. The legacy /Demos/… site URLs are noted for the redirect map in the #430 cutover checklist.

  • ADR-002 revised to v2 (no associated issue; revision documented in the ADR itself). The original ADR-002 was authored ahead of the M3-2 Semigroup load test; v2 incorporates the findings from that load test. No higher-level architecture is overturned; the revisions clarify and refine the original decisions across nine numbered sections. See the ADR's Empirical revision history section for the substantive content of the revision.

  • src/Base/ frozen as src/Legacy/Base/ (M2-1, #256). Setoid/ is now the canonical development tree for agda-algebras 3.0. The pre-3.0 bare-types tree has been moved to src/Legacy/Base/; the top-level aggregator agda-algebras.lagda.md re-exports it as Legacy.Base. This is a breaking change for downstream users of Base.*. The migration is mechanical for most imports; see src/Legacy/Base/DEPRECATED.md for the categorization (deprecated-with-replacement vs. pending-port vs. no-replacement-planned) and docs/adr/001-setoid-as-canonical.md for the rationale.

Migration recipe (most imports):

   sed -i -E 's/import(\s+)Base\./import\1Legacy.Base./g' YOUR_FILE.lagda.md

For modules that have a Setoid/ analog (Category A in DEPRECATED.md), prefer migrating to the Setoid.* import and passing Relation.Binary.PropositionalEquality.setoid A where a setoid is now expected. For modules without one (Category B), the Legacy.Base.* import is the supported interim path until the per-orphan port lands. + src/agda-algebras.lagda.md substantially revised (#256). Updated to reflect the v3.0 source-tree organization (canonical Setoid/, planned Classical/ and Cubical/, frozen Legacy.Base/). Removed stale per-file license boilerplate that contradicted the project-level licensing. + Agda target: 2.6.2 → 2.8.0. + Standard library target: 1.7 → 2.3. + Pragma: --without-K → --cubical-compatible across the tree. See src/Overture/Basic.lagda.md for the reasoning. + Literate-Agda format (breaking for external links into docs/lagda/). The historical dual-tree split — minimal src/X/Y/Z.agda skeletons paired with LaTeX-literate docs/lagda/X/Y/Z.lagda content — is consolidated into unified Markdown-literate src/X/Y/Z.lagda.md files. 127 module pairs were collapsed; the docs/lagda/ tree was deleted. Rationale and migration policy are recorded in ADR-004. External bookmarks pointing at specific docs/lagda/X/Y/Z.lagda paths will not resolve; the rendered documentation site at https://ualib.org is unaffected because it serves X.Y.Z.html paths under the same scheme as before. + Documentation directory: doc/ → docs/ following modern conventions. + README: rewritten for the 3.0 line.

Deprecated

  • docs/INSTALL_AGDA.md superseded by INSTALL.md. ~Retained with a deprecation banner; will be removed in a future release.~ removed
  • Legacy.Base.Terms.{Term, ℊ, node} (M2-6, #303). Use Overture.Terms.{Term, ℊ, node} instead. The two Term types are definitionally identical; migration is a pure import rewrite.
  • Legacy.Base.Relations.Quotients.{Equivalence, [], 0[]Equivalence, 0[_]IsEquivalence} (M2-6, #303). Use Overture.Relations instead.
  • Legacy.Base.Relations.Discrete.{0[], kerRel, kerRelOfEquiv, kernelRel, Im⊆, _preserves, |:, eval-rel, eval-pred} (M2-6, #303). Use Overture.Relations instead.
  • Legacy.Base.Functions.Inverses.{Image_∋_, eq, Inv, InvIsInverseʳ} (M2-6, #303). Use Overture.Functions instead.
  • Legacy.Base.Functions.Surjective.{IsSurjective, IsSurjective→Surjective, Surjective→IsSurjective, SurjInv, SurjInvIsInverseʳ, epic-factor, epic-factor-intensional, proj, projIsOnto} (M2-6, #303). Use Overture.Functions instead.
  • Legacy.Base.Relations.Continuous.{Rel, Rel-syntax, REL, REL-syntax, eval-Rel, compatible-Rel, eval-REL, compatible-REL} (M2-7d, #308). Use Setoid.Relations.Continuous.X instead. Notes: the canonical module introduces a Π-setoid layer (⨅ˢ) and explicit Π-Respects-Rel / Π-Respects-REL predicates as an overlay on the bare-types relation types, mirroring the design of Setoid.Relations.Quotients; the canonical compatible-REL corrects a bug in the legacy form, which read Π[ t ] eval-REL R t and was thereby independent of its operation argument.
  • Legacy.Base.Relations.Properties.{Reflexive, Sym, Symmetric, Trans, TransFlip, Transitive, Antisym, Antisymmetric, Irreflexive, Asymmetric, Connex, Total} (M2-7e, #309). Use Setoid.Relations.Properties.X instead. Notes: the canonical Reflexive uses stdlib's curried Rel A ℓ rather than Pred (A × A) ℓ; the canonical Connex is homogeneous (Rel A ℓ on both sides) where the legacy form was heterogeneous (define locally if you need the heterogeneous form).
  • Legacy.Base.Relations.Properties.{curry, uncurry} (M2-7e, #309). Use Data.Product.{curry, uncurry} (stdlib) instead.
  • Legacy.Base.Functions.Transformers.{Bijection, ∣∣=∣∣, PointwiseBijection, ∣∣≈∣∣, Curry, Uncurry, CurryFin2, UncurryFin2, CurryFin3, UncurryFin3} (M2-7f, #310). Use Examples.FunctionTypeBijections.X instead. This is the only M2-7 relocation that lands in Examples/ rather than Setoid/ or Overture/: the content is illustrative (an n-ary-function-encoding cautionary tale about η-expansion failures in Fin-indexed types) rather than load-bearing for the universal-algebra core. Stdlib alternatives: Function.Bundles.Bijection for setoid-flavored bijections; Function.Base.{curry, uncurry} for the basic combinators.
  • Legacy.Base.Varieties.Invariants.AlgebraicInvariant (M2-7g, #311). Use Setoid.Varieties.Invariants.AlgebraicInvariant instead. The setoid port carries an extra implicit ρᵃ level on Algebra but is otherwise definitionally identical; migration is a pure import rewrite.

Each deprecated definition carries a {-# WARNING_ON_USAGE #-} pragma at its definition site pointing at the canonical home. The legacy modules themselves continue to type-check and to export the deprecated names; the removal of these names is scheduled for the next minor release after the release that lands the corresponding port (per the deprecation policy in docs/STYLE_GUIDE.md).

Migration recipe (most call sites): replace open import Legacy.Base.X using (…) with open import Overture using (…) (since the Overture aggregator re-exports Overture.Relations and Overture.Functions); for Term / ℊ / node, use open import Overture.Terms {𝑆 = 𝑆} using (…) directly since the parameterized module is not re-exported through the umbrella.

Migration recipe for the M2-7 destinations: replace open import Legacy.Base.Relations.Continuous with open import Setoid.Relations.Continuous; Legacy.Base.Relations.Properties with Setoid.Relations.Properties (and replace Legacy.Base.Relations.Properties.{curry, uncurry} with Data.Product.{curry, uncurry} from stdlib); Legacy.Base.Functions.Transformers with Examples.FunctionTypeBijections; Legacy.Base.Varieties.Invariants with Setoid.Varieties.Invariants. The Setoid.Relations and Setoid.Varieties aggregators re-export their Properties, Continuous, and Invariants submodules under #308–#311, so most call sites can simplify to open import Setoid.Relations using (…) or open import Setoid.Varieties using (…).

Removed

  • docs/lagda/ tree (127 LaTeX-literate .lagda files). Content migrated to src/X/Y/Z.lagda.md; see "Literate-Agda format" above.
  • src/X/Y/Z.agda skeleton companions (127 files) that were mechanically derived from the LaTeX-literate sources by admin/illiterator/. The illiterator program itself is slated for deletion in the rendering-pipeline-modernization follow-up.

Fixed

Nothing to report. 3.0 is a forward-looking reconstruction rather than a bug-fix release.

[2.0.1] — 2021-12-07

Archival release coinciding with the TYPES 2021 submission. This version was the first to use the Setoid-based formulation, reconstructed from the earlier UALib project. Archived on Zenodo: DOI 10.5281/zenodo.5765793.

Targets Agda 2.6.2 and standard-library 1.7.

[1.x and earlier]

The earlier UALib library (GitLab-hosted) and the pre-v2.0.1 agda-algebras work. No per-version changelog was maintained; see the git log and the related papers for details.