diff --git a/build-tools/static/md/mkdocs/docs/css/agda-hover.css b/build-tools/static/md/mkdocs/docs/css/agda-hover.css
new file mode 100644
index 000000000..6a741fad7
--- /dev/null
+++ b/build-tools/static/md/mkdocs/docs/css/agda-hover.css
@@ -0,0 +1,134 @@
+/* ==========================================================================
+   Agda Hover Tooltip (clean + compact)
+   --------------------------------------------------------------------------
+   Tuning knobs:
+   - --agda-font-base: base font size used for most text in the tooltip
+   - --agda-font-code: font size for code snippet
+   - --agda-line-base: line-height for body text
+   - --agda-line-code: line-height for code snippet
+   - --agda-width:     max width of the tooltip
+   - --agda-ch:        max code line width in characters (for readability)
+   ========================================================================== */
+
+/* === Theme + size tokens ================================================= */
+:root,
+[data-md-color-scheme="default"] {
+  /* Sizes (make smaller/larger here) */
+  --agda-font-base: 0.72rem;   /* overall base text size (very compact) */
+  --agda-font-code: 0.70rem;   /* code size (very compact) */
+  --agda-line-base: 1.05rem;   /* base line-height */
+  --agda-line-code: 1.06rem;   /* code line-height */
+  --agda-width:     min(34rem, 90vw); /* tooltip max width */
+  --agda-ch:        68ch;      /* max code line width */
+
+  /* Colors (light) */
+  --agda-tip-bg:     #ffffff;
+  --agda-tip-fg:     #1f2328;
+  --agda-tip-border: rgba(0,0,0,.10);
+  --agda-tip-link:   #0969da;  /* reserved if links added later */
+  --agda-tip-codebg: rgba(127,127,127,.06);
+  --agda-shadow:     0 6px 16px rgba(0,0,0,.14), 0 2px 6px rgba(0,0,0,.10);
+}
+
+[data-md-color-scheme="slate"] {
+  /* Colors (dark) */
+  --agda-tip-bg:     #1f2430;
+  --agda-tip-fg:     #f4f6f8;
+  --agda-tip-border: rgba(255,255,255,.14);
+  --agda-tip-link:   #8ab4ff;
+  --agda-tip-codebg: rgba(255,255,255,.04);
+  --agda-shadow:     0 6px 16px rgba(0,0,0,.25), 0 2px 6px rgba(0,0,0,.18);
+}
+
+/* === Tooltip container =================================================== */
+.agda-tooltip {
+  position: absolute;
+  z-index: 2000;
+  max-width: var(--agda-width);
+  background: var(--agda-tip-bg);
+  color: var(--agda-tip-fg);
+  border: 1px solid var(--agda-tip-border);
+  border-radius: .35rem;
+  box-shadow: var(--agda-shadow);
+  opacity: 1;
+  transform: none;
+
+  /* Hover-only behavior: no interactions inside the box */
+  pointer-events: none;
+  /* To allow selection/copy, flip to 'auto' */
+}
+
+.agda-tooltip.hidden {
+  opacity: 0;
+  /* Tooltip is purely informational; hide by opacity. */
+  /* (JS is already preventing pointer events when hidden.) */
+}
+
+/* === Inner layout ======================================================== */
+.agda-tooltip .agda-tooltip-inner {
+  padding: .36rem .48rem;   /* very tight padding */
+  font-size: var(--agda-font-base);
+  line-height: var(--agda-line-base);
+}
+
+/* === Header line (kind · name · module) ================================= */
+.agda-tip-head {
+  display: flex;
+  align-items: baseline;
+  gap: .32rem;
+  margin-bottom: .16rem;
+  font-weight: 600;
+}
+
+.agda-kind {
+  font-size: calc(var(--agda-font-base) - 0.06rem); /* tiny label */
+  letter-spacing: .04em;
+  text-transform: uppercase;
+  opacity: .72;
+}
+
+.agda-name {
+  font-family: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas,
+               "Liberation Mono", "Courier New", monospace;
+  font-size: calc(var(--agda-font-base) - 0.02rem);
+  font-weight: 700;
+}
+
+.agda-module {
+  margin-left: auto;
+  font-size: calc(var(--agda-font-base) - 0.08rem);
+  opacity: .55;
+}
+
+/* === Code preview ======================================================== */
+.agda-tip-snippet {
+  margin: .10rem 0 0 0;
+  padding: .30rem .40rem;
+  border-radius: .28rem;
+  background: var(--agda-tip-codebg);
+
+  font-family: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas,
+               "Liberation Mono", "Courier New", monospace;
+  font-size: var(--agda-font-code);
+  line-height: var(--agda-line-code);
+
+  /* Keep Agda formatting exactly. If you prefer wrapping, change to 'pre-wrap'. */
+  white-space: pre;
+
+  /* Width hygiene */
+  max-width: var(--agda-ch);
+  overflow-x: auto;  /* allow horizontal scroll for long types */
+  overflow-y: hidden;
+}
+
+/* When no snippet could be extracted */
+.agda-tip-empty {
+  margin: .12rem 0 0 0;
+  font-size: calc(var(--agda-font-base) - 0.04rem);
+  opacity: .85;
+}
+
+/* === Legacy / unused bits (kept inert) ================================== */
+/* If older CSS defines these, keep them invisible to avoid layout churn. */
+.agda-tip-actions { display: none !important; }
+.agda-open-def    { display: none !important; }
diff --git a/build-tools/static/md/mkdocs/docs/js/agda-hover.js b/build-tools/static/md/mkdocs/docs/js/agda-hover.js
new file mode 100644
index 000000000..41e74d2c5
--- /dev/null
+++ b/build-tools/static/md/mkdocs/docs/js/agda-hover.js
@@ -0,0 +1,344 @@
+// === Agda hover definitions ===============================================
+// Works on Agda-generated HTML embedded in Markdown, i.e., inside <pre class="Agda">.
+// Shows a tooltip on hover with (1) token info, (2) link to full definition,
+// and (best-effort) a short snippet from the target page near the anchor.
+
+(function () {
+  const HOVER_SELECTOR = 'pre.Agda a[href]';       // limit to Agda pre blocks
+  const HOVER_DELAY_MS = 120;                      // small debounce to avoid flicker
+  const MAX_SNIPPET_CHARS = 220;                   // keep tooltips compact
+  const cache = new Map();                         // href -> { html, title, className, module, snippet }
+
+  let tooltipEl = null;
+  let hideTimer = null;
+  let showTimer = null;
+
+  function createTooltip() {
+    if (tooltipEl) return tooltipEl;
+    tooltipEl = document.createElement('div');
+    tooltipEl.className = 'agda-tooltip hidden';
+    tooltipEl.setAttribute('role', 'tooltip');
+    tooltipEl.innerHTML = '<div class="agda-tooltip-inner"></div>';
+    document.body.appendChild(tooltipEl);
+    return tooltipEl;
+  }
+
+  function positionTooltip(evt, el) {
+    const pad = 12;
+    const vw = window.innerWidth;
+    const vh = window.innerHeight;
+    const rect = el.getBoundingClientRect();
+    const tipRect = tooltipEl.getBoundingClientRect();
+    let top = rect.bottom + window.scrollY + pad;
+    let left = evt.clientX + window.scrollX + pad;
+
+    // if overflowing right edge, shift left
+    if (left + tipRect.width > window.scrollX + vw - pad) {
+      left = Math.max(window.scrollX + pad, vw + window.scrollX - tipRect.width - pad);
+    }
+    // if too low, pop above
+    if (top + tipRect.height > window.scrollY + vh - pad) {
+      top = rect.top + window.scrollY - tipRect.height - pad;
+    }
+    tooltipEl.style.top = `${top}px`;
+    tooltipEl.style.left = `${left}px`;
+  }
+
+  function sanitize(text) {
+    // very small helper: we only ever insert our own strings; still, be safe
+    const div = document.createElement('div');
+    div.textContent = text == null ? '' : String(text);
+    return div.innerHTML;
+  }
+
+  function inferTokenInfo(a) {
+    // Try to infer token info from the Agda link classes + URL
+    const classes = (a.getAttribute('class') || '').split(/\s+/).filter(Boolean);
+    const agdaClass = classes.find(c => /^(Function|Field|Datatype|Record|Module|Primitive|InductiveConstructor|Operator)$/.test(c)) || 'Symbol';
+    const href = a.getAttribute('href') || '';
+    const url = new URL(href, window.location.href);
+    const moduleFile = (url.pathname.split('/').pop() || '').replace(/\.html$/,'');
+    const moduleName = moduleFile || 'Module';
+    // The visible label (basename) is often adjacent; fall back to text
+    const basename = a.textContent.trim() || moduleName;
+    const anchor = url.hash ? url.hash.slice(1) : '';
+    return { href: url.href, basename, agdaClass, moduleName, anchor };
+  }
+
+  async function fetchSnippet(href, anchor) {
+    try {
+      const res = await fetch(href, { credentials: 'same-origin' });
+      if (!res.ok) throw new Error(`HTTP ${res.status}`);
+      const html = await res.text();
+
+      const dom = new DOMParser().parseFromString(html, 'text/html');
+
+      // 1) Find the anchor element, then its closest Agda <pre>
+      const target = anchor ? dom.getElementById(anchor) : null;
+      const pre = target ? target.closest('pre.Agda') : dom.querySelector('pre.Agda');
+      if (!pre) return { snippet: '' };
+
+      // 2) Compute the anchor's character offset within that <pre>
+      const index = target ? charIndexWithin(pre, target) : -1;
+
+      // 3) Extract a multi-line definition block that surrounds the anchor
+      const text = pre.textContent || '';
+      const { block } = extractDefinitionBlock(text, index, {
+        // -- tweakable knobs --
+        minLines: 2,     // default: 2 lines
+        maxLines: 14,    // default: 14 lines
+        maxChars: 1200,  // hard cap to keep tooltips snappy
+        includeUpwardSignature: true,
+      });
+
+      return { snippet: block.trim() };
+    } catch (_e) {
+      return { snippet: '' };
+    }
+  }
+  // async function fetchSnippet(href, anchor) {
+  //   try {
+  //     const res = await fetch(href, { credentials: 'same-origin' });
+  //     if (!res.ok) throw new Error(`HTTP ${res.status}`);
+  //     const html = await res.text();
+
+  //     // Best-effort: parse the target page & grab nearby code around the anchor
+  //     const dom = new DOMParser().parseFromString(html, 'text/html');
+  //     const target = anchor ? dom.getElementById(anchor) : null;
+  //     const pre = target ? target.closest('pre.Agda') : dom.querySelector('pre.Agda');
+
+  //     if (!pre) return { snippet: '' };
+
+  //     // Convert the <pre> to text and extract a compact snippet around the anchor id
+  //     const preText = pre.textContent || '';
+  //     if (!preText) return { snippet: '' };
+
+  //     let snippet = preText;
+  //     // Try to bias toward the area containing the anchor id text (Agda puts ids on <a>, not text;
+  //     // so we approximate by taking the middle of the <pre> if we don't find anything)
+  //     const mid = Math.floor(preText.length / 2);
+  //     const start = Math.max(0, mid - Math.floor(MAX_SNIPPET_CHARS / 2));
+  //     snippet = preText.slice(start, start + MAX_SNIPPET_CHARS).trim();
+
+  //     // Normalize whitespace; keep “code” flavor
+  //     snippet = snippet.replace(/\s+\n/g, '\n').replace(/\n{3,}/g, '\n\n');
+
+  //     return { snippet };
+  //   } catch (_e) {
+  //     return { snippet: '' };
+  //   }
+  // }
+
+  /**
+   * Compute the character index of `node` relative to the start of `root`,
+   * by using a DOM Range. Falls back to -1 if anything fails.
+   */
+  function charIndexWithin(root, node) {
+    try {
+      const r = document.createRange();
+      r.setStart(root, 0);
+      r.setEnd(node, 0);
+      return r.toString().length;
+    } catch {
+      return -1;
+    }
+  }
+
+  /**
+   * Heuristically extract a "definition block" around `anchorIndex`.
+   * Strategy:
+   *  - Split <pre> text into lines, track cumulative offsets.
+   *  - Find the line containing anchorIndex (or mid if -1).
+   *  - Expand upward to include header/signature lines:
+   *      - previous non-empty lines that are less-indented than the current line (headers),
+   *      - or that look like a type signature (contains ':' or 'record'/'data'/'module').
+   *  - Expand downward while:
+   *      - line is indented >= firstDefIndent (continuation/clauses),
+   *      - OR it’s a clause/where/with line,
+   *      - stop at first blank line following content.
+   *  - Enforce min/max lines and maxChars guardrails.
+   */
+  function extractDefinitionBlock(text, anchorIndex, opts) {
+    const {
+      minLines = 2,
+      maxLines = 12,
+      maxChars = 1000,
+      includeUpwardSignature = true,
+    } = opts || {};
+
+    const lines = text.split(/\r?\n/);
+    const lens = lines.map(l => l.length + 1); // +1 for newline
+    const starts = new Array(lines.length);
+    let acc = 0;
+    for (let i = 0; i < lines.length; i++) {
+      starts[i] = acc;
+      acc += lens[i];
+    }
+
+    // Find anchor line (or fallback to middle line)
+    let iAnchor = 0;
+    if (anchorIndex >= 0) {
+      for (let i = 0; i < starts.length; i++) {
+        const s = starts[i];
+        const e = s + Math.max(0, lens[i] - 1); // exclude trailing newline
+        if (anchorIndex >= s && anchorIndex <= e) { iAnchor = i; break; }
+        if (anchorIndex < s) { iAnchor = Math.max(0, i - 1); break; }
+        if (i === starts.length - 1) iAnchor = i;
+      }
+    } else {
+      iAnchor = Math.floor(lines.length / 2);
+    }
+
+    // Helpers
+    const indent = l => (l.match(/^\s*/)?.[0]?.length ?? 0);
+    const isBlank = l => /^\s*$/.test(l);
+    const looksLikeHeader = l =>
+      /\brecord\b|\bdata\b|\bmodule\b|\bconstructor\b/.test(l) || /:/.test(l);
+    const looksLikeClause = l =>
+      /\bwhere\b|\bwith\b|^\s*\|/.test(l) || /:=|=\s*$|→|→\s*$/.test(l);
+
+    // 1) Seed line: the one with anchor
+    let start = iAnchor, end = iAnchor;
+
+    // 2) Expand upward for headers/signatures (optional)
+    if (includeUpwardSignature) {
+      let i = iAnchor - 1;
+      while (i >= 0) {
+        const l = lines[i];
+        if (isBlank(l)) { i--; continue; }
+        if (looksLikeHeader(l) || indent(l) <= indent(lines[start])) {
+          start = i; i--;
+        } else {
+          break;
+        }
+        if (end - start + 1 >= maxLines) break;
+      }
+    }
+
+    // 3) Expand downward for continuation/clauses
+    const firstIndent = indent(lines[start]);
+    let sawContent = false;
+    for (let i = end + 1; i < lines.length; i++) {
+      const l = lines[i];
+      if (isBlank(l)) {
+        if (sawContent) { end = i - 1; break; }
+        // if blank before any content, skip it but don't count it
+        continue;
+      }
+      const ind = indent(l);
+      if (ind >= firstIndent || looksLikeClause(l)) {
+        end = i;
+        sawContent = true;
+      } else {
+        // hit a new top-level thing
+        break;
+      }
+      if (end - start + 1 >= maxLines) break;
+    }
+
+    // 4) Ensure at least minLines (extend down a bit if needed)
+    while (end - start + 1 < minLines && end + 1 < lines.length && !isBlank(lines[end + 1])) {
+      end++;
+    }
+
+    // 5) Compose block + enforce maxChars (trim softly on line boundary)
+    let blockLines = lines.slice(start, end + 1);
+    let block = blockLines.join('\n');
+    if (block.length > maxChars) {
+      // trim to nearest earlier newline before maxChars
+      const cut = block.lastIndexOf('\n', maxChars);
+      block = block.slice(0, cut > 0 ? cut : maxChars) + '\n…';
+    }
+
+    return { block, start, end, iAnchor };
+  }
+
+  function renderTooltipContent(info, snippet) {
+    const { basename, agdaClass, moduleName } = info;
+
+    const header = `<div class="agda-tip-head">
+        <span class="agda-kind">${sanitize(agdaClass)}</span>
+        <code class="agda-name">${sanitize(basename)}</code>
+        <span class="agda-module">· ${sanitize(moduleName)}</span>
+      </div>`;
+
+    const body = snippet
+      ? `<pre class="agda-tip-snippet"><code>${sanitize(snippet)}</code></pre>`
+      : `<div class="agda-tip-empty">No preview available.</div>`;
+
+    return header + body;  // ⟵ no footer
+  }
+
+  function showTooltip(evt, a, content) {
+    const el = createTooltip();
+    el.querySelector('.agda-tooltip-inner').innerHTML = content;
+    el.classList.remove('hidden');
+    positionTooltip(evt, a);
+  }
+
+  function hideTooltipSoon() {
+    if (!tooltipEl) return;
+    tooltipEl.classList.add('hidden');
+  }
+
+  async function handleEnter(evt) {
+    const a = evt.currentTarget;
+    clearTimeout(hideTimer);
+    clearTimeout(showTimer);
+
+    showTimer = setTimeout(async () => {
+      const key = a.href;
+      let data = cache.get(key);
+
+      const info = inferTokenInfo(a);
+      if (!data) {
+        // Render a fast “skeleton” immediately
+        const skeleton = renderTooltipContent(info, '');
+        showTooltip(evt, a, skeleton);
+
+        // Fetch snippet (once)
+        const { snippet } = await fetchSnippet(info.href, info.anchor);
+        data = { info, snippet };
+        cache.set(key, data);
+      }
+
+      const html = renderTooltipContent(info, data.snippet);
+      showTooltip(evt, a, html);
+    }, HOVER_DELAY_MS);
+  }
+
+  function handleLeave() {
+    clearTimeout(showTimer);
+    hideTimer = setTimeout(hideTooltipSoon, 60);
+  }
+
+  function handleMove(evt) {
+    if (!tooltipEl || tooltipEl.classList.contains('hidden')) return;
+    const a = evt.currentTarget;
+    positionTooltip(evt, a);
+  }
+
+  function wireUp() {
+    const anchors = document.querySelectorAll(HOVER_SELECTOR);
+    anchors.forEach(a => {
+      // Skip non-HTTP links
+      const href = a.getAttribute('href');
+      if (!href || href.startsWith('#') || href.startsWith('mailto:')) return;
+
+      a.addEventListener('mouseenter', handleEnter, { passive: true });
+      a.addEventListener('mouseleave', handleLeave, { passive: true });
+      a.addEventListener('mousemove', handleMove,   { passive: true });
+    });
+
+    // Keep tooltip from flickering if user hovers the tooltip itself
+    createTooltip();
+    tooltipEl.addEventListener('mouseenter', () => clearTimeout(hideTimer));
+    tooltipEl.addEventListener('mouseleave', hideTooltipSoon);
+  }
+
+  if (document.readyState === 'loading') {
+    document.addEventListener('DOMContentLoaded', wireUp);
+  } else {
+    wireUp();
+  }
+})();
diff --git a/build-tools/static/md/mkdocs/mkdocs.yml b/build-tools/static/md/mkdocs/mkdocs.yml
index e4331f2d3..bd0967a61 100644
--- a/build-tools/static/md/mkdocs/mkdocs.yml
+++ b/build-tools/static/md/mkdocs/mkdocs.yml
@@ -71,6 +71,7 @@ extra_css:
   # auto-generated by Agda fls backend (load after katex.css)
   # - css/Agda.css
   - css/custom.css
+  - css/agda-hover.css
 
 extra_javascript:
   # KaTeX JavaScript
@@ -82,6 +83,7 @@ extra_javascript:
   - AgdaKaTeX.js
   - https://cdn.jsdelivr.net/npm/chart.js
   - js/custom.js
+  - js/agda-hover.js
 
 markdown_extensions:
   - admonition                # call-out boxes like !!! note