[M4-2] Port the agda-algebras docs site's Agda-HTML styling and hover tooltips

[williamdemeo]

Blocks/feeds #24 (M4-2). Raised out of #17, where the agda-algebras documentation site turned out to be worth mining rather than merely admiring.

Why

The new agda-algebras documentation site — repo UniversalAlgebra/agda-algebras, hosted at https://agda-algebras.universalalgebra.org/ — is also MkDocs Material, so its solutions port over rather than needing reinvention. Its central design problem is the one M4-2 will hit: pages that are mostly Agda, rendered from agda --html output rather than from fenced code blocks that Pygments highlights.

Confirmed by reading its stylesheets/custom.css (41 KB) and page source:

• --md-code-font: "JuliaMono", "JetBrains Mono", "Fira Code", … — it reached the same monospace conclusion [M3-1] Choose the visual system #17 did, independently. Corroboration, and a reason the two sites will look consistent side by side.
• Body face is Inter on both sites, also independently.

What to port

1. The .Agda* token classes. agda --html emits 21 of them, and none are Pygments classes, so none of this site's syntax highlighting applies to them:

.AgdaKeyword .AgdaComment .AgdaString .AgdaNumber .AgdaSymbol .AgdaArgument
.AgdaMarkup .AgdaPrimitiveType .AgdaPrimitive .AgdaBound .AgdaGeneralizable
.AgdaInductiveConstructor .AgdaCoinductiveConstructor .AgdaDatatype .AgdaField
.AgdaFunction .AgdaMacro .AgdaModule .AgdaPostulate .AgdaRecord

Their site styles each one, with pre.Agda .Keyword aliases for the older class naming.

Do not copy the colours as-is. They are Agda's Emacs defaults — #0000cd for functions and datatypes, #b22222 for comments and strings, #cd6600 for keywords, #ee1289 for fields, #a020f0 for modules — chosen for a white Emacs buffer. On this site they have to clear WCAG AA on --c-bg-raised in both themes, which several will not. Derive them from tokens.css and check with make contrast-audit, which already walks every text element in both schemes; if the Agda pages are in the build, they are already covered.

2. Identifier cross-linking. agda --html makes every token a link to its definition — click a record, a constructor, a function and jump to where it is defined. That is the single most valuable property of their site and it comes free with the generator; the work is pipeline (getting the HTML into docs/) rather than CSS.

3. Hover tooltips. assets/js/agda-hover.js plus .agda-tooltip, .agda-tooltip-inner, .agda-tip-head, .agda-tip-snippet, .agda-tip-loading, .agda-tip-empty — type information on hover, fetched lazily. Nice, and the most work of the three. Judge it against #22 (M3-6): it adds script weight and needs a keyboard-accessible equivalent, since hover-only affordances fail WCAG 2.1 SC 1.4.13.

4. agda-copy.js and agda-toggle.js. Copy-a-block and show/hide. Material already provides content.code.copy for fenced blocks, but not for pre.Agda, so something equivalent is needed.

Worth telling them

Their site loads JuliaMono from cdn.jsdelivr.net and Inter/Roboto Mono from Google Fonts, while self-hosting Space Grotesk, Inter, Geist and Sora under assets/fonts/. So it is half-migrated to self-hosting already. scripts/python/build_fonts.py from #17 subsets and pins by SHA-256 and would port over nearly unchanged — worth offering upstream, given the Fira-Code-from-cdn.rawgit.com precedent that motivated #17 in the first place.

Tasks

• Get agda --html output into the build for at least one page, and decide where it comes from (checked in, generated in CI, or fetched).
• Style the 21 .Agda* classes from tokens.css, both themes.
• Confirm make contrast-audit covers those pages and passes.
• Confirm make font-audit reports no substitution on a real Agda-HTML page.
• Decide on hover tooltips, with a keyboard-accessible path or not at all.
• Copy-to-clipboard for pre.Agda.

Acceptance criteria

• An agda --html page renders in the site's visual system, in both themes, with no bespoke colours outside tokens.css.
• Identifier links resolve.
• make design-audit stays green with those pages in the build.