SUMMARY
- Home
- The Library
- Overture
- Setoid
- Classical
- Bundles
- Categories
- Equations
- Interpretations
- Operations
- Properties
- Signatures
- Small
- Structures
- CommutativeMonoid
- CommutativeRing
- CommutativeSemigroup
- Group
- AbelianGroup
- Basic
- Centralizer
- Commutator
- Complements
- Complexes
- Congruences
- Conjugation
- Cosets
- Dedekind
- Diagonal
- GSet
- IndexAction
- MaximalSubgroup
- MinimalNormal
- MinimalNormalDescent
- NormalClosure
- NormalCore
- NormalSubgroupLattice
- PartitionSubgroup
- Power
- PowerCollapse
- Product
- RegularAction
- Simple
- SubgroupClassification
- SubgroupLattice
- Subgroups
- TableGroup
- Wreath
- Interpret
- Lattice
- Magma
- Monoid
- Ring
- Semigroup
- Semilattice
- Unary
- Theories
- Order
- Examples
- Exercises
- Legacy
- Everything (module index)
- Classic Agda HTML ↗
- Constellation
- Project
- Roadmap
- Maintaining the site
- Style Guide
- Architecture Decisions
- Overview
- ADR-NNN: Short noun phrase describing the decision
- ADR-001: Setoid as canonical development tree for 3.0
- ADR-002: Classical structures over the universal-algebra foundation
- ADR-003: Cubical Agda as the canonical long-term target
- ADR-004: Markdown-literate Agda (
.lagda.md) as the canonical literate format - ADR-005: Scope of the
𝓞/𝓥universe-level variables - ADR-006: Signature morphisms and the self-contained
Sigcategory - ADR-007: MkDocs (Material) as the documentation rendering pipeline
- ADR-008: Two-layer congruence discipline for finite algebras
- ADR-009: Signature genericity via generalized variables in the core; module parameters at the Classical layer
- ADR-010: Documentation coverage policy for public definitions
- ADR-011:
--without-Kfor every module
- Installation
- Contributing
- Changelog