SUMMARY
- Home
- The Library
- Overture
- Setoid
- Classical
- Order
- Examples
- Exercises
- Legacy
- FLRP
- 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
- Installation
- Contributing
- Changelog