`, every token classed + linked). The precedent is 1Lab and formal-ledger-specifications. On top sits a "chalkboard" visual identity (Direction A) for a scholarly, inviting feel. Sections: 1. Typography (Unicode-complete monospace + Fraunces display serif). 2. Agda token colours — light and dark, mirroring Agda's HTML palette. 3. Inline Agda terms (the attribute spans) in running prose. 4. Code blocks — plain fenced + agda --html highlighted/linked. 5. Landing-page hero + grid cards (base). 6. Chalkboard palette — Material colour-variable overrides per scheme. 7. Display type (Fraunces headings). 8. Hero as a chalkboard panel. 9. "By the numbers" stat strip. 10. Featured-results gallery + ink-roundel portraits. 11. Structures × properties coverage matrix. ========================================================================== */ /* -- 1. Typography --------------------------------------------------------- Agda source is saturated with mathematical Unicode — 𝓞, 𝑆, ⟨_⟩, →, ≈, ⨅, ∀, ≋ — that most monospace fonts render with tofu or inconsistent metrics. JuliaMono is purpose-built for exactly this glyph range and is the de-facto choice across the Agda/Lean/Julia ecosystems. We load it from a CDN with a broad fallback stack so the page still reads well if the font is blocked. */ @import url("https://cdn.jsdelivr.net/gh/cormullion/juliamono/webfonts/juliamono.css"); /* Display + body type are self-hosted from docs/assets/fonts/, so the site needs no external font CDN: faster first paint, renders offline, and is identical in CI screenshots. Space Grotesk is a geometric grotesque — modern, a touch technical, pairs naturally with monospace — for headings; Inter carries body text. Both are variable fonts (one file, all weights). */ @font-face { font-family: "Space Grotesk"; font-style: normal; font-display: swap; font-weight: 300 700; src: url("../assets/fonts/space-grotesk-latin-wght-normal.woff2") format("woff2"); } @font-face { font-family: "InterVar"; font-style: normal; font-display: swap; font-weight: 100 900; src: url("../assets/fonts/inter-latin-wght-normal.woff2") format("woff2"); } /* Two alternate display faces, also self-hosted, so retheming the headings is a one-word change to --ualib-display (no new download): "Geist" (Vercel's neo-grotesque, the cleanest) or "Sora" (geometric, rounder). */ @font-face { font-family: "Geist"; font-style: normal; font-display: swap; font-weight: 400; src: url("../assets/fonts/geist-sans-latin-400-normal.woff2") format("woff2"); } @font-face { font-family: "Geist"; font-style: normal; font-display: swap; font-weight: 500; src: url("../assets/fonts/geist-sans-latin-500-normal.woff2") format("woff2"); } @font-face { font-family: "Geist"; font-style: normal; font-display: swap; font-weight: 600; src: url("../assets/fonts/geist-sans-latin-600-normal.woff2") format("woff2"); } @font-face { font-family: "Geist"; font-style: normal; font-display: swap; font-weight: 700; src: url("../assets/fonts/geist-sans-latin-700-normal.woff2") format("woff2"); } @font-face { font-family: "Sora"; font-style: normal; font-display: swap; font-weight: 300 700; src: url("../assets/fonts/sora-latin-wght-normal.woff2") format("woff2"); } :root { --md-code-font: "JuliaMono", "JetBrains Mono", "Fira Code", "Cascadia Code", "DejaVu Sans Mono", "Menlo", "Consolas", monospace; --md-text-font: "InterVar", "Inter", -apple-system, BlinkMacSystemFont, "Segoe UI", "Helvetica Neue", Arial, sans-serif; /* The single display/heading family. Swap this one line to retheme every heading, the hero title + formula, the stat numbers, the figure titles, and the matrix header row. Alternatives self-hosted alongside Space Grotesk: "Geist", "Sora" (see docs/site-guide.md). */ --ualib-display: "Space Grotesk", "InterVar", "Segoe UI", system-ui, sans-serif; } /* Slightly larger line-height in code so stacked diacritics (𝒾, ≋, ⊑) and subscripts never collide; tabular figures keep alignment honest. */ .md-typeset code, .md-typeset pre > code { font-variant-ligatures: none; font-feature-settings: "ss20" 1; /* JuliaMono: dotted-zero / clearer glyphs */ } /* -- 2. Agda token colours -------------------------------------------------- The formal-ledger-specifications palette: Agda's classic vivid HTML colours in light mode, a low-saturation "zenburn"-style set in dark mode. Each rule colours BOTH the inline prose span (`.AgdaFunction`) and the agda --html code-block token (`pre.Agda .Function`). `--code-accent` is the scheme's signature colour, reused by decorative rules (the code-block rule, etc.). */ [data-md-color-scheme="default"] { --code-accent: #0000cd; .AgdaKeyword, pre.Agda .Keyword { color: #cd6600; } .AgdaComment, pre.Agda .Comment { color: #b22222; font-style: italic; } .AgdaString, pre.Agda .String { color: #b22222; } .AgdaNumber, pre.Agda .Number { color: #a020f0; } .AgdaSymbol, pre.Agda .Symbol { color: #404040; } .AgdaArgument, pre.Agda .Argument { color: #404040; } .AgdaMarkup, pre.Agda .Markup { color: #000000; } .AgdaPrimitiveType, pre.Agda .PrimitiveType { color: #0000cd; } .AgdaPrimitive, pre.Agda .Primitive { color: #0000cd; } .AgdaBound, pre.Agda .Bound { color: inherit; } .AgdaGeneralizable, pre.Agda .Generalizable { color: inherit; } .AgdaInductiveConstructor, pre.Agda .InductiveConstructor { color: #008b00; } .AgdaCoinductiveConstructor, pre.Agda .CoinductiveConstructor { color: #8b7500; } .AgdaDatatype, pre.Agda .Datatype { color: #0000cd; } .AgdaField, pre.Agda .Field { color: #ee1289; } .AgdaFunction, pre.Agda .Function { color: #0000cd; } .AgdaMacro, pre.Agda .Macro { color: #0000cd; } .AgdaModule, pre.Agda .Module { color: #a020f0; } .AgdaPostulate, pre.Agda .Postulate { color: #0000cd; } .AgdaRecord, pre.Agda .Record { color: #0000cd; } } /* Dark mode: the bespoke "Aurora Deep" palette — cool indigo ground, with orange keywords that echo the hero accent and indigo functions/modules that match the site links, so code reads as part of the Aurora theme. Two cooler alternates ("Tokyo Night", "Nord") are written out in docs/site-guide.md; swap this whole block (and §4's slate code background) to retheme. */ [data-md-color-scheme="slate"] { --code-accent: #8b88ff; .AgdaKeyword, pre.Agda .Keyword { color: #ff8a3d; } .AgdaComment, pre.Agda .Comment { color: #6b73a8; font-style: italic; } .AgdaString, pre.Agda .String { color: #c3a0ff; } .AgdaNumber, pre.Agda .Number { color: #ffb86c; } .AgdaSymbol, pre.Agda .Symbol { color: #b8c0ff; } .AgdaArgument, pre.Agda .Argument { color: #d7dcff; } .AgdaMarkup, pre.Agda .Markup { color: #d7dcff; } .AgdaPrimitiveType, pre.Agda .PrimitiveType { color: #6cc5ff; } .AgdaPrimitive, pre.Agda .Primitive { color: #6cc5ff; } .AgdaBound, pre.Agda .Bound { color: #d7dcff; } .AgdaGeneralizable, pre.Agda .Generalizable { color: #d7dcff; } .AgdaInductiveConstructor, pre.Agda .InductiveConstructor { color: #5eead4; } .AgdaCoinductiveConstructor, pre.Agda .CoinductiveConstructor { color: #5eead4; } .AgdaDatatype, pre.Agda .Datatype { color: #6cc5ff; } .AgdaField, pre.Agda .Field { color: #ff9ed6; } .AgdaFunction, pre.Agda .Function { color: #8b88ff; } .AgdaMacro, pre.Agda .Macro { color: #8b88ff; } .AgdaModule, pre.Agda .Module { color: #c3a0ff; } .AgdaPostulate, pre.Agda .Postulate { color: #8b88ff; } .AgdaRecord, pre.Agda .Record { color: #6cc5ff; } } /* -- 3. Inline Agda terms in prose ----------------------------------------- A reference like `Algebra`{.AgdaRecord} should read as a coloured mathematical name woven into the sentence — not as a boxed code chip. We therefore strip Material's inline-code background and padding for spans that carry an Agda class, leaving crisp coloured monospace. Plain inline code (no class) keeps the default chip so shell snippets still stand out. */ .md-typeset code[class*="Agda"] { background-color: transparent; padding: 0; box-shadow: none; font-weight: 480; white-space: pre-wrap; word-break: keep-all; } /* A whisper of a highlight on hover helps when scanning a dense paragraph for one identifier, without colouring the page in resting state. */ .md-typeset code[class*="Agda"]:hover { background-color: var(--md-code-bg-color); border-radius: 0.15rem; } /* -- 4. Code blocks -------------------------------------------------------- Two kinds of code blocks appear: + plain fenced ```agda blocks (the fast `make site` path, no agda --html); + agda-highlighted `

` blocks (the `make site-full` path,
       #3a) — every token semantically classed and hyperlinked to its source.
   The token COLOURS are shared with the inline spans (§2) via the same CSS
   variables; agda --html uses the bare class names (`.Function`) scoped under
   `.Agda`, whereas the prose spans carry the `Agda`-prefixed names. */
.md-typeset pre > code {
  line-height: 1.55;
}

[data-md-color-scheme="default"] {
  --md-code-bg-color: #f2f5fb;   /* cool near-white — the classic blues pop   */
  --md-code-fg-color: #2b2f36;
}
[data-md-color-scheme="slate"] {
  --md-code-bg-color: #0f1230;   /* deep indigo — the "Aurora Deep" palette   */
  --md-code-fg-color: #d7dcff;
}

/* The agda --html block itself (no inner ; children are  tokens).
   Token colours come from §2 (`pre.Agda .Function` …). */
.md-typeset pre.Agda {
  font-family: var(--md-code-font);
  font-size: 0.6rem;
  line-height: 1.6;
  background-color: var(--md-code-bg-color);
  color: var(--md-code-fg-color);
  border-radius: 0.25rem;
  border: 1px solid color-mix(in srgb, var(--code-accent) 20%, transparent);
  border-left: 3px solid var(--code-accent);
  padding: 0.8em 1em;
  margin: 1em 0;
  overflow-x: auto;
  white-space: pre;
  -webkit-overflow-scrolling: touch;
}

/* Tokens are hyperlinks: keep the token colour (not link-blue); underline only
   on hover so the click affordance is discoverable but unobtrusive. */
.md-typeset pre.Agda a {
  color: inherit;
  text-decoration: none;
}
.md-typeset pre.Agda a[href]:hover {
  text-decoration: underline;
  text-decoration-thickness: 1px;
  text-underline-offset: 0.18em;
}

/* Same restraint for inline prose spans that are also links. */
.md-typeset a code[class*="Agda"],
.md-typeset code[class*="Agda"] a {
  color: inherit;
  text-decoration: none;
}
.md-typeset a:hover code[class*="Agda"] {
  text-decoration: underline;
  text-underline-offset: 0.2em;
}

/* -- 5. Landing page -------------------------------------------------------
   A quiet hero and a grid of cards for the entry points.  Uses Material's
   built-in `.grid.cards` where possible; the hero is bespoke. */
.ualib-hero {
  text-align: center;
  padding: 2.4rem 0 1.2rem;
}
.ualib-hero h1 {
  font-weight: 800;
  font-size: 2.6rem;
  line-height: 1.1;
  margin: 0.2rem 0 0.6rem;
  letter-spacing: -0.01em;
}
.ualib-hero .ualib-tagline {
  font-size: 1.05rem;
  color: var(--md-default-fg-color--light);
  max-width: 42rem;
  margin: 0 auto 1.4rem;
}
.ualib-hero .ualib-formula {
  font-family: var(--md-code-font);
  font-size: 1.5rem;
  color: var(--code-accent);
  margin: 0.8rem 0 1.4rem;
}

/* Buttons row under the hero. */
.ualib-cta {
  display: flex;
  gap: 0.6rem;
  justify-content: center;
  flex-wrap: wrap;
  margin-bottom: 1.5rem;
}

/* Tighten Material's table rendering for the small reference tables that
   appear throughout the library (signatures, operation arities, etc.). */
.md-typeset table:not([class]) {
  font-size: 0.74rem;
}

/* Give section-index (clickable parent nav items) a subtle "overview" cue. */
.md-nav__item--section > .md-nav__link {
  font-weight: 700;
}

/* ==========================================================================
   6. Modern theme — "Aurora": an indigo→violet chrome with a vivid-orange
      accent over cool, near-white (light) / deep-navy (dark) surfaces.  We
      override Material's colour variables per scheme rather than adding a
      bespoke scheme, so the light/dark toggle keeps working.  The `--ualib-*`
      aliases drive the bespoke components (hero, stats, figures, matrix); the
      hero gradient runs from `--ualib-board-2` (violet) to `--ualib-board`
      (indigo).  Swap this whole block to retheme — two ready alternates,
      "Cobalt" (blue-led) and "Ultraviolet" (violet-led), are in
      docs/site-guide.md.  Code-block colours are owned by §4, not here.
   ========================================================================== */

[data-md-color-scheme="default"] {
  --md-default-bg-color:          #fbfcff; /* cool paper-white                */
  --md-default-bg-color--light:   #eef0fc; /* card / inset surface            */
  --md-default-fg-color:          #181c2c; /* near-navy ink                   */
  --md-default-fg-color--light:   #535d75;
  --md-default-fg-color--lighter: #818bab;
  --md-primary-fg-color:          #4f46e5; /* indigo-violet chrome (header)   */
  --md-primary-fg-color--dark:    #4338ca;
  --md-primary-fg-color--light:   #7c6cf0;
  --md-primary-bg-color:          #f3f3ff; /* text on the chrome              */
  --md-accent-fg-color:           #fb6a00; /* vivid orange (hover / accent)   */
  --md-typeset-a-color:           #5b54e6; /* indigo-violet links             */
  --md-footer-bg-color:           #20204a;

  --ualib-board:   #201f4d; /* indigo base of the hero gradient       */
  --ualib-board-2: #4a2f86; /* violet top of the hero gradient        */
  --ualib-ink:     #eef0ff; /* text on deep panels                    */
  --ualib-ink-dim: #bcc0ec;
  --ualib-rule:    #e2e4f6; /* hairline borders                       */
  --ualib-coral:   #fb6a00; /* the orange accent                      */
  --ualib-teal:    #5b54e6; /* the signature indigo (✓, stat numbers) */
}

[data-md-color-scheme="slate"] {
  --md-default-bg-color:          #0c0e1d; /* deep navy                       */
  --md-default-bg-color--light:   #15172e; /* card / inset surface            */
  --md-default-fg-color:          #c3c8de; /* soft cool grey — easier on the  */
  --md-default-fg-color--light:   #9197b6; /* eyes in a dim room than white   */
  --md-default-fg-color--lighter: #6a7197;
  --md-primary-fg-color:          #0c0d1f; /* near-black navy chrome          */
  --md-primary-fg-color--dark:    #08091a;
  --md-primary-fg-color--light:   #2a2566;
  --md-primary-bg-color:          #e8eaf8;
  --md-accent-fg-color:           #ff7a1a; /* orange                          */
  --md-typeset-a-color:           #8b88ff; /* light indigo-violet links       */
  --md-footer-bg-color:           #08091a;

  --ualib-board:   #0d0e24;
  --ualib-board-2: #2f1f6e; /* navy→violet hero in dark mode          */
  --ualib-ink:     #e8eaf8;
  --ualib-ink-dim: #9ea4cc;
  --ualib-rule:    #262a4a;
  --ualib-coral:   #ff7a1a;
  --ualib-teal:    #8b88ff;
}

/* ---- 7. Display type: Space Grotesk headings (--ualib-display) ---------- */
.md-typeset h1,
.md-typeset h2,
.md-typeset h3,
.ualib-hero h1,
.ualib-stat__num {
  font-family: var(--ualib-display), Georgia, "Times New Roman", serif;
  letter-spacing: -0.012em;
}
.md-typeset h1 { font-weight: 600; }
.md-typeset h2 { font-weight: 600; }
.md-typeset h3 { font-weight: 500; }

/* ---- 8. Hero: a chalkboard panel laid on the paper desk ----------------- */
.ualib-hero {
  position: relative;
  text-align: center;
  margin: 0.4rem 0 2.2rem;
  padding: 2.8rem 1.4rem 2.4rem;
  border-radius: 0.5rem;
  color: var(--ualib-ink);
  background:
    radial-gradient(1200px 240px at 50% -40%, rgba(255,255,255,0.05), transparent 70%),
    linear-gradient(180deg, var(--ualib-board-2), var(--ualib-board));
  box-shadow: 0 1px 0 rgba(255,255,255,0.04) inset,
              0 14px 40px -22px rgba(0,0,0,0.55);
  border: 1px solid rgba(0,0,0,0.25);
  overflow: hidden;
}
/* a faint chalk-dust wash + a wooden tray at the bottom edge */
.ualib-hero::before {
  content: ""; position: absolute; inset: 0;
  background-image:
    radial-gradient(1px 1px at 20% 30%, rgba(255,255,255,0.05) 50%, transparent 51%),
    radial-gradient(1px 1px at 70% 60%, rgba(255,255,255,0.04) 50%, transparent 51%),
    radial-gradient(1px 1px at 45% 80%, rgba(255,255,255,0.04) 50%, transparent 51%);
  background-size: 120px 120px, 160px 160px, 90px 90px;
  pointer-events: none;
}
.ualib-hero::after {
  content: ""; position: absolute; left: 0; right: 0; bottom: 0; height: 8px;
  background: linear-gradient(180deg, #8a6a45, #6e5436);
  box-shadow: 0 -1px 2px rgba(0,0,0,0.3);
}
.ualib-hero h1 {
  color: var(--ualib-ink);
  font-size: 2.7rem;
  line-height: 1.08;
  margin: 0.1rem 0 0.5rem;
}
.ualib-hero .ualib-tagline {
  color: var(--ualib-ink-dim);
  max-width: 44rem;
  margin: 0 auto 1.2rem;
  font-size: 1.04rem;
}
.ualib-hero .ualib-formula {
  font-family: var(--ualib-display), Georgia, serif;
  font-size: 2.0rem;
  letter-spacing: 0.04em;
  color: #fff;
  text-shadow: 0 0 18px rgba(255,255,255,0.25);
  margin: 0.6rem 0 1.4rem;
}
/* buttons read like chalk on the board */
.ualib-hero .md-button {
  color: var(--ualib-ink);
  border-color: rgba(244,241,232,0.6);
}
.ualib-hero .md-button--primary {
  background: var(--ualib-coral);
  border-color: var(--ualib-coral);
  color: #fff;
}
.ualib-hero .md-button:hover {
  background: var(--ualib-ink);
  border-color: var(--ualib-ink);
  color: var(--ualib-board);
}

/* ---- 9. "By the numbers" stat strip ------------------------------------- */
.ualib-stats {
  display: grid;
  grid-template-columns: repeat(4, 1fr);
  gap: 0.6rem;
  margin: 0 0 2.4rem;
  text-align: center;
}
.ualib-stat {
  padding: 0.8rem 0.4rem;
  border: 1px solid var(--ualib-rule);
  border-radius: 0.4rem;
  background: var(--md-default-bg-color--light);
}
.ualib-stat__num {
  display: block;
  font-size: 1.7rem;
  font-weight: 700;
  color: var(--ualib-teal);
  line-height: 1.1;
}
.ualib-stat__label {
  font-size: 0.72rem;
  text-transform: uppercase;
  letter-spacing: 0.08em;
  color: var(--md-default-fg-color--light);
}
@media (max-width: 44em) { .ualib-stats { grid-template-columns: repeat(2, 1fr); } }

/* ---- 10. Featured-results gallery: ink-roundel "portraits" --------------
   The roundels are placeholders (a commemorative-medallion monogram) until
   the consistent ink/line caricatures are produced; the layout is final. */
.ualib-figures {
  display: grid;
  grid-template-columns: repeat(auto-fill, minmax(15rem, 1fr));
  gap: 1rem;
  margin: 0.6rem 0 2rem;
}
.ualib-figure {
  display: flex;
  gap: 0.9rem;
  align-items: center;
  padding: 0.9rem 1rem;
  border: 1px solid var(--ualib-rule);
  border-radius: 0.5rem;
  background: var(--md-default-bg-color--light);
  transition: border-color 120ms ease, transform 120ms ease, box-shadow 120ms ease;
}
.ualib-figure:hover {
  border-color: var(--ualib-teal);
  transform: translateY(-2px);
  box-shadow: 0 10px 26px -20px rgba(0,0,0,0.5);
}
.ualib-portrait {
  flex: 0 0 auto;
  width: 74px; height: 74px;
  border-radius: 50%;
  display: grid; place-items: center;
  font-family: var(--ualib-display), serif;
  font-weight: 600; font-size: 1.5rem;
  color: var(--md-primary-fg-color);
  background: radial-gradient(circle at 50% 36%, #fff, var(--md-code-bg-color));
  border: 2px solid var(--md-primary-fg-color);
  position: relative;
}
[data-md-color-scheme="slate"] .ualib-portrait {
  color: var(--ualib-ink);
  background: radial-gradient(circle at 50% 36%, #2c3a34, #1c241e);
  border-color: var(--ualib-ink-dim);
}
/* Drop a real portrait in: replace the monogram text with
   .  The photo fills the
   medallion (the engraving ring via ::after still frames it), the grayscale
   easing to full colour on hover keeps the gallery cohesive. */
.ualib-portrait:has(img) { background: none; overflow: hidden; }
.ualib-portrait img {
  width: 100%; height: 100%;
  object-fit: cover;
  border-radius: 50%;
  display: block;
  filter: grayscale(0.35) contrast(1.02);
  transition: filter 160ms ease;
}
.ualib-figure:hover .ualib-portrait img { filter: grayscale(0); }
.ualib-portrait::after { /* engraving-style inner ring */
  content: ""; position: absolute; inset: 5px; border-radius: 50%;
  border: 1px solid color-mix(in srgb, var(--md-primary-fg-color) 35%, transparent);
}
[data-md-color-scheme="slate"] .ualib-portrait::after {
  border-color: color-mix(in srgb, var(--ualib-ink) 30%, transparent);
}
.ualib-figure__body { min-width: 0; }
.ualib-figure__result {
  display: block;                /* keep the result and the name on separate lines */
  font-family: var(--ualib-display), serif; font-weight: 600;
  font-size: 0.95rem; line-height: 1.15;
  color: var(--md-default-fg-color);
  transition: color 120ms ease;
}
.md-typeset a.ualib-figure { color: inherit; }
.md-typeset a.ualib-figure:hover { text-decoration: none; }
.md-typeset a.ualib-figure:hover .ualib-figure__result { color: var(--md-accent-fg-color); }
.ualib-figure__who {
  display: block;
  font-size: 0.74rem; color: var(--md-default-fg-color--light); margin-top: 0.15rem;
}

/* ---- 11. Structures × properties coverage matrix ------------------------ */
.ualib-matrix-wrap { overflow-x: auto; margin: 0.6rem 0 1.4rem; }
.md-typeset table.ualib-matrix {
  width: 100%;
  border-collapse: collapse;
  font-size: 0.74rem;
}
.md-typeset .ualib-matrix th,
.md-typeset .ualib-matrix td {
  border: 1px solid var(--ualib-rule);
  padding: 0.34rem 0.5rem;
  text-align: center;
  white-space: nowrap;
}
.md-typeset .ualib-matrix thead th {
  background: var(--ualib-board);
  color: var(--ualib-ink);
  font-family: var(--ualib-display), serif; font-weight: 500;
  position: sticky; top: 0;
}
.md-typeset .ualib-matrix tbody th {
  text-align: left;
  font-weight: 600;
  background: var(--md-default-bg-color--light);
}
.md-typeset .ualib-matrix tbody th a { color: var(--md-default-fg-color); }
.md-typeset .ualib-matrix tbody th a:hover { color: var(--md-accent-fg-color); }
.md-typeset .ualib-matrix .yes { color: var(--ualib-teal); font-weight: 700; }
.md-typeset .ualib-matrix .yes-2 { color: var(--ualib-coral); font-weight: 700; }
.md-typeset .ualib-matrix tbody tr:hover td,
.md-typeset .ualib-matrix tbody tr:hover th { background: color-mix(in srgb, var(--ualib-teal) 8%, transparent); }

/* ---- 12. Module-dependency constellation -------------------------------- */
#constellation {
  position: relative;
  height: 640px;
  border-radius: 0.5rem;
  background: radial-gradient(1100px 520px at 50% -10%, #1d2c25, #10150e 75%);
  border: 1px solid #2a352e;
  box-shadow: inset 0 1px 0 rgba(255, 255, 255, 0.03);
  margin: 0.6rem 0 0.8rem;
  overflow: hidden;
  touch-action: none;
}
.constellation-readout {
  position: absolute; left: 14px; bottom: 14px;
  pointer-events: none; opacity: 0; transition: opacity 120ms ease;
  background: rgba(8, 12, 9, 0.74);
  border: 1px solid #34423a; border-radius: 0.35rem;
  padding: 0.45rem 0.7rem; max-width: 72%;
}
.constellation-readout b {
  display: block; color: #eef2ee; font-size: 0.92rem; font-weight: 600;
  font-family: var(--md-code-font);
}
.constellation-readout span { color: #9fb3a8; font-size: 0.72rem; }
.constellation-legend {
  display: flex; flex-wrap: wrap; gap: 0.4rem 1rem;
  font-size: 0.74rem; margin: 0.5rem 0 0.3rem;
  color: var(--md-default-fg-color--light);
}
.constellation-legend span { display: inline-flex; align-items: center; gap: 0.35rem; }
.constellation-legend i { width: 0.7rem; height: 0.7rem; border-radius: 50%; display: inline-block; }
.constellation-note { font-size: 0.78rem; color: var(--md-default-fg-color--light); margin-top: 0.4rem; }

/* ==========================================================================
   13. Modern overrides — retire the chalkboard skeuomorphism (wooden tray,
       chalk dust, serif glow) for a sleek, "from the future" surface; blend
       the admonition blocks into the card system; and style the copy button
       that agda-copy.js adds to highlighted `` blocks.
       Appended last so these win over §§8–11 without rewriting them.
   ========================================================================== */

/* -- Hero: a deep-indigo glass panel, lit from above ---------------------- */
.ualib-hero {
  border-radius: 0.9rem;
  background:
    radial-gradient(820px 280px at 50% -25%,
      color-mix(in srgb, var(--ualib-coral) 22%, transparent), transparent 70%),
    radial-gradient(900px 360px at 50% 120%,
      color-mix(in srgb, var(--md-primary-fg-color--light) 35%, transparent), transparent 72%),
    linear-gradient(135deg, var(--ualib-board-2), var(--ualib-board));
  border: 1px solid color-mix(in srgb, var(--ualib-ink) 12%, transparent);
  box-shadow: 0 1px 0 rgba(255, 255, 255, 0.06) inset,
              0 30px 60px -34px rgba(8, 12, 36, 0.7);
}
.ualib-hero::before {            /* a single soft top sheen, not chalk dust  */
  background: radial-gradient(60% 40% at 50% 0%,
    rgba(255, 255, 255, 0.08), transparent 70%);
  background-size: auto;
}
.ualib-hero::after {             /* an accent hairline, not a wooden tray    */
  height: 2px;
  background: linear-gradient(90deg, transparent,
    var(--ualib-coral) 25%, var(--md-primary-fg-color--light) 75%, transparent);
  box-shadow: none;
}
.ualib-hero h1 {
  letter-spacing: -0.022em;
  font-weight: 600;
}
.ualib-hero .ualib-formula {     /* the theorem, glowing in the accent       */
  font-family: var(--md-code-font);
  color: #fff;
  text-shadow: 0 0 26px color-mix(in srgb, var(--ualib-coral) 55%, transparent);
}

/* -- Cards: one rounded radius across stats, figures, admonitions ---------- */
.ualib-stat,
.ualib-figure { border-radius: 0.7rem; }

/* -- Admonitions: make a `!!! note` read as one of the site's cards, not a
      boxy callout.  The `!important`s override Material's per-type rules (which
      out-specify a plain `.admonition` selector); the accent is the signature
      indigo (`--ualib-teal`), vivid in both light and dark. ----------------- */
.md-typeset .admonition,
.md-typeset details {
  border: 1px solid var(--ualib-rule) !important;
  border-left: 0.2rem solid var(--ualib-teal) !important;
  border-radius: 0.7rem;
  background: var(--md-default-bg-color--light) !important;
  box-shadow: 0 10px 28px -22px rgba(8, 12, 36, 0.55);
  font-size: 0.78rem;
}
.md-typeset .admonition-title,
.md-typeset summary {
  background: color-mix(in srgb, var(--ualib-teal) 10%, transparent) !important;
  font-family: var(--ualib-display);
  font-weight: 600;
  letter-spacing: -0.004em;
}
.md-typeset .admonition-title::before,
.md-typeset summary::before {
  background-color: var(--ualib-teal) !important;
}

/* -- Copy button on highlighted Agda blocks (added by agda-copy.js) -------
   Material's content.code.copy only reaches its own `.highlight` blocks; the
   agda --html output is a bare ``, so we add our own.  The
   button is quiet until the block is hovered or keyboard-focused. */
.ualib-agda-copy {
  position: absolute; top: 0.4rem; right: 0.4rem;
  width: 1.6em; height: 1.6em; padding: 0;
  display: grid; place-items: center;
  border: 1px solid var(--ualib-rule); border-radius: 0.35rem;
  background: color-mix(in srgb, var(--md-code-bg-color) 78%, transparent);
  color: var(--md-default-fg-color--light);
  cursor: pointer; opacity: 0;
  transition: opacity 140ms ease, color 140ms ease, border-color 140ms ease;
}
.md-typeset pre.Agda:hover .ualib-agda-copy,
.ualib-agda-copy:focus-visible { opacity: 1; }
.ualib-agda-copy:hover { color: var(--md-accent-fg-color); border-color: var(--md-accent-fg-color); }
.ualib-agda-copy svg { width: 0.95em; height: 0.95em; }
.ualib-agda-copy.ualib-copied { color: var(--ualib-teal); border-color: var(--ualib-teal); }

/* ==========================================================================
   14. Featured-results carousel — one card in focus, auto-advancing every few
       seconds, with clickable dots (docs/assets/js/carousel.js).  With JS off
       it degrades to a horizontal row of cards; autoplay yields to
       prefers-reduced-motion.
   ========================================================================== */
/* Cards-per-view scales with width: 1 on a phone, 2 on a tablet, 3 on a wide
   monitor.  carousel.js reads `--per`, sizes the slide step from the measured
   card width + gap, and clones the leading cards for a seamless wrap. */
.ualib-carousel {
  --per: 1; --gap: 1rem;
  position: relative; max-width: 1120px; margin: 0.5rem auto 0;
}
@media (min-width: 720px)  { .ualib-carousel { --per: 2; } }
@media (min-width: 1024px) { .ualib-carousel { --per: 3; } }
.ualib-carousel__viewport { overflow: hidden; }
.ualib-carousel__track {
  display: flex; gap: var(--gap);
  will-change: transform;       /* the transform + its transition are set by JS */
}
.md-typeset .ualib-carousel .ualib-figure {
  flex: 0 0 calc((100% - (var(--per) - 1) * var(--gap)) / var(--per));
  box-sizing: border-box;
  margin: 0; min-height: 7.4rem; padding: 1.1rem 1.3rem;
}
.ualib-carousel .ualib-portrait { width: 76px; height: 76px; }
.ualib-carousel .ualib-figure__result { font-size: 1.05rem; }
.ualib-carousel .ualib-figure.is-clone { pointer-events: none; }

/* Deliberately understated: tiny dots, a muted resting colour, and a small
   accent mark for the current card (no scale jump, no large bright dot). */
.ualib-carousel__dots {
  display: flex; justify-content: center; gap: 0.42rem; margin-top: 0.9rem;
}
.ualib-carousel__dot {
  width: 0.36rem; height: 0.36rem; padding: 0;
  border: 0; border-radius: 50%;
  background: color-mix(in srgb, var(--md-default-fg-color--light) 38%, transparent);
  cursor: pointer;
  transition: background 0.2s ease;
}
.ualib-carousel__dot:hover { background: var(--md-default-fg-color--light); }
.ualib-carousel__dot.is-active { background: var(--ualib-coral); }
.ualib-carousel__dot:focus-visible {
  outline: 1px solid var(--ualib-teal); outline-offset: 2px;
}
@media (prefers-reduced-motion: reduce) {
  .ualib-carousel__track { transition: none; }
}

/* ==========================================================================
   15. "Show more Agda" toggle (#431, M10-5) — module sources wrap their
       leading OPTIONS/module/import scaffolding in HTML comments, and
       mkdocs_gen_library.py re-surfaces those blocks tagged `hidden-source`:
       `` on the highlighted path, a fenced block inside a
       `` on the plain path.  They stay hidden until
       docs/assets/js/agda-toggle.js flips `reveal-agda-source` on  — a
       global choice persisted in localStorage, like the palette toggle.
   ========================================================================== */
.md-typeset pre.Agda.hidden-source,
.md-typeset div.hidden-source {
  display: none;
}
body.reveal-agda-source .md-typeset pre.Agda.hidden-source,
body.reveal-agda-source .md-typeset div.hidden-source {
  display: block;
}

/* Click-to-definition must keep working while the scaffolding is hidden:
   agda --html links every token to its defining occurrence, and the binders
   introduced by `private variable` (and header renamings) live inside the
   hidden block.  When the URL fragment targets an anchor in a hidden block,
   reveal that block so the browser can scroll to it. */
.md-typeset pre.Agda.hidden-source:has(:target),
.md-typeset div.hidden-source:has(:target) {
  display: block;
}

/* A block revealed locally via its inline `▸ hidden code (n lines)` note
   (agda-toggle.js), independently of the global toggle. */
.md-typeset pre.Agda.hidden-source.revealed,
.md-typeset div.hidden-source.revealed {
  display: block;
}

/* The inline note itself: quiet and small, sitting where the hidden block
   would be, so a page never looks silently truncated.  Redundant while the
   global toggle already reveals everything, so hide it then. */
.md-typeset .ualib-hidden-note {
  display: block;
  margin: 0.6em 0;
  padding: 0;
  border: 0;
  background: none;
  color: var(--md-default-fg-color--light);
  font-family: var(--md-code-font);
  font-size: 0.6rem;
  cursor: pointer;
}
.md-typeset .ualib-hidden-note:hover {
  color: var(--md-accent-fg-color);
}
body.reveal-agda-source .md-typeset .ualib-hidden-note {
  display: none;
}

/* -- Shared header switch (agda-toggle.js "Show all Agda", agda-hover.js
      "Tooltips") -----------------------------------------------------------
   A sliding toggle: a static label + icon, then a track whose thumb slides
   right and turns lime when the feature is on.  `role="switch"` + aria-checked
   carry the state (the label is the accessible name).  `currentColor` is the
   header foreground, so the muted "off" track reads on the indigo/navy chrome
   in both schemes; only the lit colour is a bespoke token. */
:root { --ualib-switch-on: #84cc16; }                          /* vivid lime  */
[data-md-color-scheme="slate"] { --ualib-switch-on: #a3e635; } /* brighter    */

.ualib-switch {
  display: inline-flex;
  align-items: center;
  gap: 0.5em;
  flex-shrink: 0;
  padding: 0.2em 0.4em;
  border: 0;
  background: none;
  color: inherit;
  font-family: var(--ualib-display);
  font-size: 0.66rem;
  font-weight: 500;
  line-height: 1.2;
  white-space: nowrap;
  cursor: pointer;
}
.ualib-switch__label {
  display: inline-flex;
  align-items: center;
  gap: 0.35em;
}
.ualib-switch__track {
  position: relative;
  flex-shrink: 0;
  width: 1.85em;
  height: 1.02em;
  border-radius: 999px;
  background: color-mix(in srgb, currentColor 24%, transparent);
  transition: background 160ms ease;
}
.ualib-switch__thumb {
  position: absolute;
  top: 50%;
  left: 0.13em;
  width: 0.76em;
  height: 0.76em;
  border-radius: 50%;
  background: #fff;
  box-shadow: 0 1px 2px rgba(0, 0, 0, 0.35);
  transform: translateY(-50%);
  transition: transform 160ms ease;
}
.ualib-switch[aria-checked="true"] .ualib-switch__track {
  background: var(--ualib-switch-on);
}
.ualib-switch[aria-checked="true"] .ualib-switch__thumb {
  transform: translate(0.83em, -50%);
}
.ualib-switch:hover .ualib-switch__track {
  background: color-mix(in srgb, currentColor 36%, transparent);
}
.ualib-switch[aria-checked="true"]:hover .ualib-switch__track {
  background: color-mix(in srgb, var(--ualib-switch-on) 84%, #ffffff);
}
.ualib-switch:focus-visible {
  outline: 1px solid currentColor;
  outline-offset: 3px;
  border-radius: 4px;
}
.agda-logo-icon { width: 1.15em; height: 1.15em; }
.agda-tip-icon  { width: 1.05em; height: 1.05em; }

/* On narrow headers (hamburger + title + palette + search) an unshrinkable
   control would crush the page title, so drop both switches below the same
   breakpoint at which Material hides its repo-source chrome.  Phones keep the
   defaults, which is the right reading mode there anyway. */
@media screen and (max-width: 59.9844em) {
  .ualib-switch {
    display: none;
  }
}

/* ==========================================================================
   16. Type-on-hover tooltips (#429, M10-3) — docs/assets/js/agda-hover.js pairs
       each linked Agda token with the `` at its definition and,
       on hover, shows a small popover with a snippet of that definition.  A
       "Tooltips" switch (a sibling of the Show-all-Agda control) lets a reader
       switch them off; the choice persists in localStorage.  Colours ride the
       theme tokens so the popover matches the page in both schemes, and the
       snippet reuses the code surface.
   ========================================================================== */
:root {
  --agda-tip-font:   0.72rem;             /* compact body text                */
  --agda-tip-code:   0.70rem;             /* compact code                     */
  --agda-tip-width:  min(34rem, 90vw);    /* max popover width                */
  --agda-tip-ch:     68ch;                /* max code line width              */
  --agda-tip-shadow: 0 6px 16px rgba(0, 0, 0, 0.14), 0 2px 6px rgba(0, 0, 0, 0.10);
}
[data-md-color-scheme="slate"] {
  --agda-tip-shadow: 0 6px 16px rgba(0, 0, 0, 0.35), 0 2px 6px rgba(0, 0, 0, 0.28);
}
/* The colour tokens (`--md-default-bg-color`, `--md-code-bg-color`, …) are set
   on  by the palette — `data-md-color-scheme` lives there, not on :root —
   so the popover reads them *directly* in the rules below.  Resolving them into
   an `--agda-tip-*` alias at :root would freeze the light-scheme values and the
   tooltip would stay pale in dark mode. */

/* -- The popover ---------------------------------------------------------- */
/* Page-absolute (agda-hover.js folds in the scroll offset); purely
   informational, so it never takes pointer or focus. */
.agda-tooltip {
  position: absolute;
  z-index: 2000;
  max-width: var(--agda-tip-width);
  background: var(--md-default-bg-color);
  color: var(--md-default-fg-color);
  border: 1px solid color-mix(in srgb, var(--md-default-fg-color) 16%, transparent);
  border-radius: 0.4rem;
  box-shadow: var(--agda-tip-shadow);
  opacity: 1;
  pointer-events: none;
}
.agda-tooltip.hidden {
  opacity: 0;
  visibility: hidden;   /* also drop it from hit-testing + the a11y tree */
}
.agda-tooltip .agda-tooltip-inner {
  padding: 0.4rem 0.5rem;
  font-size: var(--agda-tip-font);
  line-height: 1.4;
}

/* -- Header line: kind · name · module ------------------------------------ */
.agda-tip-head {
  display: flex;
  align-items: baseline;
  gap: 0.34rem;
  margin-bottom: 0.16rem;
  font-weight: 600;
}
.agda-kind {
  font-size: calc(var(--agda-tip-font) - 0.06rem);
  letter-spacing: 0.04em;
  text-transform: uppercase;
  opacity: 0.72;
}
.agda-name {
  font-family: var(--md-code-font);
  font-size: calc(var(--agda-tip-font) - 0.01rem);
  font-weight: 700;
  color: inherit;
}
.agda-module {
  margin-left: auto;
  font-size: calc(var(--agda-tip-font) - 0.08rem);
  opacity: 0.6;
}

/* -- The definition snippet ----------------------------------------------- */
/* The snippet is cloned from the target page's tokens and carries `class="Agda"`
   too, so the token-colour rules (`[data-md-color-scheme] pre.Agda .Function`, …)
   reach it and the preview keeps Agda's highlighting.  The code-block *layout*
   rules are scoped to `.md-typeset pre.Agda`, which the tooltip is outside of,
   so only the compact styling here applies; `white-space: pre` keeps Agda's
   spacing. */
.agda-tip-snippet {
  margin: 0.12rem 0 0 0;
  padding: 0.32rem 0.42rem;
  border-radius: 0.3rem;
  background: var(--md-code-bg-color);
  font-family: var(--md-code-font);
  font-size: var(--agda-tip-code);
  line-height: 1.5;
  white-space: pre;
  max-width: var(--agda-tip-ch);
  overflow-x: auto;    /* long types scroll rather than wrap or clip */
  overflow-y: hidden;
}
/* Cloned tokens are  elements; keep their kind colour (the token rules win on
   specificity) but drop the link chrome — the site's `pre.Agda a` reset is
   `.md-typeset`-scoped and does not reach here. */
.agda-tip-snippet a {
  color: inherit;
  text-decoration: none;
  cursor: inherit;
}
.agda-tip-empty {
  margin: 0.14rem 0 0 0;
  font-size: calc(var(--agda-tip-font) - 0.04rem);
  opacity: 0.85;
}
.agda-tip-loading {
  font-style: italic;
  opacity: 0.6;
}

/* The header "Tooltips" control is the shared `.ualib-switch` (styled with the
   Show-all-Agda control in §15); agda-hover.js only sets its aria-checked. */