/* Outcrop site styles.
 *
 * The colour palette and the Agda syntax-token colours are adapted from the 1lab
 * (https://1lab.dev), which is licensed AGPL-3.0; this file is therefore likewise
 * AGPL-3.0. The reusable page layout is Outcrop's own. See NOTICE.
 */

/* All web fonts self-hosted (see resources/static/fonts/, all OFL-1.1): EB Garamond (body serif),
   Inria Sans (UI sans), JuliaMono (code) -- matching 1lab's typefaces, but with no runtime
   dependency on Google Fonts (which can be blocked or slow). CJK falls back to the system
   rounded font (see --cjk-font). URLs are relative to this stylesheet, so they work under
   any deploy base path. */
@font-face { font-family: "EB Garamond"; font-display: swap; font-weight: 400; font-style: normal;
  src: url("fonts/eb-garamond-latin-400-normal.woff2") format("woff2"); }
@font-face { font-family: "EB Garamond"; font-display: swap; font-weight: 400; font-style: italic;
  src: url("fonts/eb-garamond-latin-400-italic.woff2") format("woff2"); }
@font-face { font-family: "EB Garamond"; font-display: swap; font-weight: 600; font-style: normal;
  src: url("fonts/eb-garamond-latin-600-normal.woff2") format("woff2"); }
@font-face { font-family: "EB Garamond"; font-display: swap; font-weight: 700; font-style: normal;
  src: url("fonts/eb-garamond-latin-700-normal.woff2") format("woff2"); }
@font-face { font-family: "Inria Sans"; font-display: swap; font-weight: 400; font-style: normal;
  src: url("fonts/inria-sans-latin-400-normal.woff2") format("woff2"); }
@font-face { font-family: "Inria Sans"; font-display: swap; font-weight: 700; font-style: normal;
  src: url("fonts/inria-sans-latin-700-normal.woff2") format("woff2"); }
@font-face { font-family: "JuliaMono"; font-display: swap; font-weight: 400; font-style: normal;
  src: url("fonts/JuliaMono-Regular.woff2") format("woff2"); }
@font-face { font-family: "JuliaMono"; font-display: swap; font-weight: 700; font-style: normal;
  src: url("fonts/JuliaMono-Bold.woff2") format("woff2"); }
@font-face { font-family: "Bedrock Dotted Operators"; font-display: swap;
  src: url("fonts/BedrockDottedOperators-Regular.woff2") format("woff2"); }
/* Exact grapheme spans only: never replace plain ⇒/¬ or other combining dots. */
.dotted-operator { font-family: "Bedrock Dotted Operators", var(--mono);
  white-space: nowrap; }

:root {
  --text-bg: #fff;       --text-fg: #222;       --fg-alt: #475569;
  --primary: #0054F4;    --ruler: #94A3B8;      --highlight: #F5DEB3;
  /* Blue-violet navigation stays distinct from Agda's blue definitions. */
  --link-color: #7244b7;
  --code-bg: #f3f5f8;    --code-inline-bg: #e9edf3; --code-fg: #1f2937;
  --code-border: #d7dde7;
  --code-symbol: #86652e;
  --code-comment: #6a737d; --code-keyword: #BB3B13; --code-string: #d52753;
  --code-number: #8A1060;  --code-module: #8A1060;  --code-field: #9C1BD6;
  --code-macro: #0054F4;   --code-constructor: #207B1D; --code-identifier: #0054F4;
  --popup-bg: #fff;        --banner-bg: #FEF3C7;    --banner-fg: #92400E;
  --button-hover: #e5e7eb; --input-border: #cbd5e1;
  --occ-bg: #F5DEB3;       /* same-definition occurrence highlight */
  --ast-node-lightness: 56%; --ast-node-chroma: .17;
  /* CJK glyphs fall through to a rounded system sans (PingFang on macOS). Latin uses the
     fonts before it (EB Garamond / Inria Sans) via per-glyph fallback. ja is overridden
     below to prefer Hiragino. */
  --cjk-font: "PingFang SC", "PingFang TC", "Hiragino Sans GB", "Microsoft YaHei",
              "Noto Sans CJK SC", sans-serif;
  --serif: "EB Garamond", Georgia, "Times New Roman", var(--cjk-font);
  --sans: "Inria Sans", -apple-system, BlinkMacSystemFont, "Segoe UI", var(--cjk-font);
  --mono: "JuliaMono", "Cascadia Code", "JetBrains Mono", "Fira Code", ui-monospace,
          "SF Mono", Menlo, Consolas, monospace;
  --font-size: 1.3rem;                      /* 1lab's default (sans-serif mode) body size */
  --code-font-size: calc(0.92 * var(--font-size));
  --reading-width: 48rem;
  --reading-done-color: #207b1d;
  --reviewed-color: #24784f;
  --unreviewed-color: #9b6519;
  --content-frame-radius: 8px;
}

html[lang="zh"] { --reading-width: 52rem; }

/* Japanese prefers Hiragino (Mac) over PingFang to avoid Han-unification glyph mismatch. */
html[lang="ja"] {
  --reading-width: 50rem;
  --cjk-font: "Hiragino Sans", "Hiragino Kaku Gothic ProN", "Yu Gothic",
              "Noto Sans CJK JP", sans-serif;
}

:root.theme-dark, html.theme-dark {
  --text-bg: #171a21;    --text-fg: #d6dbe5;    --fg-alt: #aeb8c8;
  --primary: #119DDB;    --ruler: #475569;      --highlight: #EF444499;
  --link-color: #ba8bea;
  --code-bg: #232936;    --code-inline-bg: #2a3240; --code-fg: #e6edf3;
  --code-border: #3b4658;
  --code-symbol: #e4c88b;
  --code-comment: #aab4c6; --code-keyword: #ffb454; --code-string: #f58ca6;
  --code-number: #c8a0ff;  --code-module: #d0a8ff;  --code-field: #ff8cc8;
  --code-macro: #e6c96f;   --code-constructor: #65d6ad; --code-identifier: #7dcfff;
  --popup-bg: #1B1E24;     --banner-bg: #3f2d12;    --banner-fg: #FCD34D;
  --button-hover: #3B4454; --input-border: #475569;
  --occ-bg: #EAD16E2E;     /* same-definition occurrence highlight */
  --ast-node-lightness: 76%; --ast-node-chroma: .14;
  --reading-done-color: #2fcb8f;
  --reviewed-color: #65c99d;
  --unreviewed-color: #e6b667;
}
@media (prefers-color-scheme: dark) {
  :root:not(.theme-light) {
    --text-bg: #171a21;    --text-fg: #d6dbe5;    --fg-alt: #aeb8c8;
    --primary: #119DDB;    --ruler: #475569;      --highlight: #EF444499;
    --link-color: #ba8bea;
    --code-bg: #232936;    --code-inline-bg: #2a3240; --code-fg: #e6edf3;
    --code-border: #3b4658;
    --code-symbol: #e4c88b;
    --code-comment: #aab4c6; --code-keyword: #ffb454; --code-string: #f58ca6;
    --code-number: #c8a0ff;  --code-module: #d0a8ff;  --code-field: #ff8cc8;
    --code-macro: #e6c96f;   --code-constructor: #65d6ad; --code-identifier: #7dcfff;
    --popup-bg: #1B1E24;     --banner-bg: #3f2d12;    --banner-fg: #FCD34D;
    --button-hover: #3B4454; --input-border: #475569;
    --occ-bg: #EAD16E2E;     /* same-definition occurrence highlight */
    --ast-node-lightness: 76%; --ast-node-chroma: .14;
    --reading-done-color: #2fcb8f;
    --reviewed-color: #65c99d;
    --unreviewed-color: #e6b667;
  }
}

* { box-sizing: border-box; }
html { scroll-padding-top: var(--anchor-inset, calc(var(--site-header-height, 3.5rem) + var(--section-nav-height, 0px) + 1rem)); }
/* Base rem = browser default (16px), so 1.4rem matches 1lab's body size exactly. */
/* Prose font: Inria Sans (sans-serif), matching 1lab's default. (1lab also ships EB Garamond
   for an optional "Serif" toggle; we keep the @font-face above but default to sans like 1lab.) */
body {
  margin: 0; background: var(--text-bg); color: var(--text-fg);
  font-family: var(--sans); font-size: var(--font-size); line-height: 1.5;
}
body.nav-layout-changing { overflow-anchor: none; }
.scroll-anchor-marker { display: inline-block; width: 0; height: 1em;
  margin: 0; padding: 0; border: 0; vertical-align: baseline; pointer-events: none; }

/* ---- top bar ---- */
/* Banner (if any) + topbar pin to the top together; the external warning stays on scroll. */
#site-header { position: sticky; top: 0; z-index: 50; background: var(--text-bg); }
#topbar {
  display: flex; align-items: center; gap: 0.75rem;
  padding: 0.5rem 1rem; background: var(--text-bg);
}
#brand { display: inline-flex; align-items: center; gap: 0.45rem;
         font-family: var(--sans); font-weight: 700; font-size: 1.2rem;
         color: var(--primary); text-decoration: none; }
/* The favicon SVG has only a viewBox (no intrinsic size), so size it explicitly. */
.brand-logo { height: 1.5rem; width: 1.5rem; display: block; flex: none; }
.topbar-spacer { flex: 1; }
.search-form { position: relative; }
#search-box {
  font-family: var(--sans); font-size: 0.95rem; padding: 0.3rem 0.6rem;
  border: 1px solid var(--input-border); border-radius: 6px;
  background: var(--text-bg); color: var(--text-fg); width: 14rem; max-width: 40vw;
}
#search-results {
  position: absolute; right: 0; top: 2.2rem; width: 28rem; max-width: 80vw;
  max-height: 60vh; overflow-y: auto; background: var(--popup-bg);
  border: 1px solid var(--input-border); border-radius: 8px;
  box-shadow: 0 8px 24px rgba(0,0,0,.18); padding: 0.25rem;
}
#search-results .res { display: block; padding: 0.35rem 0.5rem; border-radius: 6px;
  text-decoration: none; color: var(--text-fg); font-family: var(--sans); font-size: 0.9rem; }
#search-results .res:hover, #search-results .res.sel { background: var(--button-hover); }
#search-results .res .nm { font-family: var(--mono); color: var(--link-color); }
#search-results .res .mod { color: var(--fg-alt); font-size: 0.8rem; }
#search-results .res .ty { font-family: var(--mono); color: var(--fg-alt); font-size: 0.8rem; }
#search-results .res { min-height: 44px; overflow-wrap: anywhere; }
#search-results .res :is(.nm, .mod, .ty) { display: block; }
#search-results .res .ty { display: -webkit-box; -webkit-line-clamp: 2; -webkit-box-orient: vertical; overflow: hidden; }
#search-results .search-message { padding: .75rem; margin: 0; color: var(--text-fg); font: inherit; }
#search-results button.search-message { width: 100%; background: var(--text-bg); border: 0; cursor: pointer; text-align: left; }
#lang-switch { font-family: var(--sans); font-size: 0.9rem; }
#lang-switch a { color: var(--fg-alt); text-decoration: none; }
#lang-switch a:hover { text-decoration: underline; }
#lang-switch .cur { font-weight: 700; color: var(--text-fg); }
#theme-toggle { font-size: 1.1rem; background: none; border: none; cursor: pointer;
  color: var(--text-fg); padding: 0.2rem 0.4rem; border-radius: 6px; }
#theme-toggle:hover { background: var(--button-hover); }
/* Keep the hamburger in one stable place so it can both open and close navigation. */
#nav-toggle { display: inline-flex; align-items: center; justify-content: center;
  min-width: 2rem; min-height: 2rem; font-size: 1.3rem; line-height: 1; background: none; border: none;
  cursor: pointer; color: var(--text-fg); padding: 0.2rem 0.45rem; border-radius: 6px;
  margin-left: -0.25rem; }
#nav-toggle:hover { background: var(--button-hover); }
#toc-drawer-head { display: none; align-items: center; justify-content: space-between;
  margin-bottom: 0.5rem; }
#toc-drawer-head .drawer-title { font-family: var(--sans); font-weight: 700; font-size: 0.8rem;
  text-transform: uppercase; letter-spacing: 0.05em; color: var(--fg-alt); }
#toc-collapse { display: none; align-items: center; justify-content: center; float: right;
  min-width: 2rem; min-height: 2rem; margin: .1rem .2rem .35rem .4rem;
  border: 0; border-radius: 6px; color: var(--fg-alt); background: transparent;
  font: 1rem/1 var(--sans); cursor: pointer; }
#toc-collapse:hover { color: var(--primary); background: var(--button-hover); }
#nav-close { font-size: 1.1rem; line-height: 1; background: none; border: none; cursor: pointer;
  color: var(--text-fg); padding: 0.2rem 0.45rem; border-radius: 6px; }
#nav-close:hover { background: var(--button-hover); }
#nav-backdrop { display: none; }

/* ---- layout (the reading column stays centered at every viewport width) ---- */
main { max-width: 80rem; width: 100%; margin: 0 auto; padding: 0 1rem; box-sizing: border-box; }
#post-toc-container {
  display: grid; gap: 1.5rem 2.5rem; align-items: start;
  grid-template-columns: minmax(0, 1fr);
  grid-template-areas: "content";
}
article { position: relative; grid-area: content; width: 100%; max-width: var(--reading-width); justify-self: center; }
#sidenote-container { grid-area: gutter; display: none; }

