docs: add STYLE.md (initial stub for M4 refinement)

Adds a first draft of docs/STYLE.md documenting the conventions
agda-algebras currently follows, with explicit flags for the axes where
style decisions remain open (naming conventions, notation table,
universe-level variable scope).

The style guide is deliberately short at this stage.  Applying and
refining it across Setoid/ and Classical/ is tracked in M4-1, and the
document will grow as specific decisions are settled.  A premature
full-length style guide would codify decisions that are properly made
during the M4 sweep.

Addresses #253 (M1-4).

Author: williamdemeo

docs/STYLE.md

@@ -0,0 +1,129 @@
+<!-- File: docs/STYLE.md -->
+
+# agda-algebras Style Guide
+
+This document describes the conventions that the `agda-algebras` library follows.  It is a living document: when the library adopts a new convention, this file changes.  When it describes a convention that the library doesn't actually follow, it's wrong — the code is the ground truth, and the style guide chases it.
+
+The long-tail work of applying this guide consistently across `Setoid/` and `Classical/` is tracked in [#M4-1](https://github.com/ualib/agda-algebras/issues).  This document is the reference for that sweep; it will be refined as specific axes are settled.
+
+---
+
+## File format
+
+Every Agda source file begins with:
+
+```agda
+{-# OPTIONS --cubical-compatible --safe --exact-split #-}
+```
+
+followed, on the next non-comment line, by the module header.  The module name must match the filename (with `/` replaced by `.` under the `src/` include root): `src/Base/Algebras/Basic.agda` contains `module Base.Algebras.Basic where`.
+
+Exceptions:
+
++  `src/Legacy/Base/` retains its historical `--without-K` pragma.  New contributions do not belong in this tree.
++  `src/Everything.agda` is generated by the Makefile; do not edit it directly.
+
+## Module structure
+
++  One concept per module, where feasible.  A module called `Congruences` should be about congruences.  When a module grows large enough to warrant subdivision, make the subdivision along mathematical lines, not lines of implementation convenience.
+
++  Module headers name the mathematical object being developed, not the technical construction (`Setoid.Algebras.Congruences` over `Setoid.Algebras.Records.QuotientRecords`).
+
++  Re-exports use `open import X public` at the top of an umbrella module, with imports grouped into blocks (stdlib, then internal, with a blank line between).
+
++  Classical algebraic structures follow the Signatures / Theories / Structures / Bundles / Small quintuple pattern (see [#253's M3-1 description](../blob/master/docs/GITHUB_PROJECT.md) for the reasoning).
+
+## Imports
+
++  Prefer tight `using (...)` clauses over bare `open import X`.
+
++  Group imports into blocks with blank lines between: Agda primitives, stdlib, internal modules.  Within each block, alphabetize.
+
+## Naming
+
+The library has some established conventions and some open questions.
+
+**Established**:
+
++  Types start with uppercase: `Algebra`, `Congruence`, `Homomorphism`.
++  Level variables are lowercase Greek: `α`, `β`, `ρ`, `ℓ`.
++  First/second projections of Σ-types are `∣_∣` and `∥_∥` rather than `proj₁` / `proj₂` (a long-standing agda-algebras idiom carried over from the Escardó style).
+
+**Not yet settled** (tracked in M4-1):
+
++  Whether predicates are named `IsX` (matching stdlib idiom) or `is-X` (matching some parts of the existing code).  Until settled, follow local convention.
++  The scope of universe-level variables `𝓞` and `𝓥` (design-discussion in #M4-3).
+
+When in doubt, follow the convention of the surrounding code and ask in the PR.
+
+## Notation
+
+Notation in agda-algebras is Unicode-heavy and largely inherited from Escardó-style type-theory developments.  A canonical symbol table will land as part of M4-1.
+
+Pending that, the rules of thumb are:
+
++  Do not introduce new notation for a concept that already has notation elsewhere in the library.
++  If you're adding notation for a new concept, make it consistent with the surrounding idioms.
++  Avoid overloading single Unicode characters with multiple meanings.
+
+## Record vs Σ
+
++  The core `Algebra` type is a record.  This was an early design choice and remains canonical.
++  Classical algebraic structures (`Semigroup`, `Monoid`, etc.) are Σ-typed at the core, with record-typed bundle views for stdlib interop (ratified in ADR-002, to land with M3-1).
++  When adding a new structure, the default is: record for foundational types that will be inhabited many times and benefit from named projections; Σ for theories-over-an-algebra whose mathematical meaning is "an algebra equipped with a proof it satisfies a theory."
+
+## Proof style
+
++  Prefer many small focused theorems over few large ones.  A theorem whose proof is more than about 20 lines should usually be restructured as two or three lemmas.
+
++  Named helper lemmas over `where`-clauses and opaque rewrite chains.  A named lemma becomes part of the library's training corpus; a `where`-clause does not.
+
++  Explicit type signatures on every public definition.  Not just the ones Agda cannot infer: the ones humans will want to read.
+
++  Equational reasoning with `≡⟨ ⟩` / `≈⟨ ⟩` notation is preferred over manual `trans` / `sym` chains when feasible.
+
+## Comments and documentation
+
+agda-algebras is intended to serve as a high-quality corpus of Agda proofs for machine-learning work.  Comments are first-class artifacts, not afterthoughts.
+
+Every public definition should have a prose comment block immediately above it explaining:
+
++  What the definition is, in the same terms a mathematician would use.
++  When one would use it, in terms of mathematical motivation.
++  Cross-references to related definitions (the closest mathematical neighbors, not everything possibly related).
+
+Example:
+
+```agda
+-- | `Hom 𝑨 𝑩` is the type of homomorphisms from 𝑨 to 𝑩.  A homomorphism
+-- | is a function on carriers that commutes with every basic operation of
+-- | the signature.  See also: `IsHomomorphism` for the predicate form,
+-- | and `Base.Homomorphisms.Isomorphisms` for the isomorphism variant.
+Hom : (𝑨 : Algebra α) (𝑩 : Algebra β) → Type _
+Hom 𝑨 𝑩 = ...
+```
+
+These prose comments are not decoration — they are part of the training data the library aspires to produce.  Treat each one as a short paragraph that would help a mathematician approaching this concept for the first time.
+
+## Deprecation
+
+The public API stability policy: breaking changes to names or signatures in publicly-exported definitions go through at least one minor-version deprecation cycle.  Internal helpers (not re-exported from umbrella modules, not documented) can change without notice.
+
+To deprecate a public definition:
+
+1.  Add the new form.
+2.  Mark the old form with a `{-# WARNING_ON_USAGE ... #-}` pragma explaining the replacement.
+3.  Announce in `CHANGELOG.md` under `### Deprecated`.
+4.  Remove the old form no sooner than the next minor version.
+
+## References
+
++  The full milestone roadmap: [`docs/GITHUB_PROJECT.md`](GITHUB_PROJECT.md).
++  Architecture Decision Records: [`docs/adr/`](adr/) (scaffolding tracked in #M1-6).
++  Contributor workflow: [`CONTRIBUTING.md`](../CONTRIBUTING.md).
+
+---
+
+*This document is incomplete by design.  It will be refined as specific style decisions are settled in M4.  Contributions to STYLE.md itself are welcome, particularly if you encounter an undocumented convention while working on the library.*
+
+