:root { --proof: #f4f5f0; }
.supplementary-page { --accent: #315b7a; background: #edf3f8; }
.supplementary-page .notes-page { background: #fafdff; border-left: .3rem solid #668ca8; }
.ai-notice { max-width: 760px; font: .9rem/1.6 system-ui,sans-serif; color: #31516a; }
.ai-label { display: inline-block; margin-left: .4rem; font: .72rem/1.5 system-ui,sans-serif; color: #31516a; }
.supplementary-links { margin-top: 2rem; padding-top: 1rem; border-top: 1px solid var(--rule); }
.notes-page .supplementary-links h2 { font-size: 1.2rem; }
.supplementary-targets { margin-top: 2rem; font-size: .9rem; }
.reader-explanations { font: .75rem/1.5 system-ui,sans-serif; padding: .5rem .9rem; }
.reader-explanations a { display: inline-block; margin-right: .7rem; }
@media print { .supplementary-page .eyebrow, .ai-notice { color: black; } }
.site-header { max-width: 1120px; width: calc(100% - 3rem); padding: 3rem 0 2rem; }
.site-header h1 { max-width: 900px; font-size: clamp(2rem,4.5vw,3.1rem); }
.reader-grid { display: grid; grid-template-columns: 220px minmax(0, 820px); gap: 2rem; max-width: 1120px; margin: 0 auto; padding: 0 1.5rem; align-items: start; }
.notes-page { width: 100%; min-width: 0; margin: 0; padding: 2.3rem 2.8rem; background: var(--paper); border: 1px solid var(--rule); border-radius: .4rem; box-shadow: 0 12px 35px #20251f06; }
.reader-nav { position: static; font: .87rem/1.5 system-ui,sans-serif; }
.reader-nav > h2 { margin: 0; font: 650 .87rem/1.5 system-ui,sans-serif; }
.reader-nav .reader-resources { gap: .1rem; padding-bottom: 1rem; border-bottom: 1px solid var(--rule); }
.reader-resources a { padding-block: .3rem; }
.text-button { padding: 0; border: 0; background: none; color: var(--accent); font: inherit; text-decoration: underline; cursor: pointer; }
.agda-invitation { display: none; }
.hide-agda-links .agda-invitation { display: inline; }
.hide-agda-links .agda-instructions { display: none; }
.reader-nav nav { display: grid; gap: .35rem; margin: .8rem 0 1.4rem; }
.reader-nav nav a { display: block; padding: .6rem .7rem; text-decoration: none; border-radius: .3rem; }
.reader-nav a[aria-current] { background: #e2eae2; font-weight: 650; }
.reader-nav summary { font-weight: 650; }
.contents-chapter { border-block: 1px solid var(--rule); padding-block: .35rem; }
.contents-chapter + .contents-chapter { border-top: 0; }
.contents-chapter > summary { padding: .55rem .35rem; }
.chapter-number { font-size: .8rem; }
.chapter-name { display: block; margin: .25rem 0 0 1rem; font-weight: 500; line-height: 1.4; }
.chapter-sections { display: grid; gap: .2rem; margin: .4rem 0 .65rem .5rem; border-left: 1px solid var(--rule); padding-left: .35rem; }
.chapter-sections a { font-size: .8rem; }
.utility-dock { position: fixed; z-index: 50; top: 1rem; left: max(1rem,env(safe-area-inset-left)); display: flex; gap: .4rem; font-family: system-ui,sans-serif; }
.utility-button { display: grid; place-items: center; width: 2.55rem; height: 2.55rem; padding: 0; border: 1px solid var(--rule); border-radius: 50%; background: #fffef9f5; color: var(--accent); box-shadow: 0 .35rem 1.2rem #2d342c1a; font: 1.25rem/1 "Segoe UI Symbol",system-ui,sans-serif; text-decoration: none; cursor: pointer; }
.utility-button:hover, .utility-button[aria-expanded="true"] { background: var(--accent); color: white; border-color: var(--accent); }
.settings-panel { position: absolute; left: 0; top: calc(100% + .55rem); width: min(19rem,calc(100vw - 2rem)); max-height: calc(100dvh - 6rem); overflow-y: auto; padding: 1rem; border: 1px solid var(--rule); border-radius: .55rem; background: #fffef9; box-shadow: 0 .75rem 2.5rem #2d342c24; color: var(--ink); font: .85rem/1.5 system-ui,sans-serif; }
.settings-panel h2 { font: 700 .9rem/1.5 system-ui,sans-serif; margin: 0 0 .8rem; }
.settings-panel label { display: flex; align-items: center; gap: .55rem; margin: .8rem 0; cursor: pointer; }
.settings-panel input { width: 1rem; height: 1rem; margin: 0; accent-color: var(--accent); flex-shrink: 0; }
.utility-dock ~ .site-header { padding-top: 5rem; }
footer { max-width: 1120px; width: calc(100% - 3rem); padding: 2rem 0; font: .75rem/1.5 system-ui,sans-serif; color: var(--muted); }
.notes-page h2 { font-size: 1.7rem; margin: 2rem 0 1rem; line-height: 1.2; }
.notes-page h3 { font-size: 1.45rem; margin: 2rem 0 1rem; line-height: 1.25; }
.notes-page h4 { font-size: 1.16rem; margin: 1.7rem 0 .8rem; line-height: 1.3; }
.notes-page h5 { font-size: 1rem; margin: 1.5rem 0 .8rem; }
.notes-page > .sectionHead:first-child, .notes-page > .chapterHead:first-child { margin-top: 0; }
.notes-page p { margin: .9rem 0; }
.notes-page p:empty { display: none; }
.titlemark { margin-right: .3em; }
[class*="Italic"] { font-style: italic; }
[class*="Bold"] { font-weight: 700; }
.underline { text-decoration: underline; text-underline-offset: .2em; }
.source-anchor { scroll-margin-top: 2rem; }
.Agda a:target { background: #e3efcb; outline: 1px solid #8d9f68; }
.statement { margin: 1.35rem 0; padding: .9rem 1.1rem; border-left: 3px solid #a8b9b8; background: #f3f6f1; }
.statement p:first-child { margin-top: 0; }
.statement p:last-child { margin-bottom: 0; }
.newtheorem .head { display: inline; }
.framedenv { margin: 1.3rem 0; }
.framedenv .statement { background: #eef2ed; border-color: #829a86; }
.framedenv > blockquote { padding: .8rem 1rem; margin: 0; border: 1px solid var(--rule); }
.book-proof { background: var(--proof); border-left: 2px solid #c9cdc2; margin: 1rem 0 1.7rem; padding: .7rem 1rem; }
.book-proof > summary { font-style: italic; }
.proof-content .head { display: none; }
summary { cursor: pointer; }
summary:hover { color: var(--accent); }
:focus-visible { outline: 2px solid var(--accent); outline-offset: 4px; }
.skip-link { position: absolute; top: -5rem; left: 1rem; padding: .8rem; background: white; z-index: 100; }
.skip-link:focus { top: 1rem; }
.diagram { position: relative; margin: 1.4rem 0; text-align: center; overflow-x: auto; }
.diagram img { max-width: 100%; height: auto; }
.diagram details { font: .72rem/1.4 system-ui,sans-serif; text-align: left; margin-top: .5rem; color: var(--muted); }
.diagram details pre { font-size: .73rem; }
dl.enumerate { margin: .9rem 0; }
dt.enumerate { float: left; clear: left; margin-right: .45rem; }
dd.enumerate { margin-left: 1.7rem; margin-bottom: .8rem; }
li { margin: .5rem 0; }
.agda-panel { margin: 1rem 0 .4rem; border-top: 1px solid #cedbd2; padding-top: .65rem; font-style: normal; scroll-margin-top: 1rem; }
.agda-panel > summary { font: .8rem/1.5 system-ui,sans-serif; color: var(--accent); }
.agda-tag { font: 650 .7rem/1.3 system-ui,sans-serif; letter-spacing: .025em; background: #e0ebe5; border: 1px solid #b8ccc0; padding: .14rem .35rem; border-radius: .22rem; white-space: nowrap; }
.agda-content { margin-top: .8rem; padding: .2rem 0; font: .86rem/1.55 system-ui,sans-serif; }
.agda-content .scope-note { color: #58645c; font-size: .75rem; border-left: 2px solid #bdcec3; padding-left: .6rem; }
.agda-content h4 { margin: 1.2rem 0 .5rem; font-size: .87rem; overflow-wrap: anywhere; }
.agda-declaration { border-bottom: 1px solid var(--rule); padding-bottom: .9rem; }
.agda-declaration:last-child { border-bottom: 0; }
.status { font-size: .7rem; color: #3c5c48; font-weight: 650; }
pre, pre.Agda { max-width: 100%; overflow: auto; padding: .85rem; background: #fffefa; border: 1px solid #e1e5dc; border-radius: .25rem; font: .79rem/1.6 "Cascadia Code","DejaVu Sans Mono",Consolas,monospace; tab-size: 2; text-align: left; }
pre.Agda a { text-decoration: none; }
pre.Agda a:hover { background: #e5ede2; }
pre.Agda .Background, pre.Agda .Markup { color: #64695f; }
.source-links, .permalink { font-size: .72rem; }
.agda-proof, .module-context, .supporting { margin: .6rem 0; }
.module-context pre { max-height: 23rem; }
.copy-code { display: block; margin: .3rem 0 .6rem auto; border: 1px solid var(--rule); color: var(--accent); border-radius: .2rem; background: white; padding: .3rem .5rem; font-size: .7rem; cursor: pointer; }
.chapter-card-grid { display: grid; grid-template-columns: repeat(2,minmax(0,1fr)); gap: 1rem; margin: 1.8rem 0; }
.chapter-card { padding: 1.2rem; border: 1px solid var(--rule); background: #f7f8f3; border-radius: .25rem; }
.chapter-card h2, .chapter-card h3 { margin: .5rem 0; font-size: 1.3rem; line-height: 1.2; }
.overview-chapter { border-block: 1px solid var(--rule); }
.overview-chapter + .overview-chapter { border-top: 0; }
.overview-chapter > summary { padding: 1rem 0; }
.overview-chapter > summary h2 { display: inline; margin: 0; font-size: 1.45rem; line-height: 1.4; }
.overview-chapter .chapter-card-grid { margin: 1rem 0 1.5rem; }
.overview-chapter .chapter-card h3 a { color: var(--accent); text-decoration: underline; }
.chapter-card p { font-size: .9rem; }
.available-sections { margin-top: 2.5rem; }
.section-card-grid { display: grid; grid-template-columns: repeat(2,minmax(0,1fr)); gap: .8rem; }
.section-card { display: flex; min-height: 11rem; padding: 1.2rem; flex-direction: column; border: 1px solid var(--rule); border-radius: .5rem; background: #fff; }
.notes-page .section-card-meta { margin: 0; color: var(--accent); font: 750 .7rem/1.5 system-ui,sans-serif; letter-spacing: .06em; text-transform: uppercase; }
.notes-page .section-card h3 { margin: .5rem 0 0; font-size: 1.2rem; line-height: 1.25; }
.section-card h3 a { color: var(--ink); text-decoration: none; }
.section-card h3 a:hover, .section-card h3 a:focus-visible { color: var(--accent); text-decoration: underline; }
.section-card > p:not(.section-card-meta) { color: var(--muted); font-size: .9rem; }
.header-top { display: flex; align-items: flex-start; justify-content: space-between; gap: 1rem; flex-wrap: wrap; margin-bottom: 1.5rem; }
.header-top .collection-return { margin-bottom: 0; }
.book-breadcrumbs { flex: 1 1 20rem; font: 650 .73rem/1.7 system-ui,sans-serif; letter-spacing: .045em; text-transform: uppercase; color: var(--muted); }
.book-breadcrumbs ol { display: flex; flex-wrap: wrap; gap: .4rem .65rem; list-style: none; margin: 0; padding: 0; }
.book-breadcrumbs li { margin: 0; }
.book-breadcrumbs li + li::before { content: '·'; margin-right: .65rem; color: var(--muted); }
.book-breadcrumbs a { color: var(--accent); text-decoration-thickness: 1px; text-underline-offset: .22em; }
.page-turns { display: grid; grid-template-columns: repeat(2,minmax(0,1fr)); gap: .55rem; width: min(100%,22rem); flex-shrink: 0; margin-left: auto; font: .8rem/1.35 system-ui,sans-serif; }
.page-turns a, .page-turns button { display: grid; gap: .15rem; min-width: 0; padding: .65rem .9rem; border: 1px solid var(--rule); border-radius: .4rem; background: var(--paper); color: inherit; font: inherit; text-align: left; text-decoration: none; }
.page-turns a:hover { background: #eaf0e8; border-color: var(--accent); }
.page-turns button:disabled { background: transparent; color: var(--muted); opacity: .65; }
.turn-direction { color: var(--muted); font-size: .72rem; }
.turn-target { font-weight: 650; }
@media (max-width: 620px) { .section-card-grid { grid-template-columns: 1fr; } .section-card { min-height: 0; } }
.module-caption { font: .85rem/1.5 system-ui,sans-serif; color: var(--muted); }
body:has(.module-caption) .site-header h1 { font-size: 1.5rem; overflow-wrap: anywhere; }
.notes-page table { border-collapse: collapse; width: 100%; font-size: .9rem; }
.notes-page th, .notes-page td { padding: .6rem; border-bottom: 1px solid var(--rule); text-align: left; vertical-align: top; }
mjx-container[display="true"] { overflow-x: auto; overflow-y: hidden; max-width: 100%; padding-block: .25rem; }
@media (max-width: 850px) { .reader-grid { display: block; } .reader-nav { margin-bottom: 1.5rem; } .reader-nav nav { grid-template-columns: 1fr; } .notes-page { padding: 1.5rem; } }
@media (max-width: 500px) { body { font-size: 16px; } .reader-grid { padding: 0 .6rem; } .notes-page { padding: 1.1rem .8rem; } .site-header { width: calc(100% - 2rem); padding-top: 2rem; } .chapter-card-grid { grid-template-columns: 1fr; } .statement { padding: .8rem; } pre, pre.Agda { font-size: .72rem; } dd.enumerate { margin-left: 1.3rem; } }
@media (prefers-reduced-motion: reduce) { html { scroll-behavior: auto; } }
@media print { .reader-nav, .utility-dock, .agda-panel, .copy-code, .page-turns, .skip-link { display: none; } .reader-grid { display: block; padding: 0; } .notes-page { border: 0; box-shadow: none; } }
/* Phrase links stay quiet while all code is closed by default. */
.agda-trigger { color: inherit; text-decoration: underline dotted; text-decoration-color: #75908f; text-underline-offset: .22em; }
.agda-trigger:hover, .agda-trigger:focus-visible { color: #17615d; background: #edf5f2; }
.agda-inline:not([open]):not(:target) { display: none; }
.agda-inline { scroll-margin-top: 1rem; }
.code-index-entry { border-bottom: 1px solid #dce3df; padding: .7rem 0; }
.code-index-entry h3 { font-size: 1rem; overflow-wrap: anywhere; margin: .3rem 0; }
.module-qualified { font: .7rem/1.5 monospace; color: #526b62; overflow-wrap: anywhere; }
.module-group { margin: .6rem 0; border: 1px solid #dce3df; border-radius: .3rem; }
.module-group > summary { padding: .65rem .8rem; cursor: pointer; font-weight: 600; }
.module-group > summary:hover { background: #edf5f2; }
.module-group-content { padding: 0 .8rem .5rem; }
.module-group .module-group { border-width: 0 0 0 2px; border-radius: 0; }
.module-group summary:focus-visible, .module-picker:focus-visible, .module-choice:focus-visible { outline: 2px solid #17615d; outline-offset: 2px; }
.code-search { display: block; margin: 1.5rem 0; }
.code-search input { display: block; width: 100%; padding: .7rem; font: inherit; border: 1px solid #8a9f99; border-radius: .3rem; }
.symbol-entry { overflow-wrap: anywhere; }
[hidden] { display: none !important; }
@media print { .agda-inline { display: none !important; } .agda-trigger { text-decoration: none; } }
.agda-help { font: .78rem/1.5 system-ui, sans-serif; color: #526b62; padding-bottom: .7rem; border-bottom: 1px solid var(--rule); }
.agda-content > .agda-declaration { padding-bottom: .45rem; }
.agda-declaration > h4 { display: inline; margin: 0 .7rem 0 0; }
.agda-declaration > .status { display: inline; font-size: .67rem; }
.mapping-note { margin: .55rem 0; font-size: .75rem; }
.panel-return { font-size: .75rem; }
/* The side reader never participates in the manuscript's paragraph flow. */
.side-reader-ready .agda-inline { display: none !important; }
.agda-trigger.is-active { background: #e0eee5; text-decoration-style: solid; color: #145b47; }
.agda-book-anchor.is-active { background: #e0eee5; }
.reader-backlink { padding: .4rem 1rem; border-top: 1px solid #e2e7df; font-size: .66rem; color: #53695b; }
.book-picker { display: block; max-width: 100%; font: inherit; margin-top: .3rem; }
.book-picker[hidden] { display: none; }
button.line-number { font: inherit; border: 0; padding-left: 0; background: transparent; cursor: pointer; }
button.line-number:hover, button.line-number:focus-visible { opacity: 1; color: #145b47; }
.agda-reader { position: fixed; z-index: 30; top: 1rem; right: 1rem; bottom: 1rem; width: var(--rail-width, 440px); background: #fffefa; border: 1px solid #d4dcd3; border-radius: .5rem; box-shadow: 0 8px 32px #243b2914; display: flex; flex-direction: column; font: .77rem/1.4 system-ui,sans-serif; overflow: hidden; }
.agda-reader-header { display: flex; justify-content: space-between; align-items: center; gap: .5rem; padding: .7rem 1rem .45rem; }
.agda-reader-header .eyebrow { font-size: .6rem; margin: 0; }
.agda-reader h2 { font: 600 .95rem/1.3 system-ui,sans-serif; margin: .15rem 0 0; }
.reader-close { border: 0; background: transparent; font: 1.5rem/1 system-ui,sans-serif; padding: .4rem; cursor: pointer; color: #405746; }
.reader-toolbar { display: flex; flex-wrap: wrap; gap: .4rem .7rem; align-items: center; padding: .35rem 1rem .5rem; border-bottom: 1px solid #e2e7df; font-size: .67rem; }
.module-browser { position: relative; flex: none; margin: .35rem 1rem; min-width: 0; }
.module-picker { cursor: pointer; padding: .35rem .5rem; border: 1px solid #d5ddd4; border-radius: .2rem; overflow-wrap: anywhere; }
.module-menu { position: absolute; z-index: 2; top: 100%; left: 0; right: 0; max-height: min(50dvh, 26rem); overflow-y: auto; overscroll-behavior: contain; background: #fffefa; border: 1px solid #d5ddd4; border-radius: .25rem; box-shadow: 0 6px 18px #243b2926; padding: .5rem; }
.module-menu .module-group > summary { padding: .45rem; }
.module-menu .module-group-content { padding: 0 .35rem .3rem; }
.module-choice { display: block; width: 100%; text-align: left; border: 0; border-radius: .2rem; background: transparent; padding: .4rem .5rem; cursor: pointer; color: inherit; font: inherit; overflow-wrap: anywhere; }
.module-choice:hover { background: #edf5f2; }
.module-choice[aria-pressed="true"] { background: #e0eee5; color: #145b47; font-weight: 600; }
.module-related { display: inline-block; margin-left: .6rem; font-size: .6rem; color: #53695b; font-weight: normal; }
.standalone-module-nav { display: flex; flex-wrap: wrap; align-items: center; gap: .6rem 1rem; margin: 1rem 0 .5rem; font: .85rem/1.5 system-ui, sans-serif; }
.standalone-module-browser { margin: 0; flex: 1 1 18rem; max-width: 42rem; }
.standalone-module-browser .module-menu { max-height: min(60dvh, 30rem); }
.standalone-module-browser a.module-choice { box-sizing: border-box; text-decoration: none; }
.module-choice[aria-current="page"] { background: #e0eee5; color: #145b47; font-weight: 600; }
.module-peers { font: .8rem/1.5 system-ui, sans-serif; margin: .5rem 0 1.2rem; border-bottom: 1px solid var(--rule); padding-bottom: .6rem; }
.module-peers > summary { cursor: pointer; font-weight: 600; }
.module-peers > ul { max-height: 10rem; overflow-y: auto; overscroll-behavior: contain; padding: .4rem 1.5rem; columns: 2 16rem; column-gap: 1.5rem; }
.module-peers li { break-inside: avoid; overflow-wrap: anywhere; margin: .2rem 0; }
.reader-role { color: #53695b; }
.reader-copy { font: inherit; border: 1px solid #d5ddd4; border-radius: .2rem; padding: .25rem .4rem; background: transparent; cursor: pointer; margin-left: auto; }
.reader-location { padding: .45rem 1rem; color: #68776b; font-size: .63rem; overflow-wrap: anywhere; }
pre.reader-code { position: relative; flex: 1; min-height: 0; width: 100%; max-width: none; margin: 0; padding: .8rem 0 2rem; border: 0; border-radius: 0; background: transparent; font: .73rem/1.65 "Cascadia Code","DejaVu Sans Mono",Consolas,monospace; overscroll-behavior: contain; }
.code-line { display: block; width: max-content; min-width: 100%; border-left: 2px solid transparent; padding-right: 1rem; }
.line-number { display: inline-block; width: 3.4rem; padding-right: .85rem; text-align: right; color: #78877a; user-select: none; opacity: 1; }
.line-text { opacity: 1; }
.code-line.is-relevant { background: #edf4e9; border-left-color: #42724d; }


.reader-code a:focus-visible { opacity: 1; outline-offset: 1px; }
.code-line:focus-within .line-text { opacity: 1; }
.reader-bottom { width: 100%; max-width: none; margin: 0; padding: .55rem 1rem; border-top: 1px solid #e2e7df; font-size: .65rem; display: flex; align-items: start; justify-content: space-between; gap: 1rem; }
.reader-bottom input { vertical-align: middle; }
.reader-bottom details { max-width: 65%; }
@media (min-width: 1001px) {
  body.has-passages { --rail-width: clamp(380px,37vw,620px); --book-width: min(690px,calc(100vw - var(--rail-width) - 64px)); }
  .has-passages .reader-grid { grid-template-columns: 180px var(--book-width); max-width: max-content; gap: 1.5rem; }
  .has-passages .notes-page { width: var(--book-width); }
  .agda-reader-open .reader-grid { grid-template-columns: var(--book-width); margin-left: max(0px,calc((100vw - var(--rail-width) - var(--book-width) - 64px)/2)); margin-right: 0; }
  .agda-reader-open .reader-nav { display: none; }
  .agda-reader-open .site-header, .agda-reader-open > footer { margin-left: 1.5rem; max-width: var(--book-width); }
}
/* Wide screens have room for navigation, prose and code together. */
@media screen and (min-width: 1280px) {
  body.has-passages.agda-reader-open {
    --rail-width: clamp(380px,32vw,620px);
    --book-width: min(690px,calc(100vw - var(--rail-width) - 268px));
  }
  .agda-reader-open .reader-grid {
    grid-template-columns: 180px var(--book-width);
    margin-left: max(0px,calc((100vw - var(--rail-width) - var(--book-width) - 268px)/2));
  }
  .agda-reader-open .reader-nav {
    display: block;
  }
  .agda-reader-open .site-header, .agda-reader-open > footer { max-width: calc(var(--book-width) + 204px); }
}
@media (max-width: 1000px) {
  .agda-reader { top: auto; bottom: .5rem; right: .5rem; left: .5rem; width: auto; height: 44dvh; }
  .agda-reader-open { padding-bottom: 46dvh; }
  .agda-reader-header { padding: .45rem .7rem .2rem; }
  .reader-toolbar { padding: .25rem .7rem; }
  .reader-location { padding: .2rem .7rem; }
  .reader-bottom { padding: .35rem .7rem; }
  pre.reader-code { font-size: .68rem; }
}
@media print { .agda-reader { display: none !important; } .has-passages .reader-grid { display: block; } .has-passages .notes-page { width: auto; } }
@media (max-width: 1000px) { .module-menu { max-height: max(5rem, calc(44dvh - 9rem)); } }

.hide-agda-links .agda-trigger { color: inherit; text-decoration: none; background: transparent; cursor: text; pointer-events: none; }
.hide-agda-links .agda-point { display: none; }

.supplementary-page .supplementary-statement { background: #f0f5fa; border-color: #668ca8; }
.supplementary-page [class*="ecti-"] { font-style: italic; }
.supplementary-page [class*="ecbx-"] { font-weight: 700; }