/* 80rem fits the widest reading column (52rem), two 10rem side tracks,
   two 2.5rem gaps and 2rem outer padding. Let the tracks grow continuously
   instead of hiding a sidebar that still fits a scaled laptop viewport.
   Keep this breakpoint synchronized with reader/navigation.js. */
@media (min-width: 80rem) {
  main { max-width: 100%; }
  #post-toc-container {
    grid-template-columns: minmax(10rem, 1fr) minmax(0, var(--reading-width)) minmax(10rem, 1fr);
    grid-template-areas: "sidebar content gutter";
  }
  #sidenote-container { display: block; }
}

#toc { grid-area: sidebar; position: sticky; top: calc(var(--site-header-height, 3.5rem) + .5rem);
  width: 100%; max-width: 20rem; justify-self: start; font-family: var(--sans);
  font-size: .85rem; max-height: calc(100dvh - var(--site-header-height, 3.5rem) - 1rem); overflow-y: auto;
  scrollbar-width: thin; scrollbar-color: var(--input-border) transparent; }
#toc-container { padding: .25rem .65rem .75rem .1rem; }
details.navsec { padding-block: .65rem; border-bottom: 1px solid var(--ruler); }
details.navsec:first-child { padding-top: 0; }
details.navsec:last-child { border-bottom: 0; }
.nav-title { color: var(--text-fg); font-size: .8rem; font-weight: 650; line-height: 1.5;
  margin: 0; text-transform: none; letter-spacing: .015em; }
#toc summary { display: flex; align-items: center; gap: .55rem; list-style: none;
  cursor: pointer; padding: .6rem .5rem; border-radius: 6px; }
#toc summary::-webkit-details-marker { display: none; }
#toc summary::after { content: ""; flex: 0 0 .35rem; height: .35rem; margin-left: auto;
  border-right: 1.5px solid currentColor; border-bottom: 1.5px solid currentColor;
  transform: rotate(45deg) translateY(-2px); transition: transform .15s ease; opacity: .65; }
#toc details[open] > summary::after { transform: rotate(225deg) translate(-1px, -1px); }
#toc summary:hover, #toc a:hover { background: color-mix(in srgb, var(--primary) 7%, transparent);
  color: var(--primary); }
#toc a:hover { color: var(--link-color); }
#toc ul { list-style: none; margin: .2rem 0; padding: 0; }
#toc .navsec > ul { margin-left: .65rem; padding-left: .4rem;
  border-left: 1px solid var(--ruler); }
#toc li { margin: .12rem 0; }
#toc a { display: block; padding: .48rem .55rem; border-radius: 5px;
  font-size: .8rem; line-height: 1.5; color: var(--fg-alt); text-decoration: none;
  overflow-wrap: anywhere; transition: background-color .15s ease, color .15s ease; }
#toc .current-route > summary { gap: .35rem; }
#toc .current-route-name { min-width: 0; overflow: hidden;
  color: var(--fg-alt); font-size: .72rem; font-weight: 500; text-overflow: ellipsis;
  white-space: nowrap; }
#toc .route-nav li { display: flex; align-items: stretch; border-radius: 5px; }
#toc .route-nav li:has(> a[aria-current]) { background: color-mix(in srgb, var(--primary) 10%, transparent);
  box-shadow: inset 2px 0 var(--primary); }
#toc .route-nav a { display: flex; flex: 1 1 auto; align-items: center; min-width: 0; padding-inline-end: .3rem; }
#toc .route-nav a[aria-current] { background: none; box-shadow: none; }
#toc .route-chapter-viewport { display: block; flex: 1; min-width: 0; overflow: hidden; }
#toc .route-chapter-title { display: inline-block; white-space: nowrap; }
#toc .route-nav a.is-title-overflowing .route-chapter-title {
  animation: route-title-pan var(--route-title-duration, 8s) ease-in-out infinite; }
@keyframes route-title-pan {
  0%, 12%, 100% { transform: translateX(0); }
  50%, 62% { transform: translateX(calc(0px - var(--route-title-overflow, 0px))); }
}
@media (prefers-reduced-motion: reduce) {
  #toc .route-nav a.is-title-overflowing .route-chapter-title { animation: none; }
}
@media (hover: hover) and (pointer: fine) {
  #toc .route-nav a.is-title-overflowing { position: relative; }
  #toc .route-nav a.is-title-overflowing::after {
    content: attr(data-full-title); position: absolute; z-index: 12;
    inset-block-start: calc(100% + .2rem); inset-inline-start: 0;
    width: max-content; max-width: calc(100% + 2.4rem); padding: .35rem .5rem;
    border: 1px solid var(--code-border); border-radius: 6px;
    color: var(--text-fg); background: var(--popup-bg); box-shadow: 0 4px 14px #0002;
    font: .7rem/1.35 var(--sans); text-align: start; white-space: normal;
    pointer-events: none; visibility: hidden; opacity: 0;
  }
  #toc .route-nav a.is-title-overflowing:is(:hover, :focus-visible)::after {
    visibility: visible; opacity: 1; }
}
#toc .route-statuses { flex: none; display: inline-flex; align-items: center;
  gap: .25rem; padding-inline: .2rem .55rem; }
#toc .route-statuses > button { position: relative; display: inline-grid; place-items: center;
  width: 1rem; height: 1rem; padding: 0; border: 0; border-radius: 3px;
  background: transparent; font-family: var(--sans); cursor: help; }
#toc .route-statuses > button:focus-visible { outline: 2px solid var(--primary); outline-offset: 2px; }
#toc .route-reading-status { display: inline-grid; place-items: center;
  color: var(--fg-alt); font-size: .78rem; line-height: 1; }
#toc .route-reading-status::before { content: "○"; }
#toc .route-reading-status.is-complete { color: color-mix(in srgb, var(--reading-done-color) 38%, var(--fg-alt)); font-weight: 700; }
#toc .route-reading-status.is-complete::before { content: "✓"; }
#toc .route-reading-status.is-available { color: color-mix(in srgb, var(--primary) 38%, var(--fg-alt)); font-weight: 700; }
#toc .route-reading-status.is-available::before { content: "→"; }
#toc .route-review-status { display: inline-grid; place-items: center;
  color: var(--fg-alt); }
#toc .route-review-status svg { width: .9rem; height: .9rem; fill: none;
  stroke: currentColor; stroke-width: 1.5; stroke-linecap: round; stroke-linejoin: round; }
#toc .route-review-status.is-reviewed { color: color-mix(in srgb, var(--reviewed-color) 38%, var(--fg-alt)); }
#toc .route-review-status.is-unreviewed { color: color-mix(in srgb, var(--unreviewed-color) 38%, var(--fg-alt)); }
#toc .route-statuses > button::after {
  content: attr(aria-label); position: absolute; z-index: 10;
  inset-block-end: calc(100% + .3rem); inset-inline-end: 0;
  width: max-content; max-width: 9rem; padding: .35rem .5rem;
  border: 1px solid var(--code-border); border-radius: 6px;
  color: var(--text-fg); background: var(--popup-bg); box-shadow: 0 4px 14px #0002;
  font: .7rem/1.35 var(--sans); text-align: start; white-space: normal;
  pointer-events: none; visibility: hidden; opacity: 0;
}
#toc .route-statuses > button.is-tip-open { z-index: 2; }
#toc .route-statuses > button.is-tip-open::after,
#toc .route-statuses > button:focus-visible::after { visibility: visible; opacity: 1; pointer-events: auto; }
@media (hover: hover) and (pointer: fine) {
  #toc .route-statuses > button:hover::after { visibility: visible; opacity: 1; pointer-events: auto; }
}
@media (max-width: 60rem), (pointer: coarse) {
  #toc .route-statuses { padding-inline-end: .2rem; }
}
#toc a[aria-current] { color: var(--link-color); font-weight: 600;
  background: color-mix(in srgb, var(--primary) 10%, transparent);
  box-shadow: inset 2px 0 var(--primary); }
#toc .toc-branch > summary { gap: .55rem; padding: 0 .65rem 0 .55rem; }
/* The title alone navigates. The remaining summary, including its whitespace
   and chevron, toggles the branch, like the section menu above the article. */
#toc .toc-branch > summary > a { flex: 0 1 auto; min-width: 0;
  max-width: calc(100% - 2.4rem); padding-inline: 0; }
#toc .toc-branch > summary > a:hover,
#toc .toc-branch > summary > a[aria-current] { background: none; box-shadow: none; }
#toc .toc-branch > summary > a:hover { text-decoration: underline; }
#toc .toc-branch > summary:has(> a[aria-current]) {
  background: color-mix(in srgb, var(--primary) 10%, transparent);
  box-shadow: inset 2px 0 var(--primary); }
#toc .toc-branch > ul { margin-left: .65rem; padding-left: .4rem;
  border-left: 1px solid var(--ruler); }
#toc :is(a, summary):focus-visible { outline: 2px solid var(--primary); outline-offset: -2px; }
article { min-width: 0; line-height: 1.2; overflow-wrap: anywhere; }   /* 1lab's prose line-height */
article p, article ul, article ol, article blockquote { margin-block: 0.95em; }
/* A proof immediately following its statement is one reading unit. Reduce
   both facing margins so margin collapse cannot restore the ordinary gap. */
article p.prose-statement:has(+ p.prose-proof) { margin-block-end: .45em; }
article p.prose-statement + p.prose-proof { margin-block-start: .45em; }
/* CJK at 1.2 is cramped; relax slightly for Chinese/Japanese prose (1lab is Latin-only). */
html[lang="zh"] article, html[lang="ja"] article { line-height: 1.5; }
article h1 { font-size: 2rem; margin-top: 0; }
#section-sticky + h1 { margin-top: 1.25rem; }
article h2, article h3 { margin-top: 2rem; }   /* no underline, like 1lab */
#sidenote-container { }

/* The current position opens a compact chapter directory beneath the reading column. */
#section-sticky {
  position: sticky; top: calc(var(--site-header-height, 3.5rem) - 1px); z-index: 19;
  width: 100%; height: var(--section-nav-height, 2.75rem);
  color: var(--fg-alt); background: color-mix(in srgb, var(--text-bg) 96%, transparent);
  border-bottom: 1px solid var(--ruler); backdrop-filter: blur(10px);
  font: 600 .82rem/1.2 var(--sans);
}
.section-trigger { display: flex; align-items: center; gap: .6rem; width: 100%; height: 100%;
  padding: 0 .65rem; border: 0; background: transparent; color: inherit;
  font: inherit; text-align: left; cursor: pointer; }
.section-trigger:hover, .section-trigger[aria-expanded="true"] {
  color: var(--text-fg); background: color-mix(in srgb, var(--primary) 7%, var(--text-bg)); }
.section-trigger:focus-visible, #section-menu :is(a, button):focus-visible {
  outline: 2px solid var(--primary); outline-offset: -2px; }
.section-trail { display: flex; align-items: center; gap: .45rem; min-width: 0; overflow: hidden;
  flex: 1; white-space: nowrap; }
.section-trail > span:not(.section-separator) { min-width: 0; overflow: hidden; text-overflow: ellipsis; }
.section-trail > span:last-child { color: var(--text-fg); }
#section-sticky .section-separator { flex: none; color: var(--ruler); font-weight: 400; }
.section-chevron, .section-branch-toggle::before { display: block; width: .45rem; height: .45rem;
  border-right: 2px solid currentColor; border-bottom: 2px solid currentColor;
  transform: rotate(45deg); transition: transform .16s ease; }
.section-chevron { flex: none; margin: -.25rem .2rem 0 0; }
.section-trigger[aria-expanded="true"] .section-chevron,
.section-branch-toggle[aria-expanded="true"]::before { transform: rotate(225deg); }
#section-menu { position: absolute; top: 100%; left: 0; right: 0; margin-top: .2rem;
  max-height: min(60dvh, calc(100dvh - var(--site-header-height, 3.5rem) - var(--section-nav-height, 2.75rem) - 1rem));
  overflow-y: auto; overscroll-behavior: contain; padding: .25rem;
  background: var(--popup-bg); border: 1px solid var(--input-border); border-radius: 8px;
  box-shadow: 0 9px 28px rgba(0, 0, 0, .18); scrollbar-width: thin;
  animation: section-menu-in .16s ease-out; }
#section-menu[hidden], #section-menu ul[hidden] { display: none; }
.section-menu-list, .section-menu-item > ul { list-style: none; margin: 0; padding: 0; }
.section-menu-item > ul { margin-left: .75rem; padding-left: .45rem; border-left: 1px solid var(--ruler); }
.section-menu-row { display: flex; align-items: stretch; }
.section-menu-row.has-children { min-height: 2.4rem; padding: 0 .55rem;
  border-radius: 5px; }
#section-menu a { display: flex; align-items: center; flex: 1; min-width: 0; min-height: 2.4rem;
  padding: .42rem .55rem; border-radius: 5px; color: var(--text-fg);
  font: 500 .84rem/1.35 var(--sans); text-decoration: none; overflow-wrap: anywhere; }
