Commit ce75866
Draft. Three commits on this branch, ahead of `main`:
1. **`879ec9b` docs(licence)** — long-form prose relicensed `MPL-2.0` →
`CC-BY-SA-4.0` (9 docs; re-applies the owner-authorised `f6cc023`).
2. **`c97d0c4` feat(aggregation)** — `EchoAggregation.agda` generalised
to the monoid/group form open issue **#175** asks for: `Monoid` /
`GroupAggregator` records, the proved `aggregation-as-fold` homomorphism
law, `sum`/`count`/`max`/`min` instances, the generic
`no-canonical-disaggregation-of` (also covers the **#174** no-section
sibling), and the macro `Example-PairSum` anchor the Oikos bridge cites.
The macro economics is now an *instance* of the general form — nothing
re-proved.
3. **`8744a25` docs(affirmation)** — `AFFIRMATION.adoc` re-anchored to
this branch @ `c97d0c4` and a new `docs/status/STATUS-2026-06-19.adoc`
(musts/intends/wishes; normative MUST = the Oikos accounting DSL).
**Verified green this session** (Agda 2.6.3 + stdlib 2.3 +
absolute-zero):
`agda --safe --without-K … All.agda` / `Smoke.agda` /
`characteristic/All.agda` exit 0; `scripts/kernel-guard.sh` PASS;
`postulate` declarations confined to the two unwired fenced modules
(`Fidelity.agda`, `EchoImageFactorizationPropPostulated.agda`), neither
imported by `All.agda`.
Refs #175, #174 (no auto-close — owner decides when the consumer side
lands).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku
---
_Generated by [Claude
Code](https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku)_
---------
Co-authored-by: Claude <noreply@anthropic.com>
1 parent 634e7a4 commit ce75866
2 files changed
Lines changed: 310 additions & 194 deletions
0 commit comments