#section-menu .has-children > a { flex: 0 1 auto; min-height: 0; max-width: calc(100% - 2.4rem);
  padding: 0; }
#section-menu a:hover {
  background: color-mix(in srgb, var(--primary) 8%, transparent); }
#section-menu .has-children:hover { background: color-mix(in srgb, var(--primary) 8%, transparent); }
#section-menu .has-children > a:hover, #section-menu .has-children > a[aria-current] {
  background: none; box-shadow: none; }
#section-menu .has-children > .section-branch-toggle:hover { background: transparent; }
#section-menu .has-children > a:hover { text-decoration: underline; }
#section-menu a[aria-current] { color: var(--link-color); font-weight: 650;
  background: color-mix(in srgb, var(--primary) 10%, transparent);
  box-shadow: inset 2px 0 var(--primary); }
#section-menu .has-children:has(> a[aria-current]) {
  background: color-mix(in srgb, var(--primary) 10%, transparent);
  box-shadow: inset 2px 0 var(--primary); }
.section-branch-toggle { display: flex; align-items: center; justify-content: center;
  flex: 1 0 2.4rem; min-width: 2.4rem; min-height: 2.4rem; padding: 0; border: 0; border-radius: 5px;
  background: transparent; color: var(--fg-alt); cursor: pointer; }
.has-children > .section-branch-toggle { justify-content: flex-end; }
.section-branch-toggle::before { content: ""; margin-top: -.2rem; }
@keyframes section-menu-in { from { opacity: 0; transform: translateY(-.35rem); }
  to { opacity: 1; transform: translateY(0); } }
@media (max-width: 60rem) {
  #section-menu a, .section-branch-toggle, .section-menu-row.has-children { min-height: 44px; }
  .section-branch-toggle { flex-basis: 44px; min-width: 44px; }
  #section-menu .has-children > a { max-width: calc(100% - 44px); min-height: 0; }
}
@media (prefers-reduced-motion: reduce) {
  #section-menu { animation: none; }
  .section-chevron, .section-branch-toggle::before { transition: none; }
}

/* ---- prose ---- */
article a { color: var(--link-color); text-decoration: none; }
article a:hover { text-decoration: underline; }
/* Prose hyperlinks need a non-colour cue; code and glossary links retain their
   existing semantic treatments instead of inheriting this underline. */
article :is(p, li, blockquote, figcaption, td) > a[href]:not(.inline-ref):not(.term-ref) {
  text-decoration: underline;
  text-decoration-color: color-mix(in srgb, var(--link-color) 55%, transparent);
  text-decoration-thickness: .055em; text-underline-offset: .16em;
}
article :not(pre):not(code) > code { font-family: var(--mono); font-size: 0.88em;
  color: var(--code-fg); background: var(--code-inline-bg); padding: 0.1em 0.3em;
  border: 1px solid var(--code-border); border-radius: 4px; }
.single-line-code { position: relative; margin: 1rem 0; text-align: center; }
.single-line-code > code { font-family: var(--mono); font-size: var(--code-font-size);
  color: var(--code-fg); background: var(--code-bg); padding: 0.35rem 0.7rem;
  border: 1px solid var(--code-border); border-radius: 6px; white-space: nowrap;
  transition: background-color .16s ease, border-color .16s ease, box-shadow .16s ease; }
.single-line-code[data-note]::before { position: absolute; left: calc(100% + .35rem); top: 50%; width: 1.3rem;
  height: 2px; content: ""; background: var(--primary); opacity: .65; }
.single-line-code-note { position: absolute; left: calc(100% + 2rem); top: 50%;
  width: min(22rem, var(--note-width, 30vw)); transform: translateY(-50%); color: var(--fg-alt);
  border-left: 3px solid var(--primary); padding: .35rem .65rem; background: var(--code-bg);
  border-radius: 0 6px 6px 0; font-size: 0.86em; line-height: 1.4; text-align: left;
  user-select: text;
  transition: background-color .16s ease, border-color .16s ease, box-shadow .16s ease; }
.single-line-code[data-note] > code:hover,
.single-line-code[data-note] > code:focus-visible,
.single-line-code[data-note]:has(.single-line-code-note:hover) > code {
  border-color: var(--primary);
  background: color-mix(in srgb, var(--primary) 14%, var(--code-bg));
  box-shadow: 0 2px 10px color-mix(in srgb, var(--primary) 16%, transparent); }
.single-line-code[data-note] > code:hover ~ .single-line-code-note,
.single-line-code[data-note] > code:focus-visible ~ .single-line-code-note,
.single-line-code-note:hover {
  border-left-color: color-mix(in srgb, var(--primary) 80%, white);
  background: color-mix(in srgb, var(--primary) 16%, var(--code-bg));
  box-shadow: 0 4px 16px color-mix(in srgb, var(--primary) 20%, transparent); }
.prose-annotation { display: inline; }
.prose-annotation-target { border-bottom: 2px solid color-mix(in srgb, var(--primary) 55%, transparent);
  background: color-mix(in srgb, var(--primary) 8%, transparent);
  transition: background-color .16s ease, border-color .16s ease; }
.prose-annotation-connector { position: absolute; top: var(--note-top, 0px);
  left: calc(100% + .35rem); width: 1.3rem;
  height: 2px; transform: translateY(-50%); content: ""; background: var(--primary); opacity: .65; }
.prose-annotation-note { position: absolute; top: var(--note-top, 0px);
  left: calc(100% + 2rem);
  width: min(22rem, var(--note-width, 30vw)); transform: translateY(-50%); color: var(--fg-alt);
  border-left: 3px solid var(--primary); padding: .35rem .65rem; background: var(--code-bg);
  border-radius: 0 6px 6px 0; font-size: .86em; line-height: 1.4; text-align: left;
  user-select: text; z-index: 2;
  transition: background-color .16s ease, border-color .16s ease, box-shadow .16s ease; }
.prose-annotation-target:hover, .prose-annotation-target:focus-visible,
.prose-annotation-target.annotation-active {
  border-bottom-color: var(--primary);
  background: color-mix(in srgb, var(--primary) 20%, transparent); }
.prose-annotation-note.annotation-active {
  border-left-color: color-mix(in srgb, var(--primary) 80%, white);
  background: color-mix(in srgb, var(--primary) 16%, var(--code-bg));
  box-shadow: 0 4px 16px color-mix(in srgb, var(--primary) 20%, transparent); }
/* Each submodule owns an indented column; align code within that column. */
.submodule-fold { margin: 1.25rem 0 1.25rem .8rem; padding: .4rem .8rem .35rem;
  border-left: 2px solid color-mix(in srgb, var(--ruler) 75%, var(--text-bg));
  border-radius: 0 8px 8px 0;
  background: color-mix(in srgb, var(--code-bg) 32%, var(--text-bg)); }
.submodule-fold > .submodule-fold-heading { display: flex; align-items: center; gap: .65rem;
  list-style: none; cursor: pointer; padding-right: .2rem;
  border: 1px solid color-mix(in srgb, var(--ruler) 55%, transparent);
  border-radius: 5px;
  background: color-mix(in srgb, var(--code-bg) 68%, var(--text-bg)); }
.submodule-fold > .submodule-fold-heading::-webkit-details-marker { display: none; }
.submodule-fold > .submodule-fold-heading::after { content: ""; flex: 0 0 .45rem;
  width: .45rem; height: .45rem; margin: 0 .35rem;
  border-right: 2px solid var(--primary); border-bottom: 2px solid var(--primary);
  transform: rotate(45deg); transition: transform .24s ease; }
.submodule-fold:is(:not([open]), .submodule-closing) > .submodule-fold-heading::after { transform: rotate(-45deg); }
.submodule-fold > .submodule-fold-heading:hover { background: color-mix(in srgb, var(--primary) 5%, transparent); }
.submodule-fold > .submodule-fold-heading:focus-visible { outline: 2px solid var(--primary); outline-offset: 3px; }
.submodule-fold > .submodule-fold-heading > pre.Agda { flex: 1; min-width: 0; margin: 0;
  padding: .45rem .2rem; border: 0; background: transparent; }
.submodule-fold > .submodule-fold-content { margin-top: .35rem; }
.submodule-fold:not([open]) { padding-bottom: .4rem; }
.submodule-fold > .submodule-fold-content > :last-child { margin-bottom: 0; }
.submodule-fold .submodule-fold { margin-left: .35rem;
  background: color-mix(in srgb, var(--code-bg) 42%, var(--text-bg)); }
@media (max-width: 700px) {
  .submodule-fold { margin-left: .25rem; padding: .3rem .45rem .3rem; }
  .submodule-fold .submodule-fold { margin-left: 0; padding-left: .35rem; padding-right: .35rem; }
  .submodule-fold > .submodule-fold-heading { gap: .3rem; }
}
article li > code { font-family: var(--mono); font-size: .88em;
  color: var(--code-fg); background: var(--code-inline-bg); padding: .1em .3em;
  border: 1px solid var(--code-border); border-radius: 4px; white-space: nowrap; }
.banner { background: var(--banner-bg); color: var(--banner-fg);
  padding: 0.6rem 1rem; border-radius: 8px; margin-bottom: 1.5rem; font-family: var(--sans);
  font-size: 0.9rem; }

/* External-library pages: a coloured header marks departure from the current
   project. The background alone signals the state, without an extra divider. */
.ext-banner { background: var(--banner-bg); color: var(--banner-fg); font-family: var(--sans);
  font-weight: 600; text-align: center; padding: 0.55rem 1rem; }
.ext-banner a { color: var(--banner-fg); text-decoration: underline; margin-left: 0.5rem; }
blockquote { border-left: 0.3ex solid var(--ruler); margin-left: 0; padding-left: 1rem;
  color: var(--fg-alt); }
.module-index { list-style: none; padding-left: 0; }
.module-index li { margin: 0.3rem 0; }
.module-index a { font-family: var(--mono); }

/* ---- prose tables ---- */
main .prose-table { margin: 1.2rem 0; min-width: 0; max-width: 100%; }
main .prose-table-scroll { max-width: 100%; overflow-x: auto; margin: 1.2rem 0;
  -webkit-overflow-scrolling: touch; }
main .prose-table .prose-table-scroll { margin: 0; }
main .prose-table > figcaption { margin: .65rem auto 0; color: var(--fg-alt);
  font-size: .85em; line-height: 1.55; text-align: center; text-wrap: pretty; }
main table { border-collapse: separate; border-spacing: 0; margin: 1.2rem auto;
  border: 1px solid var(--ruler); border-radius: var(--content-frame-radius); overflow: hidden; }
main .prose-table-scroll table { margin-block: 0; }
main th, main td { border: 0; border-inline-end: 1px solid var(--ruler);
  border-block-end: 1px solid var(--ruler); padding: 0.4rem 0.9rem;
  text-align: left; vertical-align: top; }
main table tr > :last-child { border-inline-end: 0; }
main table > :last-child > tr:last-child > * { border-block-end: 0; }
main table > :first-child > tr:first-child > :first-child {
  border-top-left-radius: calc(var(--content-frame-radius) - 1px); }
main table > :first-child > tr:first-child > :last-child {
  border-top-right-radius: calc(var(--content-frame-radius) - 1px); }
main th { background: var(--code-bg); font-family: var(--sans); font-size: 0.9em; }
main .prose-table-scroll :is(th, td) > span.Agda.inline-code { display: inline-block; }

/* ---- code blocks (Agda) ---- */
pre.Agda, pre.sourceCode {
  font-family: var(--mono); font-size: var(--code-font-size); line-height: 1.45;
  background: var(--code-bg); padding: 0.8rem 1rem; border-radius: 8px;
  border: 1px solid var(--code-border); overflow-x: auto; margin: 1.2rem 0;
}
/* Exposition introduces the following Agda block, not the preceding one. */
pre.Agda { position: relative; margin: .5rem 0 1.6rem; height: auto; max-height: none; overflow-y: hidden;
  -webkit-text-size-adjust: 100%; text-size-adjust: 100%; }
/* Keep padding outside the scrolling viewport, so code never paints against
   either border, even at an intermediate scroll offset. Fold declarations
   deliberately retain their own compact, unwrapped presentation. */
pre.Agda:has(> .agda-code-content) { overflow: visible; }
pre.Agda > .agda-code-content {
  display: block; min-width: 0; max-width: 100%; height: auto; max-height: none;
  overflow-x: auto; overflow-y: hidden;
}
.code-copy-button {
  display: grid; place-items: center; box-sizing: border-box;
  width: 2rem; height: 2rem; padding: 0;
  border: 1px solid var(--input-border); border-radius: 7px;
  color: var(--fg-alt); background: var(--popup-bg);
  font: 500 .75rem/1 var(--sans); cursor: pointer;
  touch-action: manipulation; -webkit-tap-highlight-color: transparent;
  transition: opacity .14s ease, color .14s ease, background-color .14s ease;
}
.code-copy-button svg { width: 19px; height: 19px; fill: none;
  stroke: currentColor; stroke-width: 1.6; stroke-linecap: round; stroke-linejoin: round; }
.code-copy-button:is(:hover, :focus-visible), .code-copy-button.is-copied {
  color: var(--text-fg); background: color-mix(in srgb, var(--primary) 9%, var(--popup-bg));
}
.code-copy-button:focus-visible { outline: 2px solid var(--primary); outline-offset: 2px; }
.code-copy-button[data-feedback]::after { content: attr(data-feedback); position: absolute;
  z-index: 2; inset-inline-end: 0; top: calc(100% + .3rem);
  width: max-content; max-width: 12rem; padding: .4rem .55rem;
  border: 1px solid var(--input-border); border-radius: 6px;
  color: var(--text-fg); background: var(--popup-bg); box-shadow: var(--shadow-float);
  white-space: nowrap; pointer-events: none; }
.code-copy-inline { position: absolute; z-index: 4; top: .35rem; inset-inline-end: .35rem;
  opacity: 0; pointer-events: none; }
.submodule-fold-heading > pre.Agda > .code-copy-inline {
  top: 50%; transform: translateY(-50%);
}
pre.Agda:is(:hover, :focus-within) > .code-copy-inline,
.code-copy-inline:focus-visible { opacity: 1; pointer-events: auto; }
.code-copy-mobile { position: fixed; z-index: 170; width: 44px; height: 44px;
  box-shadow: var(--shadow-float); }
.code-copy-mobile[hidden] { display: none; }
@media (hover: none), (pointer: coarse) { .code-copy-inline { display: none; } }
@media (prefers-reduced-motion: reduce) { .code-copy-button { transition: none; } }
article :is(p, ul, ol, blockquote, .prose-table-scroll):has(+ pre.Agda) {
  margin-block-end: .5rem;
}
article :is(p, ul, ol, blockquote, .prose-table-scroll):has(+ .agda-code-preview) {
  margin-block-end: .5rem;
}
.agda-code-preview { margin: .5rem 0 1.6rem; min-width: 0;
  border: 1px solid var(--code-border); border-radius: 8px;
  background: var(--code-bg); overflow: hidden; }
.agda-code-preview > .agda-code-preview-clip { min-width: 0; max-height: var(--agda-preview-full-height, none); overflow: hidden; }
.agda-code-preview.is-ready > .agda-code-preview-clip { transition: max-height .2s ease; }
.agda-code-preview > .agda-code-preview-clip > pre.Agda {
  margin: 0; border: 0; border-radius: 0; }
.agda-code-preview.is-collapsed > .agda-code-preview-clip {
  max-height: var(--agda-preview-height);
}
.agda-code-preview-toggle {
  display: flex; align-items: center; justify-content: center; gap: .55rem;
  width: 100%; min-height: 2.75rem; margin: 0; padding: .45rem .8rem;
  border: 0; border-top: 1px solid var(--code-border); border-radius: 0;
  background: color-mix(in srgb, var(--code-bg) 90%, var(--text-bg));
  color: var(--fg-alt); font: 500 .82rem/1.4 var(--sans); cursor: pointer;
  touch-action: manipulation; transition: background-color .16s ease, color .16s ease;
}
.agda-code-preview-toggle::after { content: ""; width: .4rem; height: .4rem;
  border-right: 1.5px solid currentColor; border-bottom: 1.5px solid currentColor;
  transform: rotate(-135deg); transition: transform .16s ease; }
.agda-code-preview-toggle[aria-expanded="false"]::after { transform: rotate(45deg); }
.agda-code-preview-toggle[hidden] { display: none; }
.agda-code-preview-toggle:hover, .agda-code-preview-toggle:focus-visible {
  color: var(--text-fg); background: color-mix(in srgb, var(--primary) 7%, var(--code-bg));
}
.agda-code-preview-toggle:focus-visible { outline: 2px solid var(--primary); outline-offset: -3px; }
@media (prefers-reduced-motion: reduce) {
  .agda-code-preview.is-ready > .agda-code-preview-clip,
  .agda-code-preview-toggle, .agda-code-preview-toggle::after { transition: none; }
}
pre.Agda a { text-decoration: none; color: var(--code-fg); }
pre.Agda a:hover[href] { text-decoration: underline; }
.Agda .Comment, .Agda .Markup, .Agda .Pragma { color: var(--code-comment); }
.Agda .Comment { font-style: italic; }
.Agda .Keyword { color: var(--code-keyword); }
.Agda .String  { color: var(--code-string); }
.Agda .Number  { color: var(--code-number); }
.Agda .Symbol  { color: var(--code-fg); }
.Agda .Bound, .Agda .Generalizable { color: var(--code-fg); }
.Agda .InductiveConstructor, .Agda .CoinductiveConstructor { color: var(--code-constructor); }
.Agda .Field   { color: var(--code-field); }
.Agda .Module  { color: var(--code-module); }
.Agda .Datatype, .Agda .Function, .Agda .Postulate, .Agda .Primitive,
.Agda .Record, .Agda .PrimitiveType { color: var(--code-identifier); }
.type-value.Agda a:is(.Primitive, .PrimitiveType):not([data-type]),
.type-value.Agda a[data-hover-stop] { color: var(--code-fg); }
.Agda .Macro   { color: var(--code-macro); }
.inline-ref { font-family: var(--mono); font-size: 0.88em; }
article p > .inline-ref, article li > .inline-ref,
article :not(pre):not(code) > .Agda.inline-code { background: var(--code-inline-bg);
  border: 1px solid var(--code-border); border-radius: 4px;
  /* Combining hats (x̂, b̂) rise above the ordinary glyph box. Keep their ink
     clear of the top border without enlarging the paragraph's line spacing. */
  padding: .24em .28em .08em; }
/* Wrapped inline code needs a complete box on each line, not sliced edges.
   Allow long list-item names to wrap too instead of overflowing the column. */
article :not(pre):not(code) > code,
article p > .inline-ref, article li > .inline-ref,
article :not(pre):not(code) > .Agda.inline-code {
  box-decoration-break: clone; -webkit-box-decoration-break: clone;
  white-space: normal; overflow-wrap: anywhere;
}
a.inline-ref { color: var(--code-identifier); }
/* expression refs: links inside the span default to identifier colour
   (aspect classes override via .Agda .<Aspect>), plain tokens to code fg */
span.inline-ref { color: var(--code-fg); }
.inline-ref a { color: var(--code-identifier); text-decoration: none; }
.inline-ref a:hover[href] { text-decoration: underline; }
/* same-definition occurrence highlight (hover any occurrence, all light up) */
.Agda a.occ,
.Agda a.name-active {
  background: var(--occ-bg); border-radius: 3px;
}
.type-value a[data-hover-stop]:is(:hover, .occ, .name-active) {
  background: transparent; border-radius: 0;
}

/* ---- chapter prev/next navigation (the reading order, on every page) ---- */
.chapnav { display: flex; justify-content: space-between; gap: 1rem;
  margin-top: 2.5rem; padding-top: 1rem; border-top: 1px solid var(--ruler);
  font-family: var(--sans); font-size: 0.95rem; }
.chapnav a { text-decoration: none; color: var(--link-color); }
.chapnav .chapnav-next { margin-left: auto; text-align: right; }
.chapnav-top { margin: 0 0 1.5rem; padding: 0 0 1rem;
  border-top: 0; border-bottom: 1px solid var(--ruler); }
.chapnav a { display: flex; align-items: center; gap: .45em;
  min-width: 0; max-width: 48%; overflow-wrap: anywhere; }
.chapnav-icon { width: 1.1em; height: 1.1em; flex: 0 0 auto; }
.chapnav-title { min-width: 0; }
.chapnav a:hover { text-decoration: underline; }

/* ---- quick page scrolling ---- */
.page-scroll { position: fixed; z-index: 25;
  right: max(1rem, env(safe-area-inset-right));
  bottom: max(1rem, env(safe-area-inset-bottom));
  display: flex; flex-direction: column; gap: .35rem; }
.page-scroll button { display: grid; place-items: center; width: 2.75rem; height: 2.75rem;
  padding: .65rem; border: 1px solid var(--code-border); border-radius: .65rem;
  background: var(--text-bg); color: var(--fg-alt); cursor: pointer;
  box-shadow: 0 2px 8px rgb(0 0 0 / .08); }
.page-scroll button:hover { background: var(--button-hover); color: var(--primary); }
.page-scroll button:focus-visible { outline: 2px solid var(--primary); outline-offset: 3px; }
.page-scroll svg { width: 100%; height: 100%; fill: none; stroke: currentColor;
  stroke-width: 1.7; stroke-linecap: round; stroke-linejoin: round; }

/* ---- type-on-hover popup ---- */
.expr-node, .type-node { --ast-node-level: var(--expr-level);
  /* Wide hue steps keep adjacent nesting levels distinct. OKLCH holds their
     perceived brightness steady; HSL remains as a compatibility fallback. */
  --ast-node-color: hsl(calc(210 - var(--ast-node-level) * 55) 76% 43%);
  --ast-node-color: oklch(var(--ast-node-lightness) var(--ast-node-chroma)
    calc(250 - var(--ast-node-level) * 55));
  margin-inline: .015rem; padding: .03rem .055rem .13rem;
  border-radius: .28rem .28rem .14rem .14rem;
  background: transparent;
  box-shadow: none;
  box-decoration-break: clone; -webkit-box-decoration-break: clone;
  cursor: default;
  transition: background-color .1s ease, box-shadow .1s ease; }
pre.Agda:hover .expr-node,
pre.Agda.ast-ranges-visible .expr-node,
.type-value .type-node:not([data-single-name]) {
  background: color-mix(in srgb, var(--ast-node-color) 4%, transparent);
  box-shadow: inset 1px 0 color-mix(in srgb, var(--ast-node-color) 52%, transparent),
    inset -1px 0 color-mix(in srgb, var(--ast-node-color) 52%, transparent),
    inset 0 -1px color-mix(in srgb, var(--ast-node-color) 52%, transparent);
}
pre.Agda .expr-node.expr-active,
.type-value .type-node.type-active:not([data-single-name]) {
  background: color-mix(in srgb, var(--ast-node-color) 14%, transparent);
  box-shadow: inset 2px 0 color-mix(in srgb, var(--ast-node-color) 95%, transparent),
    inset -2px 0 color-mix(in srgb, var(--ast-node-color) 95%, transparent),
    inset 0 -2px color-mix(in srgb, var(--ast-node-color) 95%, transparent);
}
.type-value .type-node[data-single-name] {
  margin-inline: 0; padding: 0; background: transparent; box-shadow: none;
}
.type-value .type-node[data-single-name].type-active {
  background: var(--occ-bg); border-radius: 3px; box-shadow: none;
}
/* Touch selection is controlled by the shared gesture state, not Safari's
   sticky :hover left on the original leaf after sliding to a parent. */
@media (hover: hover) and (pointer: fine) {
  .type-value a[href]:not([data-hover-stop]):hover,
  .type-value .type-node[data-single-name]:hover {
    background: var(--occ-bg); border-radius: 3px; box-shadow: none;
  }
}
.hover-popup {
  position: absolute; z-index: 150; max-width: 40rem;
  color: var(--code-fg); background: var(--popup-bg);
  border: 1px solid var(--input-border);
  border-radius: 8px; box-shadow: 0 6px 20px rgba(0,0,0,.2);
  padding: 0.4rem 0.6rem; font-family: var(--mono); font-size: 0.8rem;
  white-space: pre-wrap; pointer-events: none;
}
.hover-popup a { color: var(--code-identifier); text-decoration: none; }
.name-hover-popup { pointer-events: auto; }
.hover-loading { display: inline-flex; align-items: center; gap: .5rem;
  color: var(--code-comment); font: .8rem/1.6 var(--sans); }
.hover-loading::before { content: ''; width: .8rem; height: .8rem;
  border: 1.5px solid var(--code-border); border-top-color: var(--code-comment);
  border-radius: 50%; animation: hover-loading-spin .7s linear infinite; }
@keyframes hover-loading-spin { to { transform: rotate(360deg); } }
@media (prefers-reduced-motion: reduce) { .hover-loading::before { animation: none; } }
.info-hover-popup { max-width: min(42rem, calc(100vw - 1rem)); box-sizing: border-box; }
/* Revealed source code: the article's code-block surface, lifted into a card.
   Only this shell changes; nested type/syntax popups retain their own surfaces. */
.boilerplate-hover-popup {
  background: var(--code-bg); border: 1px solid var(--code-border);
  border-left: 3px solid color-mix(in srgb, var(--primary) 38%, var(--code-border));
  border-radius: 8px; padding: .75rem .9rem;
  box-shadow: 0 2px 6px rgba(0,0,0,.10), 0 12px 32px rgba(0,0,0,.18);
}
.boilerplate-hover { font: inherit; color: inherit; background: transparent; border: 0;
  padding: .12em .1em; text-align: inherit; cursor: help; border-radius: 4px;
  text-decoration: underline dashed color-mix(in srgb, var(--primary) 55%, transparent);
  text-underline-offset: .22em; text-decoration-thickness: 1px; }
/* A chapter title is already prominent; its code mark alone signals the source
   popup without making the whole title look like a reader-term link. */
.chapter-heading-row .boilerplate-hover { text-decoration: none; }
.boilerplate-hover::after { content: " ‹/›"; font: .55em var(--mono); color: var(--fg-alt);
  vertical-align: middle; white-space: nowrap; }
.boilerplate-hover.info-active { background: color-mix(in srgb, var(--primary) 12%, transparent); }
.boilerplate-hover:focus-visible, .syntax-hover:focus-visible { outline: 2px solid var(--primary); outline-offset: 3px; }
.syntax-help { font-family: var(--sans); white-space: normal; line-height: 1.65; max-width: 30rem; }
.syntax-help strong { font-family: var(--mono); }
.syntax-help p { margin: .35rem 0; }
.syntax-help .syntax-doc-link { color: var(--link-color); text-decoration: underline; display: inline-block; padding: .35rem 0; }
.Agda .syntax-hover { cursor: help; border-radius: 3px; }
.Agda .syntax-symbol { color: var(--code-symbol); }
.Agda .syntax-hover.info-active { background: color-mix(in srgb, #db8700 32%, var(--code-bg));
  box-shadow: inset 0 -2px #db8700; }
@media (hover: hover) and (pointer: fine) {
  .boilerplate-hover:hover { background: color-mix(in srgb, var(--primary) 12%, transparent); }
  .Agda .syntax-hover:hover { background: color-mix(in srgb, #db8700 32%, var(--code-bg));
    box-shadow: inset 0 -2px #db8700; }
}
.type-inspector { position: absolute; max-width: min(42rem, calc(100vw - 1rem));
  box-sizing: border-box; color: var(--code-fg); background: var(--code-bg);
  border-color: var(--code-border); pointer-events: auto; overflow-y: auto; }
.type-inspector-measure { left: -10000px; top: 0; width: max-content;
  max-height: none !important; overflow: visible !important;
  visibility: hidden; pointer-events: none; }
.type-value { padding-inline: .15rem; overflow-x: auto; overflow-y: hidden; }
.name-hover-popup.compact-type .type-value { white-space: pre; }
.type-definition-link { display: none; }

/* Landscape code is a browser-viewport reading surface. It never depends on
   device orientation lock, and uses the original nodes, anchors and gestures. */
.code-fullscreen-toggle, .code-fullscreen-close, .code-copy-fullscreen {
  display: grid; place-items: center; width: 44px; height: 44px; padding: 0;
  border: 1px solid var(--input-border); border-radius: 8px;
  color: var(--fg-alt); background: var(--popup-bg); cursor: pointer;
}
.code-fullscreen-toggle { position: fixed; z-index: 170; box-shadow: var(--shadow-float); }
.code-fullscreen-toggle[hidden] { display: none; }
.code-fullscreen-toggle svg { width: 21px; height: 21px; stroke: currentColor;
  stroke-width: 1.6; fill: none; stroke-linecap: round; stroke-linejoin: round; }
.code-fullscreen { position: fixed; inset: 0 auto auto 0; z-index: 180;
  overflow: hidden; color: var(--text-fg); background: var(--text-bg);
  /* Rotated landscape width is not a request for mobile text inflation.
     A percentage preserves user zoom; do not use viewport scale restrictions. */
  -webkit-text-size-adjust: 100%; text-size-adjust: 100%; }
.code-fullscreen-plane, .code-fullscreen-controls {
  --code-safe-top: env(safe-area-inset-top, 0px);
  --code-safe-right: env(safe-area-inset-right, 0px);
  --code-safe-bottom: env(safe-area-inset-bottom, 0px);
  --code-safe-left: env(safe-area-inset-left, 0px);
  position: absolute; top: 0; left: 0; box-sizing: border-box; transform-origin: top left;
}
.code-fullscreen .is-rotated {
  --code-safe-top: env(safe-area-inset-right, 0px);
  --code-safe-right: env(safe-area-inset-bottom, 0px);
  --code-safe-bottom: env(safe-area-inset-left, 0px);
  --code-safe-left: env(safe-area-inset-top, 0px);
}
.code-fullscreen-plane {
  padding: calc(3.5rem + var(--code-safe-top)) max(1rem, var(--code-safe-right))
    max(1.5rem, var(--code-safe-bottom)) max(1rem, var(--code-safe-left));
  overflow: auto; overscroll-behavior: contain;
}
.code-fullscreen-controls { z-index: 2; pointer-events: none; }
.code-fullscreen-close { position: absolute; pointer-events: auto;
  right: max(.5rem, var(--code-safe-right)); top: max(.35rem, var(--code-safe-top));
  font: 1.5rem/1 var(--sans); }
.code-copy-fullscreen { position: absolute; pointer-events: auto;
  right: calc(max(.5rem, var(--code-safe-right)) + 52px);
  top: max(.35rem, var(--code-safe-top)); }
.code-fullscreen-plane > pre.Agda { margin: 0; min-width: 0; }
.code-fullscreen-plane .hover-popup { max-width: min(42rem, calc(var(--code-surface-width) - 1rem)); }
body.code-fullscreen-open { overflow: hidden; }
body.code-fullscreen-open > .ast-swipe-hint { display: none; }
.code-fullscreen :focus-visible, .code-fullscreen-toggle:focus-visible, .code-copy-mobile:focus-visible {
  outline: 2px solid var(--primary); outline-offset: 2px;
}

@media (hover: none), (pointer: coarse) {
  .type-inspector { max-height: calc(100vh - 1rem); overflow-y: auto; }
  .hover-popup.has-definition-link { padding-right: 2.75rem; }
  .type-definition-link { position: absolute; top: 0; right: .25rem; bottom: 0; display: grid;
    width: 2.25rem; padding: 0; place-items: center;
    color: var(--primary) !important; border-left: 1px solid var(--code-border);
    border-radius: 0 .45rem .45rem 0; text-decoration: none;
    touch-action: manipulation; -webkit-tap-highlight-color: transparent; }
  .type-definition-link svg { width: 1.25rem; height: 1.25rem; fill: none;
    stroke: currentColor; stroke-width: 1.8; stroke-linecap: round;
    stroke-linejoin: round; vector-effect: non-scaling-stroke; }
  .type-definition-link[hidden] { display: none; }
  .type-definition-link:active { color: var(--text-fg) !important;
    background: color-mix(in srgb, var(--primary) 12%, transparent); }
  .expr-node, .type-node { padding: .07rem .08rem .17rem; }
  pre.Agda .expr-node, pre.Agda .expr-node *,
  .type-value .type-node, .type-value .type-node * {
    user-select: none; -webkit-user-select: none; }
  pre.Agda :is(.expr-node, a[data-type]),
  .type-value :is(.type-node, a[data-type]) { touch-action: pan-y;
    -webkit-touch-callout: none; }
  :is(pre.Agda, .hover-popup).ast-level-gesture {
    user-select: none; -webkit-user-select: none; }
  .type-value .type-node:not([data-single-name]),
  .type-value .type-node.type-active:not([data-single-name]) {
    background: transparent; box-shadow: none;
  }
  .hover-popup.ast-ranges-visible .type-value .type-node:not([data-single-name]) {
    background: color-mix(in srgb, var(--ast-node-color) 4%, transparent);
    box-shadow: inset 1px 0 color-mix(in srgb, var(--ast-node-color) 52%, transparent),
      inset -1px 0 color-mix(in srgb, var(--ast-node-color) 52%, transparent),
      inset 0 -1px color-mix(in srgb, var(--ast-node-color) 52%, transparent);
  }
  .hover-popup.ast-ranges-visible
  .type-value .type-node.type-active:not([data-single-name]) {
    background: color-mix(in srgb, var(--ast-node-color) 14%, transparent);
    box-shadow: inset 2px 0 color-mix(in srgb, var(--ast-node-color) 95%, transparent),
      inset -2px 0 color-mix(in srgb, var(--ast-node-color) 95%, transparent),
      inset 0 -2px color-mix(in srgb, var(--ast-node-color) 95%, transparent);
  }
  .ast-swipe-hint { position: fixed; z-index: 160;
    top: max(1.25rem, calc(env(safe-area-inset-top) + .75rem));
    left: 50%; width: max-content; max-width: calc(100vw - 1rem); box-sizing: border-box;
    min-height: 3.75rem; padding: .7rem 1rem; color: var(--text-fg); background: var(--popup-bg);
    border: 2px solid var(--primary); border-radius: 1rem;
    box-shadow: 0 6px 24px rgba(0,0,0,.3); transform: translateX(-50%);
    font: 700 1rem/1.35 var(--sans); text-align: center; pointer-events: none;
    display: grid; place-items: center; }
  .ast-swipe-hint[hidden] { display: none; }
}

/* ---- definition preview modal with in-dialog history ---- */
body.definition-modal-open { overflow: hidden; }
.definition-modal-backdrop {
  position: fixed; inset: 0; z-index: 120; display: grid; place-items: center;
  padding: max(1rem, env(safe-area-inset-top)) max(1rem, env(safe-area-inset-right))
    max(1rem, env(safe-area-inset-bottom)) max(1rem, env(safe-area-inset-left));
  background: rgb(15 23 42 / .52); backdrop-filter: blur(2px);
}
.definition-modal {
  display: flex; flex-direction: column; width: min(72rem, 94vw); height: 82dvh;
  min-height: 72vh; max-height: calc(100dvh - 2rem);
  color: var(--text-fg); background: var(--popup-bg);
  border: 1px solid var(--code-border); border-radius: 12px;
  box-shadow: 0 18px 55px rgb(0 0 0 / .34); overflow: hidden;
}
.definition-modal-header {
  display: grid; grid-template-columns: auto minmax(0, 1fr) auto auto;
  align-items: center; gap: .75rem;
  min-height: 3.25rem; padding: .65rem .75rem .65rem 1rem;
  border-bottom: 1px solid var(--code-border); font-family: var(--sans);
}
.definition-modal-backdrop.has-fullscreen-code { padding: 0; }
.has-fullscreen-code .definition-modal {
  width: 100vw; height: 100dvh; max-height: none; border: 0; border-radius: 0;
}
.has-fullscreen-code .definition-modal-header { display: none; }
.definition-modal-title {
  min-width: 0; color: var(--fg); font-weight: 700;
  overflow-wrap: anywhere; line-height: 1.4;
}
.definition-modal-title code { font-family: var(--mono); font-size: .88em; }
.definition-modal-history { display: flex; align-items: center; gap: .25rem; }
.definition-modal-history-button {
  display: grid; place-items: center; width: 2.25rem; height: 2.25rem; padding: 0;
  border: 1px solid var(--code-border); border-radius: 7px;
  color: var(--text-fg); background: transparent; font: 1.2rem/1 var(--sans); cursor: pointer;
}
.definition-modal-history-button:hover:not(:disabled),
.definition-modal-history-button:focus-visible:not(:disabled) {
  color: var(--primary); background: var(--button-hover); border-color: var(--primary);
}
.definition-modal-history-button:disabled { opacity: .35; cursor: default; }
.definition-modal-close, .definition-modal-jump {
  display: grid; place-items: center; width: 2.25rem; height: 2.25rem; padding: 0;
  border: 0; border-radius: 7px; color: var(--fg-alt); background: transparent;
  font: 1.55rem/1 var(--sans); cursor: pointer;
}
.definition-modal-close:hover, .definition-modal-close:focus-visible,
.definition-modal-jump:hover, .definition-modal-jump:focus-visible {
  color: var(--text-fg); background: var(--button-hover);
}
.definition-modal-jump { text-decoration: none; }
.definition-modal-jump svg { width: 1.25rem; height: 1.25rem; fill: none;
  stroke: currentColor; stroke-width: 1.8; stroke-linecap: round; stroke-linejoin: round; }
.definition-modal-body {
  flex: 1 1 auto; min-height: 0; padding: 0; overflow: hidden;
  position: relative; background: var(--text-bg); font-family: var(--sans);
}
.definition-modal-loading {
  position: absolute; inset: 0; z-index: 1;
  display: flex; flex-direction: column; align-items: center; justify-content: center;
  gap: 1rem; padding: 2rem; text-align: center;
  color: var(--fg-alt); background: var(--text-bg); font-size: .95rem;
}
.definition-modal-loading-indicator {
  position: relative; display: grid; place-items: center; width: 3rem; height: 3rem;
}
.definition-modal-loading-indicator::before {
  content: ""; position: absolute; inset: 0; border-radius: 50%;
  border: 2px solid color-mix(in srgb, var(--primary) 16%, var(--code-border));
  border-top-color: var(--primary); animation: modal-loading-spin 1s linear infinite;
}
.definition-modal-loading-indicator::after {
  content: "‹/›"; color: var(--primary); font: .85rem var(--mono);
}
@keyframes modal-loading-spin { to { transform: rotate(360deg); } }
.definition-modal-frame {
  display: block; width: 100%; height: 100%; border: 0;
  color-scheme: light dark; background: var(--text-bg);
  opacity: 0; pointer-events: none; transition: opacity .16s ease-out;
}
.definition-modal-frame.is-ready { opacity: 1; pointer-events: auto; }
@media (prefers-reduced-motion: reduce) {
  .definition-modal-loading-indicator::before { animation: none; }
  .definition-modal-frame { transition: none; }
}
/* All devices run the original reading body and behaviours in a frame whose
   reading column is the sole scroll container. */
html.definition-modal-document,
html.definition-modal-document body { height: 100%; overflow: hidden; }
html.definition-modal-document :is(
  #site-header, #nav-backdrop, .skip-link, #toc, #sidenote-container,
  #site-footer
) { display: none !important; }
html.definition-modal-document #section-sticky { top: 0; }
html.definition-modal-document #main-content {
  height: 100%; overflow: auto; overscroll-behavior: contain;
  -webkit-overflow-scrolling: touch; overflow-anchor: none;
  scroll-padding-top: calc(var(--section-nav-height, 0px) + 1rem);
  padding-bottom: calc(3rem + var(--definition-modal-anchor-room, 0px));
}
@media (max-width: 42rem) {
  .definition-modal-backdrop { padding: max(.5rem, env(safe-area-inset-top))
    max(.5rem, env(safe-area-inset-right)) max(.5rem, env(safe-area-inset-bottom))
    max(.5rem, env(safe-area-inset-left)); }
  .definition-modal { width: 100%; height: calc(100dvh - 1rem); min-height: 0;
    max-height: calc(100dvh - 1rem); }
  .definition-modal-header { padding-left: .75rem; }
}

.chapter-heading-row { display: flex; align-items: center; gap: .75rem; margin-bottom: 1rem; }
#section-sticky + .chapter-heading-row { margin-top: 1.25rem; }
.chapter-heading-row > :is(h1, h2) { flex: 1; min-width: 0; margin-block: 0; }
.chapter-review { position: relative; flex: none; margin-inline-start: auto;
  display: inline-flex; align-items: center; justify-content: center;
  width: 2.5rem; height: 2.5rem; border-radius: 50%; cursor: help; }
.chapter-review svg { width: 1.45rem; height: 1.45rem; fill: none;
  stroke: currentColor; stroke-width: 1.7; stroke-linecap: round; stroke-linejoin: round; }
.chapter-review.is-reviewed { color: var(--reviewed-color); }
.chapter-review.is-unreviewed { color: var(--unreviewed-color); }
.chapter-review:focus-visible { outline: 2px solid currentColor; outline-offset: 2px; }
.chapter-review::after { content: attr(data-label); position: absolute;
  z-index: 5; inset-inline-end: 0; top: 100%; width: max-content; max-width: 16rem;
  padding: .4rem .65rem; border: 1px solid var(--code-border); border-radius: 6px;
  color: var(--text-fg); background: var(--code-bg); box-shadow: 0 4px 16px #0002;
  font: .75rem/1.4 var(--sans); pointer-events: none; opacity: 0; }
.chapter-review:is(:hover, :focus)::after { opacity: 1; }

/* Compiler-certified definition ends. Each anchor follows a source line, not
   the frame bottom. CSS line units track font/zoom/fullscreen changes without
   layout observers or geometry reads, and reserve no source row or padding. */
.agda-definition-end {
  position: absolute; inset-inline-end: .65rem;
  top: calc(.8rem + var(--definition-line) * 1lh); height: 1lh; width: 0;
  user-select: none; pointer-events: none;
}
.agda-definition-end::after {
  content: "∎"; position: absolute; right: 0; bottom: -.5rem;
  /* Preserve the former prose-side glyph, not the larger JuliaMono glyph.
     Apply only to the decoration: its anchor must retain the code's 1lh. */
  color: var(--code-fg); opacity: .25; font: 1.05rem/1 var(--sans);
  user-select: none; pointer-events: none;
}

/* ---- math ---- */
.math.display { display: block; overflow-x: auto; margin: 1rem 0; text-align: center; }
/* Shared diagram grammar. Appearance belongs here; chapter markup supplies geometry. */
.book-diagram {
  --diagram-radius: var(--content-frame-radius);
  --diagram-gap: clamp(.75rem, 1.6vw, 1.125rem);
  --diagram-frame-padding: clamp(.8rem, 1.8vw, 1.2rem);
  --diagram-panel-padding: clamp(.7rem, 1.5vw, 1rem);
  --diagram-space-padding: clamp(.5rem, 1vw, .7rem);
  --diagram-path-color: var(--primary);
  --diagram-relation-color: var(--fg-alt);
  --diagram-point-fill: #fff;
  --diagram-frame-border: color-mix(in srgb, var(--code-border) 82%, var(--text-bg));
  --diagram-space-border: color-mix(in srgb, var(--text-fg) 38%, var(--text-bg));
  --diagram-space-bg: color-mix(in srgb, var(--primary) 3%, var(--text-bg));
  box-sizing: border-box;
  max-width: 100%;
  margin: clamp(1.35rem, 2.5vw, 1.75rem) 0 clamp(1.75rem, 3.5vw, 2.35rem);
  scroll-margin-top: 7rem;
  break-inside: avoid;
}
/* Figures scroll with the page; display math must not create nested scroll areas. */
.book-diagram > .diagram-framed {
  box-sizing: border-box; min-width: 0; max-width: 100%;
  padding: var(--diagram-frame-padding);
  border: 1px solid var(--diagram-frame-border); border-radius: var(--diagram-radius);
}
.book-diagram .math.display { overflow: visible; }
.book-diagram .diagram-panel {
  box-sizing: border-box; min-width: 0;
  padding: var(--diagram-panel-padding);
  border: 1px solid var(--diagram-frame-border); border-radius: var(--diagram-radius);
}
.book-diagram .diagram-space {
  box-sizing: border-box; min-width: 0; padding: var(--diagram-space-padding);
  border: 1px solid var(--diagram-space-border); border-radius: var(--diagram-radius);
  background: var(--diagram-space-bg);
}
.book-diagram > figcaption {
  margin: .65rem auto 0; color: var(--fg-alt); font-size: .85em; line-height: 1.55;
  text-align: center; text-wrap: pretty;
}
.book-diagram > figcaption p { margin: 0; }
/* KaTeX assembles stretchy symbols from its own SVG pieces. Leave their sizing alone. */
.book-diagram svg:not(.katex svg) { display: block; width: 100%; height: auto; }
.book-diagram .diagram-path {
  fill: none; stroke: var(--diagram-path-color); stroke-width: 1.6;
  stroke-linecap: round; stroke-linejoin: round;
}
.book-diagram .diagram-point {
  fill: var(--diagram-point-fill); stroke: var(--diagram-path-color); stroke-width: 1;
}
.book-diagram .diagram-map-line, .book-diagram .diagram-map-tip {
  fill: none; stroke: var(--text-fg); stroke-width: 1.3;
  stroke-linecap: round; stroke-linejoin: round;
}
.book-diagram .diagram-guide {
  fill: none; stroke: var(--fg-alt); stroke-width: 1.4; stroke-dasharray: 4 4;
}
/* Logical implication is diagram content, not a navigational link. The
   hlevel-link name is retained as a compatibility alias for existing figures. */
.book-diagram .diagram-implication, .book-diagram .hlevel-link {
  color: var(--diagram-relation-color);
}
.book-diagram .diagram-space-shape {
  fill: var(--diagram-space-bg); stroke: var(--diagram-space-border); stroke-width: 1;
  rx: var(--diagram-radius);
}
.book-diagram .diagram-centre-ring {
  fill: none; stroke: var(--diagram-path-color); stroke-width: 2.5;
}
.book-diagram .diagram-path-space { fill: var(--diagram-path-color); fill-opacity: .12;
  stroke: var(--diagram-space-border); stroke-width: 1; stroke-linejoin: round; }
.book-diagram .diagram-higher-path { fill: var(--diagram-path-color); opacity: .13; }
.book-diagram svg:not(.katex svg) :is(path, circle, rect, line, polyline, polygon, ellipse) {
  vector-effect: non-scaling-stroke;
}
@media (max-width: 480px) {
  .book-diagram {
    --diagram-gap: .65rem;
    --diagram-frame-padding: .65rem;
    --diagram-panel-padding: .6rem;
    --diagram-space-padding: .45rem;
    margin-block: 1.2rem 1.7rem;
  }
  .book-diagram > figcaption { margin-top: .55rem; line-height: 1.5; }
}

.type-comparison-panels { display: grid;
  grid-template-columns: repeat(auto-fit, minmax(min(100%, 19rem), 1fr)); gap: var(--diagram-gap); }
.type-comparison-panel { min-width: 0; }
.type-comparison-panel .math.display { margin: .65rem 0; font-size: .9em; }
.factorization-stage { position: relative; width: min(100%, 31.25rem);
  aspect-ratio: 500 / 230; margin: .35rem auto; }
.factorization-stage > svg { width: 100%; height: 100%; }
.factorization-label { position: absolute; transform: translate(-50%, -50%);
  white-space: nowrap; font-size: clamp(.74rem, 2.5vw, 1rem); }
.factorization-source { left: 10.4%; top: 21.7%; }
.factorization-truncated { left: 71.6%; top: 21.7%; }
.factorization-target { left: 71.6%; top: 82.6%; }
.factorization-top-map { left: 41%; top: 10%; }
.factorization-long-map { left: 35%; top: 68%; }
.factorization-right-map { left: 87%; top: 52%; }
.proposition-proof-panels .type-comparison-panel { display: grid; grid-template-rows: auto auto auto; }
.proposition-proof-panels .type-comparison-panel > .math.display { font-size: .8em; }
.proposition-proof-panels .diagram-space .math.display { font-size: .85em; }
.type-comparison-title { margin: .5rem .25rem .65rem; text-align: center;
  font-family: var(--sans); font-size: .9em; }
.path-figure .katex-display { margin: 0; }
.path-figure .math.display { font-size: .9em; }
.path-operations { display: grid; grid-template-columns: repeat(auto-fit, minmax(min(100%, 15rem), 1fr)); gap: var(--diagram-gap); }
.path-operation { min-width: 0; }
.path-operation p { font-size: .85em; line-height: 1.65; margin: .6rem .2rem; color: var(--fg-alt); }
.path-stage { position: relative; width: 100%; }
.path-stage > svg, .path-connection > svg { display: block; width: 100%; height: 100%; }
.path-label { position: absolute; transform: translate(-50%, -50%); white-space: nowrap; font-size: .85em; }
.diagram-compact-stage { max-width: 26rem; margin: .35rem auto; }
.diagram-compact-stage .path-label { font-size: .78em; }
.fiber-fan-stage { max-width: 42.5rem; margin: .35rem auto; }
.fiber-general .path-label { font-size: clamp(.65rem, 2.1vw, 1rem); }
.fiber-general .fiber-center-label { opacity: 0; }
.fiber-interactive .fiber-fan-stage { cursor: pointer; }
.fiber-interactive .fiber-fan-stage:focus-visible {
  outline: 2px solid var(--primary); outline-offset: 4px; border-radius: var(--diagram-radius); }
.fiber-interactive:not(.fiber-animating) .fiber-hair,
.fiber-interactive:not(.fiber-animating) .fiber-bundle .diagram-point {
  animation: diagram-interaction-stroke-pulse 2.4s ease-in-out infinite; }
.coded-truth-interactive:not(.coded-truth-playing) .coded-truth-source-region {
  animation: diagram-interaction-color-pulse 2.4s ease-in-out infinite; }
@keyframes diagram-interaction-color-pulse {
  0%, 100% { fill: color-mix(in srgb, var(--primary) 4%, var(--text-bg)); }
  50% { fill: color-mix(in srgb, var(--primary) 20%, var(--text-bg)); }
}
@keyframes diagram-interaction-stroke-pulse {
  0%, 100% { stroke: color-mix(in srgb, var(--diagram-path-color) 50%, var(--text-bg)); }
  50% { stroke: var(--diagram-path-color); }
}
@media print {
  .fiber-interactive .fiber-hair,
  .fiber-interactive .fiber-bundle .diagram-point,
  .coded-truth-interactive .coded-truth-source-region { animation: none !important; }
}
.diagram-indexed { max-width: 26rem; margin: auto; }
.diagram-indexed > .math.display { font-size: .8em; }
.vector-slots {
  display: grid; grid-template-columns: repeat(3, minmax(0, 1fr));
  margin: .75rem 3.57143%; border: 1px solid var(--code-border);
  border-radius: var(--diagram-radius); background: var(--code-bg);
}
.vector-slots > span { padding: .45rem; text-align: center; }
.vector-slots > span + span { border-left: 1px solid var(--code-border); }
.path-signature { min-height: 4.3rem; display: grid; align-items: center; }
.path-signature .math.display { margin: .6rem 0; font-size: .63em; }

.path-cong-stage { max-width: 32rem; margin: 1rem auto; }
.subst-factorization { max-width: 42rem; margin: 1rem auto; }
@media (max-width: 600px) {
  .subst-factorization .path-label { font-size: .62em; }
}
.path-connection { position: relative; width: 100%; aspect-ratio: 120 / 54; }
.path-connection-label { position: absolute; left: 50%; top: 21%; transform: translate(-50%, -50%);
  white-space: nowrap; font-size: .8em; }
.funext-scene { display: grid; grid-template-columns: minmax(0, 1fr) 5rem minmax(0, 1fr);
  align-items: center; gap: var(--diagram-gap); max-width: 44rem; margin: .8rem auto; }
.funext-family, .funext-result { min-width: 0; }
.funext-family .math.display, .funext-result .math.display { font-size: .78em; }
.funext-samples { display: grid; grid-template-columns: auto minmax(4rem, 1fr) auto;
  align-items: center; gap: .5rem .3rem; }
.funext-value { text-align: center; font-size: .8em; }
.funext-map { text-align: center; font-size: .8em; }
.funext-down { display: none; }
@media (max-width: 800px) {
  .funext-scene { grid-template-columns: minmax(0, 1fr); }
  .funext-right { display: none; }
  .funext-down { display: inline; }
  .funext-map { padding: .6rem 0; }
  .funext-result .path-stage { max-width: 20rem; margin: auto; }
}
.sigma-pair { position: relative; width: min(100%, 20rem); aspect-ratio: 320 / 130; margin: 1rem auto; }
.sigma-pair > svg { display: block; width: 100%; height: 100%; }
.sigma-component { position: absolute; transform: translate(-50%, -50%); font-size: .9em; white-space: nowrap; }
.sigma-first { left: 23.4375%; top: 13.8462%; }
.sigma-second { left: 76.5625%; top: 13.8462%; }
.sigma-result { left: 50%; top: 88.4615%; }
.structural-figure .katex-display { margin: 0; }
.transport-scene { display: grid;
  grid-template-columns: minmax(0, 1fr) 7.5rem minmax(0, 1fr);
  align-items: center; gap: .55rem 0; max-width: 38rem; margin: .9rem auto; }
.transport-fiber { min-width: 0; }

.transport-family { height: 2rem; width: 0; justify-self: center;
  border-left: 1px dashed var(--fg-alt); }
.level-scene { display: grid; justify-items: center; }
.level-copy, .level-fixed { box-sizing: border-box; max-width: 100%; }
.level-copy { width: min(100%, 20rem); margin-top: .7rem; }
.level-fixed { width: min(100%, 38rem); }
.level-lift { width: 100%; padding: .5rem 0; }
.level-properties { display: grid; grid-template-columns: 1fr auto 1fr auto 1fr;
  align-items: center; gap: .5rem; }
.level-fixed .type-comparison-title { margin-top: 1.2rem; color: var(--fg-alt); }
@media (max-width: 480px) {
  .transport-scene {
    grid-template-columns: minmax(0, 1fr) 4.75rem minmax(0, 1fr);
    gap: .4rem 0; margin: .65rem auto;
  }
  .transport-scene .math.display { font-size: .76em; }
  .level-properties { gap: .2rem; }
  .level-properties .math.display { font-size: .68em; }
}
.resizing-comparison > figcaption { grid-column: 1 / -1; }
.resizing-comparison { display: grid; gap: var(--diagram-gap);
  grid-template-columns: repeat(auto-fit, minmax(min(100%, 24rem), 1fr)); }
.resizing-case { min-width: 0; display: grid; grid-template-rows: auto auto auto 1fr auto; }
.resizing-case .type-comparison-title { font-size: 1em; }
.resizing-note { max-width: 36rem; margin: .5rem auto 1.2rem;
  text-align: center; color: var(--fg-alt); font-size: .9em; }
.resizing-case .math.display { margin: .65rem 0; font-size: .85em; }
.resizing-case .katex-display { margin: 0; }
.resizing-scene { display: grid; grid-template-columns: minmax(0, 1fr) 4rem minmax(0, 1fr);
  align-items: center; align-self: center; gap: .5rem 0; width: 100%; max-width: 34rem; margin: .75rem auto; }

.resizing-bridge { display: flex; align-items: center; }
.resizing-bridge::before, .resizing-bridge::after { content: "";
  flex: 1; border-top: 1px solid var(--primary); }
.resizing-bridge .math.display { flex: none; padding: 0 .25rem; }
.resizing-universe { min-width: 0; }
.resizing-points { display: flex; flex-wrap: wrap; justify-content: center;
  gap: .5rem; padding: .6rem .2rem; }
.resizing-point { border: 1px solid var(--code-border); border-radius: 50%;
  width: 2.4rem; height: 2.4rem; display: grid; place-items: center; }
.resizing-point .math.display { margin: 0; width: 100%; }
.classical-roundtrips { max-width: 46rem; margin: 0 auto; }
.classical-roundtrips .path-label { font-size: .78em; }

.coded-truth-proof-scene { display: grid;
  grid-template-columns: minmax(0, 1fr) 2rem minmax(0, 1.15fr) 2rem minmax(0, 1.8fr);
  align-items: center; gap: var(--diagram-gap); margin: 0 auto; }
.coded-truth-proof-scene .diagram-space { align-self: stretch; }
.coded-truth-proof-scene .coded-truth-proof .path-stage { height: 8rem; display: flex; align-items: center; }
.coded-truth-proof-scene .math.display { margin: .65rem 0; font-size: .8em; }
.coded-truth-proof-scene .coded-truth-universe .math.display { font-size: .7em; color: var(--fg-alt); }
.coded-truth-proof-scene .path-label { font-size: .75em; }
.coded-truth-proof-scene .coded-truth-equivalence { text-align: center; }
.coded-truth-detail-link { text-align: center; font-size: .7em; color: var(--fg-alt); }
.book-diagram .coded-truth-detail-link > .coded-truth-detail-vertical { display: none; }
.coded-truth-expanded { position: relative; z-index: 1; }
.coded-truth-expanded .path-stage > svg { overflow: visible; }
.coded-truth-moving-space { opacity: 0; pointer-events: none; }
.coded-truth-region-label { color: var(--text-fg); }
.coded-truth-playing .coded-truth-detail-link { opacity: .2; }
@media (max-width: 700px) {
  .coded-truth-proof-scene {
    grid-template-columns: minmax(0, 1fr); max-width: 21rem;
    gap: var(--diagram-gap);
  }
  .coded-truth-proof-scene .coded-truth-equivalence { transform: rotate(90deg); }
  .coded-truth-proof-scene .path-stage { max-width: 100%; margin: 0 auto; }
  .coded-truth-proof-scene .coded-truth-proof .path-stage { max-width: 9rem; }
  .coded-truth-detail-link { display: flex; justify-content: center; align-items: center; gap: .75rem; }
  .book-diagram .coded-truth-detail-link > .coded-truth-detail-horizontal { display: none; }
  .book-diagram .coded-truth-detail-link > .coded-truth-detail-vertical { display: block; width: 1.5rem; height: 2.5rem; }
}
.coded-truth-playing .coded-truth-target { opacity: 0; }
.coded-truth-interactive .coded-truth-trigger { cursor: pointer; }
.coded-truth-interactive .coded-truth-trigger:focus-visible {
  outline: 2px solid var(--primary); outline-offset: 4px; border-radius: var(--diagram-radius); }
.coded-truth-interactive .coded-truth-source-region { fill-opacity: 1; }
.coded-truth-playing .coded-truth-source-region { fill-opacity: .12; }
.coded-truth-playing .coded-truth-trigger { cursor: progress; }
@media print { .coded-truth-interactive .coded-truth-source-region { fill-opacity: .12; } }
.hlevel-comparison .katex-display { margin: 0; }
.hlevel-comparison .math.display { font-size: .9em; }
.hlevel-panels { display: grid;
  grid-template-columns: minmax(0, 1fr) 2rem minmax(0, 1fr) 2rem minmax(0, 1fr); gap: .35rem; }
.hlevel-link { align-self: center; justify-self: center; font-size: .9em; }
.hlevel-link-down { display: none; }
.hlevel-panel { min-width: 0; }
.hlevel-panel > .math.display { color: var(--primary); }
.hlevel-assumptions .math.display { font-size: .7em; }
.hlevel-stage { position: relative; width: 100%; aspect-ratio: 240 / 150; }
.hlevel-stage > svg { display: block; width: 100%; height: 100%; overflow: visible; }
.hlevel-label { position: absolute; transform: translate(-50%, -50%); white-space: nowrap;
  font-size: .85em; }
.hlevel-definition { min-height: 4.3rem; display: grid; align-items: center; }
.hlevel-definition .math.display { margin: .8rem 0; font-size: .68em; }
.hlevel-note { margin: .5rem .2rem; color: var(--fg-alt); font-size: .85em; line-height: 1.65; }
@media (max-width: 800px) {
  .hlevel-panels { grid-template-columns: minmax(0, 1fr); gap: var(--diagram-gap); }
  .hlevel-link-right { display: none; }
  .hlevel-link-down { display: inline; }
}
@media (max-width: 480px) {
  .resizing-scene { grid-template-columns: minmax(0, 1fr) 3rem minmax(0, 1fr); }
  .resizing-label .math.display, .resizing-universe > .math.display { font-size: .72em; }
}

/* ---- footer ---- */
#site-footer { margin-top: 4rem;
  padding: 1.5rem 1rem; font-family: var(--sans); font-size: 0.85rem;
  color: var(--fg-alt); text-align: center; }
#site-footer a { color: var(--link-color); text-decoration: none; }
#site-footer .footer-copyright { margin-top: 0.35rem; font-size: 0.8rem; opacity: 0.9; }
@media (max-width: 48rem) {
  #site-footer { padding-bottom: calc(7.5rem + env(safe-area-inset-bottom)); }
}

#code-note-toast { position: fixed; z-index: 60; width: min(24rem, calc(100vw - 1.25rem));
  padding: .8rem 2.5rem .8rem .9rem; color: var(--text-fg); background: var(--popup-bg);
  border: 1px solid var(--primary); border-radius: 9px;
  box-shadow: 0 8px 28px rgba(0,0,0,.32); font-size: .92rem; line-height: 1.5;
  overflow-y: auto; overscroll-behavior: contain; }
#code-note-toast::before { position: absolute; left: var(--note-arrow-x, 50%); width: .72rem; height: .72rem;
  content: ""; background: var(--popup-bg); border: solid var(--primary); transform: translateX(-50%) rotate(45deg); }
#code-note-toast[data-side="below"]::before { top: -.42rem; border-width: 1px 0 0 1px; }
#code-note-toast[data-side="above"]::before { bottom: -.42rem; border-width: 0 1px 1px 0; }
#code-note-toast a { color: var(--link-color); text-decoration: underline; }
#code-note-toast .Agda { display: inline; padding: .08em .28em;
  color: var(--code-fg); background: var(--code-inline-bg);
  border: 1px solid var(--code-border); border-radius: 4px;
  font-family: var(--mono); font-size: .9em; white-space: nowrap; }
#code-note-toast .Agda a { text-decoration: none; }
#code-note-toast .Agda a:hover { text-decoration: underline; }
#code-note-toast .Agda :is(.Comment, .Markup, .Pragma) { color: var(--code-comment); }
#code-note-toast .Agda .Keyword { color: var(--code-keyword); }
#code-note-toast .Agda .String { color: var(--code-string); }
#code-note-toast .Agda .Number { color: var(--code-number); }
#code-note-toast .Agda :is(.Symbol, .Bound, .Generalizable) { color: var(--code-fg); }
#code-note-toast .Agda :is(.InductiveConstructor, .CoinductiveConstructor) { color: var(--code-constructor); }
#code-note-toast .Agda .Field { color: var(--code-field); }
#code-note-toast .Agda .Module { color: var(--code-module); }
#code-note-toast .Agda :is(.Datatype, .Function, .Postulate, .Primitive, .Record, .PrimitiveType) {
  color: var(--code-identifier); }
#code-note-toast .Agda .Macro { color: var(--code-macro); }
.code-note-close { position: absolute; top: .3rem; right: .35rem; display: grid; place-items: center;
  width: 2rem; height: 2rem; padding: 0; border: 0; border-radius: 6px;
  color: var(--fg-alt); background: transparent; font: 1.35rem/1 var(--sans); cursor: pointer; }
.code-note-close:hover { color: var(--text-fg); background: var(--button-hover); }

/* Reader-facing terms link back to the section that formally introduces them. */
.term-ref, .term-intro { text-decoration-line: underline; text-decoration-style: dotted;
  text-decoration-thickness: 1px; text-underline-offset: .18em;
  text-decoration-color: color-mix(in srgb, var(--primary) 60%, transparent); }
.term-ref { color: inherit; }
.term-intro { color: inherit; font-style: normal; font-weight: inherit; cursor: help; }
.term-ref:hover, .term-ref:focus-visible, .term-intro:hover, .term-intro:focus-visible {
  color: var(--primary); text-decoration-style: solid; }
#term-popup { position: fixed; z-index: 75; width: min(22rem, calc(100vw - 1.25rem));
  padding: .75rem 2.45rem .75rem .85rem; color: var(--text-fg); background: var(--popup-bg);
  border: 1px solid color-mix(in srgb, var(--primary) 75%, var(--ruler)); border-radius: 9px;
  box-shadow: 0 8px 26px rgba(0,0,0,.3); font-size: .9rem; line-height: 1.45; }
#term-popup::before { position: absolute; left: var(--term-arrow-x, 50%); width: .65rem; height: .65rem;
  content: ""; background: var(--popup-bg); border: solid var(--primary);
  transform: translateX(-50%) rotate(45deg); }
#term-popup[data-side="below"]::before { top: -.38rem; border-width: 1px 0 0 1px; }
#term-popup[data-side="above"]::before { bottom: -.38rem; border-width: 0 1px 1px 0; }
#term-popup .term-popup-name { display: block; margin-bottom: .25rem; color: var(--primary); }
#term-popup p { margin: .2rem 0 .45rem; }
#term-popup a { color: var(--link-color); font-size: .88em; text-decoration: none; }
#term-popup a:hover { text-decoration: underline; }
#term-popup .term-popup-close { position: absolute; top: .25rem; right: .3rem; display: grid;
  place-items: center; width: 1.8rem; height: 1.8rem; padding: 0; border: 0;
  border-radius: 5px; color: var(--fg-alt); background: transparent;
  font: 1.2rem/1 var(--sans); cursor: pointer; }
#term-popup .term-popup-close:hover, #term-popup .term-popup-close:focus-visible {
  color: var(--text-fg); background: var(--button-hover); }

/* ---- layouts without room for both centered text and margin notes ---- */
@media (max-width: 78.999rem) {
  .single-line-code { display: block; text-align: center; }
  .single-line-code[data-note]::before, .single-line-code-note,
  .prose-annotation-connector, .prose-annotation-note { display: none; }
  .single-line-code[data-note] > code, .prose-annotation-target { cursor: pointer; }
}

/* Below the full three-column width, navigation becomes a drawer. Notes remain
   in the right margin where space allows, then open in a toast on narrower screens. */
@media (max-width: 79.999rem) {
  #search-box { width: 8rem; }

  #toc-drawer-head { display: flex; }

  #toc {
    display: block; position: fixed; top: var(--site-header-height, 3.5rem); left: 0; bottom: 0;
    width: min(20rem, 82vw); max-width: 20rem; max-height: none; justify-self: auto;
    padding: 0.85rem 1.1rem 1.5rem; background: var(--text-bg);
    box-shadow: 2px 0 18px rgba(0, 0, 0, 0.22);
    overflow-y: auto; -webkit-overflow-scrolling: touch; z-index: 40;
    transform: translateX(-100%); visibility: hidden;
    transition: transform 0.22s ease, visibility 0s linear 0.22s;
  }
  body.nav-open #toc {
    transform: translateX(0); visibility: visible;
    transition: transform 0.22s ease, visibility 0s;
  }

  #nav-backdrop {
    display: block; position: fixed; top: var(--site-header-height, 3.5rem);
    right: 0; bottom: 0; left: 0; z-index: 30;
    background: rgba(0, 0, 0, 0.4); opacity: 0; pointer-events: none;
    transition: opacity 0.22s ease;
  }
  body.nav-open #nav-backdrop { opacity: 1; pointer-events: auto; }
}

@media (min-width: 80rem) {
  #toc-collapse { display: inline-flex; }
  body.nav-collapsed #toc { display: none; }
  body.nav-collapsed #post-toc-container {
    /* Keep the empty left track opposite the note gutter. This preserves the
       article's centre line and prevents a horizontal jump when the TOC hides. */
    grid-template-areas: ". content gutter";
  }
}

.header-disclosure { display: none; }
/* Explicit controls: scrolling never changes compact header visibility. */
@media (max-width: 42rem) {
  #topbar { position: relative; gap: .25rem;
    padding-inline-end: max(.25rem, env(safe-area-inset-right)); }
  .header-disclosure {
    display: inline-flex; align-items: center; justify-content: center; flex: none;
    width: 44px; height: 44px; border: 1px solid transparent; border-radius: 8px;
    background: transparent; color: var(--fg-alt); cursor: pointer;
  }
  .header-disclosure svg { width: 22px; height: 22px; fill: none;
    stroke: currentColor; stroke-width: 1.7; stroke-linecap: round; stroke-linejoin: round; }
  .header-disclosure:hover, .header-disclosure[aria-expanded="true"] {
    background: var(--button-hover); color: var(--text-fg);
  }
  #topbar :is(.header-disclosure, #theme-toggle):focus-visible {
    outline-offset: 2px; /* Keep the focus ring inside the narrower edge gutter. */
  }
  #topbar :is(.search-form, #lang-switch) {
    position: absolute; top: calc(100% + .35rem); right: .65rem; margin: 0;
    padding: .65rem; background: var(--popup-bg); border: 1px solid var(--input-border);
    border-radius: 10px; box-shadow: var(--shadow-float); z-index: 1;
    opacity: 0; visibility: hidden; pointer-events: none; transform: translateY(-4px);
    transition: opacity .12s ease, transform .12s ease, visibility 0s .12s;
  }
  #topbar .search-form { left: .65rem; }
  #topbar #lang-switch { gap: .5rem; font-size: 1rem; }
  #topbar #lang-switch :is(a, .cur) { padding-inline: .6rem; }
  #topbar :is(.search-form, #lang-switch).header-panel-open {
    opacity: 1; visibility: visible; pointer-events: auto; transform: none;
    transition-delay: 0s;
  }
  #topbar #search-box { width: 100%; max-width: none; min-height: 44px; }
  #topbar #search-results { width: 100%; max-width: none; }
}
@media (prefers-reduced-motion: reduce) {
  #topbar :is(.search-form, #lang-switch) { transition: none; }
}

/* A reading surface, with navigation kept separate from the mathematical text. */
:root { --primary: #285fa5; --font-size: 1.125rem; --code-font-size: 1rem; }
html.theme-dark { --primary: #81b5eb; }
@media (prefers-color-scheme: dark) {
  html:not(.theme-light) { --primary: #81b5eb; }
}
article, html[lang="zh"] article, html[lang="ja"] article { line-height: 1.7; }
article h1 { font-size: clamp(1.7rem, 3vw, 2.35rem); line-height: 1.28; text-wrap: balance; margin-bottom: 1rem; }
article h2 { line-height: 1.35; }
/* The content grid sets the reading width; paragraphs reflow within that column. */
/* Native language-aware wrapping supplies the first pass. The reader then
   applies only bounded, measured tracking to exceptional CJK lines. */
article p { text-wrap: pretty; }
html:is([lang="zh"], [lang="ja"]) article p { line-break: strict; }
article p.punctuation-tracking { letter-spacing: var(--punctuation-tracking); }
article p.punctuation-tracking :is(.Agda, .katex, .math) { letter-spacing: normal; }
@media (max-width: 640px) {
  /* Pretty wrapping can leave wide gaps around unbreakable code/term links in
     a narrow reading column. Let the browser use its ordinary line breaks. */
  article p { text-wrap: wrap; }
  html:is([lang="zh"], [lang="ja"]) article p { line-break: normal; }
}
button, summary, a, select { -webkit-tap-highlight-color: transparent; }
:where(button, a, summary, select, input):focus-visible { outline: 2px solid var(--primary); outline-offset: 4px; }
[hidden] { display: none !important; }
.skip-link { position: fixed; left: 1rem; top: -5rem; z-index: 100; padding: .6rem 1rem; background: var(--text-bg); color: var(--link-color); }
.skip-link:focus { top: .5rem; }
.localized-fallback { border-left: 2px solid var(--input-border); margin: .9rem 0; padding: .25rem 0 .25rem .8rem; font-size: .9rem; color: var(--fg-alt); }
.localized-fallback > summary { cursor: pointer; font-family: var(--sans); font-size: .78rem; padding-block: .3rem; }
.localized-fallback[open] { padding-right: .75rem; }
.localized-fallback > :not(summary) { line-height: 1.65; }
.book-intro { padding: 1.1rem 0 1.4rem; max-width: 54rem; }
.book-intro[data-home-title] { padding-bottom: .35rem; }
.book-intro h1 { margin: 0 0 .6rem; }
.book-intro p { margin: 0; color: var(--fg-alt); font-size: 1rem; line-height: 1.65; }
.sr-only { position: absolute; width: 1px; height: 1px; padding: 0; margin: -1px; overflow: hidden; clip: rect(0, 0, 0, 0); white-space: nowrap; border: 0; }
[data-home-intro] .book-intro-lead { max-width: 54rem; margin: 0 0 1.2rem; color: var(--text-fg); font-size: 1.1rem; line-height: 1.65; }
[data-home-intro] .book-tagline { margin: -.25rem 0 .45rem; color: var(--fg-alt); font-size: 1rem;
  font-style: italic; line-height: 1.65; }
.book-tabs { display: grid; grid-template-columns: repeat(4, minmax(0, 1fr)); gap: .3rem; padding: .3rem; border: 1px solid var(--input-border); border-radius: 14px; margin-bottom: 1.5rem; background: color-mix(in srgb, var(--code-bg) 72%, var(--text-bg)); font: 700 .9rem var(--sans); box-shadow: 0 8px 24px color-mix(in srgb, var(--text-fg) 6%, transparent); }
.book-tabs a { display: block; padding: .72rem .55rem; color: var(--fg-alt); border: 1px solid transparent; border-radius: 10px; text-align: center; text-decoration: none; white-space: nowrap; transition: color .15s, background .15s, border-color .15s, box-shadow .15s; }
.book-tabs a[aria-selected="true"] { color: var(--primary); border-color: color-mix(in srgb, var(--primary) 32%, var(--input-border)); background: var(--text-bg); box-shadow: 0 3px 10px color-mix(in srgb, var(--text-fg) 9%, transparent); }
.book-tabs a:hover { color: var(--primary); background: color-mix(in srgb, var(--button-hover) 70%, transparent); }
.book-panels > section { scroll-margin-top: 7rem; }
.book-panels > section:focus-visible { outline-offset: 5px; }
.guide-landmark { width: 100%; max-width: none; }
.term-glossary-panel { width: 100%; max-width: none; }
.button-link { display: inline-block; padding: .55rem .8rem; border: 1px solid var(--input-border); border-radius: 6px; text-decoration: none; }
.button-link:hover { border-color: var(--primary); background: var(--button-hover); }
.term-glossary-head { display: flex; align-items: end; justify-content: space-between; gap: 1rem; margin: .25rem 0 1rem; padding-bottom: 1rem; border-bottom: 1px solid var(--input-border); }
.term-glossary-head p { max-width: 58ch; margin: 0; color: var(--fg-alt); line-height: 1.55; }
.term-glossary-search { flex: 0 1 15rem; }
.term-glossary-search input { width: 100%; box-sizing: border-box; padding: .6rem .75rem; border: 1px solid var(--input-border); border-radius: 999px; background: var(--text-bg); color: var(--text-fg); font: inherit; }
.term-glossary-search input:focus-visible { outline: 3px solid color-mix(in srgb, var(--primary) 42%, transparent); outline-offset: 2px; border-color: var(--primary); }
.term-glossary-list { display: grid; gap: .65rem; margin: 0; }
.term-entry { display: grid; grid-template-columns: 2.3rem minmax(9rem, 15rem) 1fr; gap: .75rem; align-items: baseline; padding: .85rem 1rem; border: 1px solid var(--input-border); border-radius: 11px; background: color-mix(in srgb, var(--code-bg) 40%, var(--text-bg)); transition: border-color .15s, transform .15s, box-shadow .15s; }
.term-entry:hover { border-color: color-mix(in srgb, var(--primary) 45%, var(--input-border)); transform: translateY(-1px); box-shadow: 0 6px 16px color-mix(in srgb, var(--text-fg) 7%, transparent); }
.term-entry[hidden] { display: none; }
.term-index { color: var(--fg-alt); font: 700 .72rem var(--mono); font-variant-numeric: tabular-nums; }
.term-glossary-list dt { margin: 0; font-weight: 700; }
.term-glossary-list dt a { color: var(--link-color); text-decoration: none; }
.term-glossary-list dt a:hover { text-decoration: underline; }
.term-abbreviation { color: var(--fg-alt); font-weight: 500; white-space: nowrap; }
.term-glossary-list dd { margin: 0; color: var(--fg-alt); line-height: 1.6; }
.term-glossary-empty { margin: 1rem 0 0; color: var(--fg-alt); font-style: italic; }
@media (max-width: 40rem) {
  .book-intro { padding-top: .4rem; padding-bottom: 1rem; }
  .book-tabs { grid-template-columns: repeat(2, minmax(0, 1fr)); gap: .25rem; font-size: .87rem; }
  .book-tabs a { padding-inline: .1rem; }
  .book-intro p { font-size: .93rem; }
  [data-home-intro] .book-tagline { font-size: .93rem; }
  [data-home-intro] .book-intro-lead { font-size: 1rem; }
  .term-glossary-head { display: grid; align-items: start; }
  .term-glossary-search { width: 100%; }
  .term-entry { grid-template-columns: 2rem 1fr; gap: .35rem .65rem; }
  .term-entry dt, .term-entry dd { grid-column: 2; }
  .term-entry dd { margin-top: -.1rem; }
}

@media (max-width: 60rem) {
  #toc { width: min(20rem, 88vw); padding: 1rem .8rem 1.5rem; }
  #toc-drawer-head { padding: 0 .5rem .8rem; margin-bottom: .8rem; border-bottom: 1px solid var(--ruler); }
  #toc-drawer-head .drawer-title { font-size: .9rem; color: var(--text-fg); }
  #toc :is(a, summary) { min-height: 44px; box-sizing: border-box; }
  #toc .toc-branch > summary > a { max-width: calc(100% - 44px);
    display: flex; align-items: center; }
  #toc-container { padding-right: .2rem; }
  #nav-close { min-width: 44px; min-height: 44px; border-radius: 6px; }
}