From 223142e932ec5fa64708b79606c5a6bef78024d8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 9 Apr 2025 14:35:28 -0300 Subject: [PATCH 1/7] web: infra to support popups for headers --- CONTRIBUTING.md | 27 +++++++++ support/shake/app/Definitions.hs | 2 +- support/shake/app/Shake/Highlights.hs | 6 +- support/shake/app/Shake/Markdown.hs | 70 +++++++++++++++++++---- support/web/css/components/highlight.scss | 49 ++++++++++++++++ support/web/css/components/popup.scss | 6 +- support/web/css/default.scss | 10 ++-- support/web/css/mixins.scss | 21 ------- support/web/css/theme.scss | 26 ++++++--- support/web/css/vars.scss | 10 +++- support/web/highlights/note.svg | 2 +- support/web/highlights/summary.svg | 17 ++++++ support/web/highlights/terminology.svg | 4 +- support/web/highlights/warning.svg | 9 ++- support/web/js/lib/hover.ts | 5 +- 15 files changed, 203 insertions(+), 61 deletions(-) create mode 100644 support/web/css/components/highlight.scss create mode 100644 support/web/highlights/summary.svg diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 5223a4979..6e664b7b2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -61,6 +61,7 @@ Link targets, called definitions, can be introduced in two ways: ``` ::: {.definition #anchor-1 alias="anchor-2"} [the definition] + ::: ``` Wikilink targets are case insensitive, and get "mangled" for whitespace: @@ -69,6 +70,32 @@ bound]]`, or `[[lub|least upper bound]]` if different textual content is required, or `[[lub|least-upper-bound]]`. White space **should** be used instead of dashes at use sites. +### Definition popups + +Definition links can have associated "popup" information which is +displayed when the reader hovers over that link. Popup information is +collected according to the following rules: + +* If the definition is associated with a header, **the content of all + top-level `div.popup`{.css} before the next header** will be + concatenated to make up the popup. + +* If the definition is associated with a `div`{.html} *and* that div + directly contains `div.popup`{.css}s, **their contents and those of + other blocks directly under the definition** will be concatenated to + make up the popup. + + This means that **non-paragraph, non-`popup`** content under a + definition will always be rendered on both the page and in popups. + + Otherwise, the content of the popup is just the literal content of the + div. + +Note that any paragraphs contained within divs with +`class="popup"`{.html} will be removed from the page entirely; other +elements (e.g. code) will be preserved. Divs that have other classes +will be preserved. + ## Linking identifiers An Agda identifier that _has been referred to_ in the current module can diff --git a/support/shake/app/Definitions.hs b/support/shake/app/Definitions.hs index 27f3bc1e7..e691801c4 100644 --- a/support/shake/app/Definitions.hs +++ b/support/shake/app/Definitions.hs @@ -90,7 +90,7 @@ definitionBlock inp fp = go where addMany id = foldMap (add id) . Text.words - go (Div (id, [only], keys) _blocks) | "definition" == only, not (Text.null id) = + go (Div (id, cls, keys) _blocks) | "definition" `elem` cls, not (Text.null id) = let aliases = foldMap (addMany id) (lookup "alias" keys) in add id id <> aliases diff --git a/support/shake/app/Shake/Highlights.hs b/support/shake/app/Shake/Highlights.hs index 9666740a7..71ab86302 100644 --- a/support/shake/app/Shake/Highlights.hs +++ b/support/shake/app/Shake/Highlights.hs @@ -48,8 +48,10 @@ renderHighlights stream = do iconSpan icn = do (icon, name') <- readIcon icn let name = TagText name' - pure $ TagBranch "span" [("class", "highlight-icon")] - (icon ++ [ TagBranch "span" [] [TagLeaf name] ]) + pure $ TagBranch "span" [("class", "highlight-header")] + [ TagBranch "span" [("class", "highlight-icon")] icon + , TagBranch "span" [("class", "highlight-text")] [TagLeaf name] + ] go :: TagTree Text -> Action (TagTree Text) go (TagBranch "div" attr children) diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs index dccc1e5ec..8e7419901 100644 --- a/support/shake/app/Shake/Markdown.hs +++ b/support/shake/app/Shake/Markdown.hs @@ -253,9 +253,10 @@ buildMarkdown modname input output = do baseUrl <- getBaseUrl filtered <- parallel $ map (runWriterT . walkM (patchBlock baseUrl modname)) blocks - let (bs, mss) = unzip filtered - MarkdownState references defs = fold mss - markdown = Pandoc meta bs + let + (bs, fold -> MarkdownState references defs) = unzip filtered + defs' = headerPopups bs + markdown = walk blankPopup $ Pandoc meta bs digest <- do cssDigest <- getFileDigest "_build/html/css/default.css" @@ -281,7 +282,7 @@ buildMarkdown modname input output = do Text.writeFile output $ renderHTML5 tags encodeFile ("_build/search" modname <.> "json") search - for_ (Map.toList defs) \(key, bs) -> traced "writing fragment" do + for_ (Map.toList defs <> Map.toList defs') \(key, bs) -> traced "writing fragment" do text <- either (fail . show) pure =<< runIO (renderMarkdown authors references modname baseUrl digest (Pandoc mempty bs)) @@ -344,9 +345,10 @@ patchInline _ h = pure h data MarkdownState = MarkdownState { mdReferences :: [Val Text] -- ^ List of references extracted from Pandoc's "reference" div. - , mdDefinitions :: Map.Map Mangled [Block] + , mdFragments :: Map.Map Mangled [Block] -- ^ List of definition blocks } + deriving (Show) instance Semigroup MarkdownState where MarkdownState a b <> MarkdownState a' b' = MarkdownState (a <> a') (b <> b') @@ -366,10 +368,11 @@ patchBlock -> Block -> f Block -- Make all headers links, and add an anchor emoji. -patchBlock _ _ (Header i a@(ident, _, _) inl) = pure $ Header i a - $ htmlInl (Text.concat [""]) - : inl - ++ [htmlInl "🔗"] +patchBlock _ _ (Header i a@(ident, _, kv) inl) = do + pure $ Header i a $ + htmlInl (Text.concat [""]) + : inl + ++ [htmlInl "🔗"] -- Replace quiver code blocks with a link to an SVG file, and depend on the SVG file. patchBlock _ mod (CodeBlock (id, classes, attrs) contents) | "quiver" `elem` classes = do @@ -425,14 +428,41 @@ patchBlock _ _ (Div ("refs", _, _) body) = do _ -> fail ("Unknown reference node " ++ show ref) pure $ Plain [] -- TODO: pandoc-types 1.23 removed Null -patchBlock _ _ b@(Div (id, [only], kv) bs) | "definition" == only, not (Text.null id) = do +patchBlock _ _ b@(Div (id, cls, kv) bs) | "definition" `elem` cls, not (Text.null id) = do let isfn (Note _) = True - isfn _ = False - b <$ tell (MarkdownState mempty (Map.singleton (mangleLink id) (walk (filter (not . isfn)) bs))) + isfn _ = False + + sel (Div (_, cls, _) bs) | "popup" `elem` cls = Unfurl True bs + sel x@Para{} = Unfurl False [] + sel x = Unfurl False [x] + + Unfurl hasU blks = foldMap sel bs + frag = walk (filter (not . isfn)) if hasU then blks else bs + + Div (id, cls, kv) bs <$ + tell mempty { mdFragments = Map.singleton (mangleLink id) frag } patchBlock _ _ h = pure h +-- | Remove any paragraphs that occur under a div with class @popup@. +blankPopup :: [Block] -> [Block] +blankPopup = concatMap go where + ispara (Para _) = True + ispara _ = False + + go (Div (_, [cls], _) bs) | "popup" == cls = filter (not . ispara) bs + go b = pure b + + +data Unfurl = Unfurl { hasUnfurl :: Bool, popupBlocks :: [Block] } + +instance Semigroup Unfurl where + Unfurl h b <> Unfurl h' b' = Unfurl (h || h') (b <> b') + +instance Monoid Unfurl where + mempty = Unfurl False [] + -- | Render our Pandoc document using the given template variables. renderMarkdown :: PandocMonad m @@ -574,6 +604,22 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) = write = writePlain def{ writerExtensions = enableExtension Ext_raw_html (writerExtensions def) } renderPlain inlines = either (error . show) id . runPure . write $ Pandoc mempty [Plain inlines] +-- | Collect fragments associated with popups. +headerPopups :: [Block] -> Map.Map Mangled [Block] +headerPopups = go Nothing where + go h (Header _ (id, _, kv) _:bs) + | isJust (lookup "defines" kv) = go (Just id) bs + | otherwise = go h bs + + go hdr (Div (_, cls, []) bs:bss) + | Just hdr <- hdr, "popup" `elem` cls + = Map.insertWith (<>) (mangleLink hdr) bs $ go (Just hdr) bss + + | otherwise = go hdr bss + + go hdr (b:bs) = go hdr bs + go hdr [] = mempty + htmlInl :: Text -> Inline htmlInl = RawInline "html" diff --git a/support/web/css/components/highlight.scss b/support/web/css/components/highlight.scss new file mode 100644 index 000000000..7fc5289a5 --- /dev/null +++ b/support/web/css/components/highlight.scss @@ -0,0 +1,49 @@ +@use 'sass:math'; + +@import "../vars.scss"; + +@mixin highlight($name) { + div.#{$name}, span.#{$name}, details.#{$name} { + .highlight-header { + fill: theme(--#{$name}-icon); + color: theme(--#{$name}-text); + } + } + + div.#{$name}, details.#{$name} { + @include material(theme(--#{$name}-bg)); + > :nth-child(2) { + margin-block-start: 0.25em; + } + } +} + + +span.highlight-header { + display: flex; + gap: 0.75ch; + align-items: baseline; + + > span.highlight-icon { + display: block; + min-height: 100%; + + svg { + position: relative; + top: #{math.div($highlight-icon-scale - 1, 2)}cap; + + height: #{$highlight-icon-scale}cap; + width: #{$highlight-icon-scale}cap; + } + } + + > span.highlight-text { + font-weight: bold; + } +} + +@include highlight(warning); +@include highlight(note); +@include highlight(terminology); +@include highlight(source); +@include highlight(summary); diff --git a/support/web/css/components/popup.scss b/support/web/css/components/popup.scss index ea29e1b2d..d3eb34705 100644 --- a/support/web/css/components/popup.scss +++ b/support/web/css/components/popup.scss @@ -26,9 +26,9 @@ div.hover-popup, div.hover-popup.sourceCode { } .text-popup { - min-width: 22em; - max-width: 26em; - width: min-content; + min-width: #{$text-popup-width}; + max-width: #{$text-popup-width * $text-popup-grow}; + width: fit-content; margin-left: 1.25em; } diff --git a/support/web/css/default.scss b/support/web/css/default.scss index 3a0089226..9398dc129 100644 --- a/support/web/css/default.scss +++ b/support/web/css/default.scss @@ -10,6 +10,7 @@ @import "components/modal.scss"; @import "components/popup.scss"; @import "components/toc.scss"; +@import "components/highlight.scss"; @import "code.scss"; @@ -65,11 +66,6 @@ main { box-sizing: border-box; } -@include highlight(warning, theme(--warning-bg), theme(--warning-icon)); -@include highlight(note, theme(--note-bg), theme(--note-icon)); -@include highlight(terminology, theme(--terminology-bg), theme(--terminology-icon)); -@include highlight(source, theme(--source-bg), theme(--source-icon)); - figure { overflow-x: auto; overflow-y: clip; @@ -103,6 +99,10 @@ span.katex { span.mord.text > span.mord.textrm { font-family: var(--serif), var(--sans-serif); } + + strong & span.mord.text > span.mord.textrm { + font-weight: bold; + } } span.abbrev { diff --git a/support/web/css/mixins.scss b/support/web/css/mixins.scss index 4e80017d6..89abce732 100644 --- a/support/web/css/mixins.scss +++ b/support/web/css/mixins.scss @@ -40,27 +40,6 @@ margin-block: 1em; } -@mixin highlight($name, $bg, $icon) { - div.#{$name}, span.#{$name}, details.#{$name} { - .highlight-icon { - fill: $icon; - color: $icon; - - display: flex; - gap: 0.5em; - align-items: center; - margin-bottom: 0.3em; - } - } - - div.#{$name}, details.#{$name} { - @include material($bg); - > :nth-child(2) { - margin-block-start: 0.25em; - } - } -} - @mixin centered-contents { display: flex; flex-direction: column; diff --git a/support/web/css/theme.scss b/support/web/css/theme.scss index 69121f5a0..f23f9400d 100644 --- a/support/web/css/theme.scss +++ b/support/web/css/theme.scss @@ -23,23 +23,33 @@ $theme: ( ruler: (light: #94A3B8, dark: #94A3B8), warning: ( - bg: (light: $yellow-400, dark: $yellow-500), - icon: (light: $yellow-700, dark: $yellow-400), + bg: (light: $rose-600, dark: $rose-700), + icon: (light: $rose-700, dark: $rose-600), + text: (light: $rose-700, dark: $rose-600), ), note: ( - bg: (light: $violet-500, dark: $violet-500), - icon: (light: $violet-600, dark: $violet-400), + bg: (light: $violet-400, dark: $violet-500), + icon: (light: $violet-500, dark: $violet-400), + text: (light: $violet-500, dark: $violet-400), + ), + + summary: ( + bg: (light: $violet-400, dark: $violet-500), + icon: (light: $violet-500, dark: $violet-400), + text: (light: $violet-500, dark: $violet-400), ), terminology: ( - bg: (light: $cyan-600, dark: $cyan-600), - icon: (light: $cyan-900, dark: $cyan-700), + bg: (light: $cyan-600, dark: $cyan-700), + icon: (light: $cyan-700, dark: $cyan-600), + text: (light: $cyan-700, dark: $cyan-600), ), source: ( - bg: (light: $cyan-600, dark: $cyan-600), - icon: (light: $cyan-900, dark: $cyan-700), + bg: (light: $cyan-600, dark: $cyan-700), + icon: (light: $cyan-700, dark: $cyan-600), + text: (light: $cyan-700, dark: $cyan-600), ), commit: ( diff --git a/support/web/css/vars.scss b/support/web/css/vars.scss index a5d678e1b..a30a72498 100644 --- a/support/web/css/vars.scss +++ b/support/web/css/vars.scss @@ -6,8 +6,16 @@ $desktop-layout-width: 95rem; // Distance and width between a "left-bordered block" (think
) // and the actual border. -$left-border-distance: 1em; +$left-border-distance: 0.75em; $left-border-width: 5px; // Size of rulers (e.g.
, border of the navbar list) $ruler-size: 2px; + +// How much larger icons should be relative to the size of a capital +// letter. +$highlight-icon-scale: 1.2; + +// Minimum width of a text popup and how much it's allowed to grow. +$text-popup-width: 25em; +$text-popup-grow: 1.25; diff --git a/support/web/highlights/note.svg b/support/web/highlights/note.svg index 5a34b86d3..2275cf48a 100644 --- a/support/web/highlights/note.svg +++ b/support/web/highlights/note.svg @@ -1,3 +1,3 @@ - + diff --git a/support/web/highlights/summary.svg b/support/web/highlights/summary.svg new file mode 100644 index 000000000..6f85c0bfe --- /dev/null +++ b/support/web/highlights/summary.svg @@ -0,0 +1,17 @@ + + + + + + + diff --git a/support/web/highlights/terminology.svg b/support/web/highlights/terminology.svg index 21696332a..8aae2c137 100644 --- a/support/web/highlights/terminology.svg +++ b/support/web/highlights/terminology.svg @@ -1,3 +1,3 @@ - - + + diff --git a/support/web/highlights/warning.svg b/support/web/highlights/warning.svg index c2d507557..1e8f07a0a 100644 --- a/support/web/highlights/warning.svg +++ b/support/web/highlights/warning.svg @@ -1,4 +1,7 @@ - - - \ + + + + diff --git a/support/web/js/lib/hover.ts b/support/web/js/lib/hover.ts index 4e2a6f858..cba63350b 100644 --- a/support/web/js/lib/hover.ts +++ b/support/web/js/lib/hover.ts @@ -75,8 +75,9 @@ export class Hover { el.classList.remove('popup-hidden'); - const selfRect = this.anchor.getBoundingClientRect(); + const selfRect = this.anchor.getBoundingClientRect(); const hoverRect = el.getBoundingClientRect(); + const textRect = document.querySelector("div#post-toc-container > article")!.getBoundingClientRect(); if (selfRect.bottom + hoverRect.height + 48 > window.innerHeight) { // Tooltip placed above anchor @@ -88,7 +89,7 @@ export class Hover { this.fadeDirection = 'up'; } - if (selfRect.left + hoverRect.width > window.innerWidth) { + if (selfRect.left + hoverRect.width > textRect.right) { el.style.left = `calc(${selfRect.right - hoverRect.width}px)`; } else { el.style.left = `${selfRect.left}px`; From e50d0b7c84012cf69395308350ea5419d2f698a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 9 Apr 2025 14:37:21 -0300 Subject: [PATCH 2/7] =?UTF-8?q?rename=20\ty=20=E2=86=92=20\type?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/1Lab/Counterexamples/Isovalence.lagda.md | 2 +- src/1Lab/Equiv.lagda.md | 8 +-- src/1Lab/Equiv/Fibrewise.lagda.md | 2 +- src/1Lab/Path.lagda.md | 4 +- src/1Lab/Path/IdentitySystem.lagda.md | 13 +++- src/1Lab/Path/IdentitySystem/Strict.lagda.md | 2 +- src/1Lab/Univalence.lagda.md | 6 +- src/1Lab/intro.lagda.md | 62 +++++++++---------- src/Algebra/Group/Concrete.lagda.md | 2 +- src/Cat/Diagram/Colimit/Base.lagda.md | 4 +- src/Cat/Diagram/Coproduct/Indexed.lagda.md | 2 +- src/Cat/Diagram/Limit/Base.lagda.md | 2 +- src/Cat/Diagram/Product/Indexed.lagda.md | 2 +- .../Instances/DisplayedFamilies.lagda.md | 2 +- .../Instances/Subobjects/Reasoning.lagda.md | 1 - src/Cat/Functor/Adjoint.lagda.md | 11 +++- src/Cat/Instances/OFE.lagda.md | 2 +- src/Cat/Instances/OFE/Product.lagda.md | 4 +- src/Cat/Univalent.lagda.md | 8 ++- src/Data/Fin/Finite.lagda.md | 2 +- src/Data/Int/Universal.lagda.md | 2 +- src/Data/Set/Coequaliser.lagda.md | 4 +- src/Data/Set/Material.lagda.md | 4 +- src/Data/Set/Projective.lagda.md | 4 +- src/Data/Wellfounded/W.lagda.md | 2 +- src/Homotopy/Space/Delooping.lagda.md | 2 +- src/Homotopy/Truncation.lagda.md | 6 +- src/Order/Univalent.lagda.md | 2 +- src/Talks/Topos2024.lagda.md | 4 +- src/preamble.tex | 2 +- 30 files changed, 96 insertions(+), 77 deletions(-) diff --git a/src/1Lab/Counterexamples/Isovalence.lagda.md b/src/1Lab/Counterexamples/Isovalence.lagda.md index dc7463926..d15f1a2c9 100644 --- a/src/1Lab/Counterexamples/Isovalence.lagda.md +++ b/src/1Lab/Counterexamples/Isovalence.lagda.md @@ -42,7 +42,7 @@ fact will be crucial in the proof below. We say that **isovalence holds** if the isomorphisms, equipped with the natural choice of identity, form an identity system on every universe -$\ty_j$. +$\type_j$. ```agda Isovalence : Typeω diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md index 22946de39..faaf0c27f 100644 --- a/src/1Lab/Equiv.lagda.md +++ b/src/1Lab/Equiv.lagda.md @@ -910,17 +910,17 @@ postcomposition with $p\inv$, so it too is an equivalence. ### The Lift type Because Agda's universes are not *cumulative*, we can not freely move a -type $A : \ty_0$ to conclude that $A : \ty_1$, or to higher universes. +type $A : \type_0$ to conclude that $A : \type_1$, or to higher universes. To work around this, we have a `Lift`{.Agda} type, which, given a small -type $A : \ty_i$ and some universe $j \gt i$, gives us a _name_ for $A$ -in $\ty_j$. To know that this operation is coherent, we can prove that +type $A : \type_i$ and some universe $j \gt i$, gives us a _name_ for $A$ +in $\type_j$. To know that this operation is coherent, we can prove that the lifting map $$ A \to \operatorname{Lift}_j A $$ -is an equivalence: the name of $A$ in $\ty_j$ really is equivalent to +is an equivalence: the name of $A$ in $\type_j$ really is equivalent to the type we started with. Because `Lift`{.Agda} is a very well-behaved record type, the proof that this is an equivalence looks very similar to the proof that the identity function is an equivalence: diff --git a/src/1Lab/Equiv/Fibrewise.lagda.md b/src/1Lab/Equiv/Fibrewise.lagda.md index 27a2e09c1..a1a1fcf9e 100644 --- a/src/1Lab/Equiv/Fibrewise.lagda.md +++ b/src/1Lab/Equiv/Fibrewise.lagda.md @@ -98,7 +98,7 @@ equiv→total always-eqv .is-eqv y = ## Equivalences over {defines="equivalence-over"} We can generalise the notion of fibrewise equivalence to families -$P : A \to \ty$, $Q : B \to \ty$ over *different* base types, +$P : A \to \type$, $Q : B \to \type$ over *different* base types, provided we have an equivalence $e : A \simeq B$. In that case, we say that $P$ and $Q$ are **equivalent over** $e$ if $P(a) \simeq Q(b)$ whenever $a : A$ and $b : B$ are identified [[over|path over]] $e$. diff --git a/src/1Lab/Path.lagda.md b/src/1Lab/Path.lagda.md index 12c0ec970..14b482197 100644 --- a/src/1Lab/Path.lagda.md +++ b/src/1Lab/Path.lagda.md @@ -175,7 +175,7 @@ turn out to be very useful: they're **dependent paths**. We'll have them with another emergent notion of dependent path, but it's important to mention the primitive notion now. -If we have a *line* of types $A : \bI \to \ty$, and inhabitants $a : +If we have a *line* of types $A : \bI \to \type$, and inhabitants $a : A(\iZ)$ and $b : A(\iO)$, we can form the **dependent** path space between them: the type $\PathP{A}{a}{b}$, which in the code is written `PathP A a b`. Here, inferring the line $A$ is basically always @@ -246,7 +246,7 @@ below. \draw plot[smooth cycle] coordinates {(0, -1.5) (-3, -0.75) (-2.5, 0.25) (3, 1.25) (3.5, 0.25)}; -\node at (2.75, -1) {$\ty$}; +\node at (2.75, -1) {$\type$}; \node (A) at (0.275, -0.375) {$A$}; diff --git a/src/1Lab/Path/IdentitySystem.lagda.md b/src/1Lab/Path/IdentitySystem.lagda.md index daf1f09a1..51ce12e13 100644 --- a/src/1Lab/Path/IdentitySystem.lagda.md +++ b/src/1Lab/Path/IdentitySystem.lagda.md @@ -19,7 +19,7 @@ open import Data.Dec.Base module 1Lab.Path.IdentitySystem where ``` -# Identity systems {defines=identity-system} +# Identity systems An **identity system** is a way of characterising the path spaces of a particular type, without necessarily having to construct a full @@ -54,6 +54,17 @@ record open is-identity-system public ``` +:::{.definition .summary #identity-system} +A type family $R : A \to A \to \type$, equipped with reflexivity +witness $r : \forall\ a,\ R\ a\ a$, is an **identity system** when we are +given a map +$$ +\operatorname{to-path} : \forall\ a\ b,\ R\ a\ b \to a \is b +$$ +and for every $p : R\ a\ b$ an identification, over +$\operatorname{to-path}(p)$, between $r(a)$ and $p$. +::: + As mentioned before, the data of an identity system gives us exactly what is required to prove J for the relation $R$. This is essentially the decomposition of J into _contractibility of singletons_, but with diff --git a/src/1Lab/Path/IdentitySystem/Strict.lagda.md b/src/1Lab/Path/IdentitySystem/Strict.lagda.md index f2ae08107..f9b4f796b 100644 --- a/src/1Lab/Path/IdentitySystem/Strict.lagda.md +++ b/src/1Lab/Path/IdentitySystem/Strict.lagda.md @@ -45,7 +45,7 @@ set-identity-is-prop {R = R} {a = a} {b = b} ids set = ``` This immediately gives us the K eliminator for an identity system over a -set: Given a type family $P : R(a, a) \to \ty$ and a witness $w : +set: Given a type family $P : R(a, a) \to \type$ and a witness $w : P(r(a))$, since $R(-,-)$ is a proposition, we can transport $w$ to $P(s)$ for an arbitrary $s : R(a,a)$. diff --git a/src/1Lab/Univalence.lagda.md b/src/1Lab/Univalence.lagda.md index 698e7ce94..f2ab5f5d3 100644 --- a/src/1Lab/Univalence.lagda.md +++ b/src/1Lab/Univalence.lagda.md @@ -654,8 +654,8 @@ Total-equiv p = Iso→Equiv isom where ``` Putting these together, we get the promised theorem: The space of maps -$B \to \ty$ is equivalent to the space of fibrations with base -space $B$ and variable total space $E$, $\Sigma_{(E : \ty)} +$B \to \type$ is equivalent to the space of fibrations with base +space $B$ and variable total space $E$, $\Sigma_{(E : \type)} (E \to B)$. If we allow $E$ and $B$ to live in different universes, then the maps are classified by the biggest universe in which they both fit, namely `Type (ℓ ⊔ ℓ')`. Note that the proof of `Fibration-equiv`{.Agda} @@ -702,7 +702,7 @@ very unwieldy description --- both in words or in Agda syntax --- we abbreviate it by $\ell /_{[P]} B$. The notation is meant to evoke the idea of a slice category: The objects of $C/c$ are objects of the category $C$ equipped with choices of maps into $c$. Similarly, the -objects of $\ell/_{[P]}B$ are objects of the universe $\ty\ +objects of $\ell/_{[P]}B$ are objects of the universe $\type\ \ell$, with a choice of map $f$ into $B$, such that $P$ holds for all the fibres of $f$. ::: diff --git a/src/1Lab/intro.lagda.md b/src/1Lab/intro.lagda.md index 9810124e2..1500e97ae 100644 --- a/src/1Lab/intro.lagda.md +++ b/src/1Lab/intro.lagda.md @@ -598,8 +598,8 @@ classifier is exactly the category of sets.
Thus we might hope to find, in addition to a subobject classifier, we -could have a general **object classifier**, an object $\ty$ such that -maps $B \to \ty$ correspond to _arbitrary_ maps $A \to B$. Let's specify +could have a general **object classifier**, an object $\type$ such that +maps $B \to \type$ correspond to _arbitrary_ maps $A \to B$. Let's specify this notion better using the language of higher category theory: A **subobject classifier** is a [[representing object|representable @@ -635,14 +635,14 @@ $\hom_{\cE}(-, U)$! The issue does eventually resolve itself, if we're very persistent: if we have an $\infty$-category $\cE$, where $\hom(-,-)$ can be a genuine $\infty$-groupoid, then it's actually perfectly possible for there to be -an object $\ty$ with an isomorphism $\cE/- \cong \hom(-, \ty)$ --- well, +an object $\type$ with an isomorphism $\cE/- \cong \hom(-, \type)$ --- well, at least as long as we restrict ourselves to $\rm{Core}(\cE/-)$. We've finally found a setting where object classifiers can exist: $\io$-categories! Again, the importance of object classifiers is that they let us talk -about arbitrary objects as if they were points of an object $\ty$. +about arbitrary objects as if they were points of an object $\type$. Specifically, any object $B$ has a _name_, a map $\ulcorner B \urcorner -: * \to \ty$, which represents the unique map $B \to *$. To make this +: * \to \type$, which represents the unique map $B \to *$. To make this connection clearer, let's pass back to a syntactic presentation of type theory, to see what universes look like "from the inside". @@ -652,7 +652,7 @@ Inside type theory, object classifiers present themselves as types which contain types, which we call **universes**. Every type is contained in some universe, but it is not the case that there is a universe containing all types; In fact, if we did have some magical universe -$\ty_\infty : \ty_\infty$, we could reproduce Russell's paradox, as is +$\type_\infty : \type_\infty$, we could reproduce Russell's paradox, as is done [here]. [here]: 1Lab.Counterexamples.Russell.html @@ -663,7 +663,7 @@ the collection of all "large" objects being "huge", etc. On the semantic side, a $\io$-topos has a sequence of object classifiers for maps with $\kappa$-compact fibres, where $\kappa$ is a regular cardinal; Syntactically, this is reflected much more simply as having a _tower_ of -universes with $\ty_i : \ty_{1+i}$. So, in Agda, we have: +universes with $\type_i : \type_{1+i}$. So, in Agda, we have: We will now show that `W'` satisfies the induction principle of $W_A B$. -To that end, suppose we have a predicate $P : W' \to \ty$, the +To that end, suppose we have a predicate $P : W' \to \type$, the *motive* for induction, and a function — the *method* $m$ — showing $P(\rm{sup}(a, f))$ given the data of the constructor $a : A$, $f : (b : B\, a) \to W'$, and the induction hypotheses $f' : (b : B\, a) \to diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md index 2ad68722d..733fc579a 100644 --- a/src/Homotopy/Space/Delooping.lagda.md +++ b/src/Homotopy/Space/Delooping.lagda.md @@ -150,7 +150,7 @@ together to establish `G ≡ (base ≡ base)`. We'll want to define the family `Code` by induction on `Deloop`. First, since we have to map into a [[groupoid]], we'll map into the type -$\set$, rather than $\ty$. This takes care of the truncation +$\set$, rather than $\type$. This takes care of the truncation constructor (which is hidden from the page since it is entirely formulaic): let's tackle the rest in order. We can also handle the `base`{.Agda} case, since `Code base = G` was already a part of our diff --git a/src/Homotopy/Truncation.lagda.md b/src/Homotopy/Truncation.lagda.md index 60deeb849..b82bc1140 100644 --- a/src/Homotopy/Truncation.lagda.md +++ b/src/Homotopy/Truncation.lagda.md @@ -222,11 +222,11 @@ $$ $$ so we will, for every $x : A$, define a type family $\mathrm{code}(x) : -\|A\|_{2+n} \to \ty$, where the fibre of $\mathrm{code}(x)$ over +\|A\|_{2+n} \to \type$, where the fibre of $\mathrm{code}(x)$ over $\rm{inc}(y)$ should be $\|x \equiv y\|_{1+n}$. However, the induction principle for $\|A\|_{2+n}$ only allows us to map into $(2+n)$-types, -while $\ty$ itself is not an $n$-type for any $n$. We salvage our -definition by instead mapping into $(1+n)\text{-}\ty$, which _is_ a +while $\type$ itself is not an $n$-type for any $n$. We salvage our +definition by instead mapping into $(1+n)\text{-}\type$, which _is_ a $(2+n)$-type. ```agda diff --git a/src/Order/Univalent.lagda.md b/src/Order/Univalent.lagda.md index d6a84e9bf..3d09c6d2d 100644 --- a/src/Order/Univalent.lagda.md +++ b/src/Order/Univalent.lagda.md @@ -63,7 +63,7 @@ constructed. We do this by an explicit cubical construction. It will suffice to construct a term $$ -i : \bI, x : \rm{ob}(i), y : \rm{ob}(i) \vdash \rm{order}_i(x,y) : \ty +i : \bI, x : \rm{ob}(i), y : \rm{ob}(i) \vdash \rm{order}_i(x,y) : \type $$ which reduces to $x \le_P y$ when $i = i0$ (resp. $x \le_Q y$ when $i = diff --git a/src/Talks/Topos2024.lagda.md b/src/Talks/Topos2024.lagda.md index 6a502995e..802cdd379 100644 --- a/src/Talks/Topos2024.lagda.md +++ b/src/Talks/Topos2024.lagda.md @@ -397,7 +397,7 @@ embeddings, monotone maps, &c., &c. # Structure (and) identity -Same setup: when are types $A, B : \ty$ identical?
+Same setup: when are types $A, B : \type$ identical?
Ideal answer: when they are *indistinguishable*.
What distinguishes types? @@ -763,7 +763,7 @@ We can present a concrete, univalent category as a displayed category. These data amount to: -1. A type family of *structures* $F : \ty \to \ty$; +1. A type family of *structures* $F : \type \to \type$; 2. A proposition $\operatorname{Hom}[f](S, T)$, given $f : A \to B$, $S : F(A)$, $T : F(B)$. diff --git a/src/preamble.tex b/src/preamble.tex index 359bb472f..4afb29d3a 100644 --- a/src/preamble.tex +++ b/src/preamble.tex @@ -65,7 +65,7 @@ \newcommand{\knowncat}[1]{\newcommand{\csname #1\endcsname}{\thecat{#1}}} \newcommand{\knownbicat}[1]{\newcommand{\csname #1\endcsname}{\thebicat{#1}}} -\newcommand{\ty}{\rm{Type}} +\newcommand{\type}{\rm{Type}} \newcommand{\set}{\rm{Set}} \newcommand{\prop}{\rm{Prop}} \newcommand{\psh}{\rm{PSh}} From d0e658df9b18739e722c493e79ec4f7ef0c492dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 9 Apr 2025 19:02:41 -0300 Subject: [PATCH 3/7] fixup --- support/shake/app/Definitions.hs | 20 ++++++++++- support/shake/app/Shake/Digest.hs | 9 +++-- support/shake/app/Shake/Markdown.hs | 49 ++++++++++++++++----------- support/web/css/components/popup.scss | 8 +++++ support/web/css/default.scss | 2 +- 5 files changed, 65 insertions(+), 23 deletions(-) diff --git a/support/shake/app/Definitions.hs b/support/shake/app/Definitions.hs index e691801c4..4190ef4f1 100644 --- a/support/shake/app/Definitions.hs +++ b/support/shake/app/Definitions.hs @@ -17,16 +17,20 @@ import Agda.Utils.Impossible import Control.Monad.IO.Class import Control.DeepSeq import Control.Arrow (first) +import Control.Monad import qualified Data.Map.Strict as Map import qualified Data.Text.IO as Text import qualified Data.Text as Text +import qualified Data.Set as Set +import Data.Traversable import Data.Map.Strict (Map) import Data.Function import Data.Hashable import Data.Foldable import Data.Monoid ( Endo(..) ) import Data.Binary ( Binary ) +import Data.Maybe import Data.List (intersperse, sortOn, groupBy) import Data.Text (Text) import Data.Char @@ -43,6 +47,7 @@ import Text.Pandoc.Walk import Text.Pandoc import {-# SOURCE #-} Shake.Markdown (readLabMarkdown) +import Shake.Digest (shortDigest) newtype Mangled = Mangled { getMangled :: Text } deriving (Show, Eq, Ord, Generic) @@ -154,7 +159,9 @@ glossaryRules = do _ <- addOracle \(LinkTargetQ target) -> do glo <- getEntries <$> askOracle GlossaryQ case Map.lookup (mangleLink target) glo of - Just def -> pure (definitionAnchor def, definitionTarget def) + Just def -> + let trg = definitionTarget def + in pure (Text.pack (shortDigest trg), definitionTarget def) Nothing -> error $ "Unknown wiki-link target: " ++ Text.unpack target @@ -183,6 +190,17 @@ glossaryRules = do Text.putStr $ Text.pack (dropExtension mod) <> ":\n" <> Text.unlines (aliases <$> bykey defs) + phony "popup-todo" do + entries <- Map.elems . getEntries <$> askOracle GlossaryQ + + keep <- for entries \def -> do + let d = shortDigest (definitionTarget def) + x <- doesFileExist $ "_build/html/fragments" d <.> "html" + pure $ definitionTarget def <$ guard (not x) + + liftIO . Text.writeFile "todo" $ Text.unlines $ Set.toList $ + foldMap (foldMap Set.singleton) (keep :: [Maybe Text]) + pure () data WikiLink = WikiLink diff --git a/support/shake/app/Shake/Digest.hs b/support/shake/app/Shake/Digest.hs index 29b793550..e671bf3b6 100644 --- a/support/shake/app/Shake/Digest.hs +++ b/support/shake/app/Shake/Digest.hs @@ -2,9 +2,11 @@ -- | Compute a truncated hash of a file, useful for computing cache-busters -- (or other unique ids) for a file. -module Shake.Digest (digestRules, getFileDigest) where +module Shake.Digest (digestRules, getFileDigest, shortDigest) where import qualified Data.ByteString.Lazy as LazyBS +import qualified Data.Text.Encoding as Text +import qualified Data.Text as Text import Data.Digest.Pure.SHA import Data.Typeable @@ -21,9 +23,12 @@ digestRules :: Rules () digestRules = versioned 1 do _ <- addOracle \(FileDigest f) -> do need [f] - take 8 . showDigest . sha256 <$> liftIO (LazyBS.readFile f) + take 12 . showDigest . sha256 <$> liftIO (LazyBS.readFile f) pure () -- | Compute a short digest of a file. getFileDigest :: FilePath -> Action String getFileDigest = askOracle . FileDigest + +shortDigest :: Text.Text -> [Char] +shortDigest = take 12 . showDigest . sha1 . LazyBS.fromStrict . Text.encodeUtf8 diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs index 8e7419901..a5c65e6f4 100644 --- a/support/shake/app/Shake/Markdown.hs +++ b/support/shake/app/Shake/Markdown.hs @@ -282,11 +282,13 @@ buildMarkdown modname input output = do Text.writeFile output $ renderHTML5 tags encodeFile ("_build/search" modname <.> "json") search - for_ (Map.toList defs <> Map.toList defs') \(key, bs) -> traced "writing fragment" do - text <- either (fail . show) pure =<< - runIO (renderMarkdown authors references modname baseUrl digest (Pandoc mempty bs)) + for_ (Map.toList defs <> Map.toList defs') \(key, bs) -> do + (key, _) <- getWikiLinkUrl key + traced "writing fragment" do + text <- either (fail . show) pure =<< + runIO (renderMarkdown authors references modname baseUrl digest (Pandoc mempty bs)) - Text.writeFile ("_build/html/fragments" Text.unpack (getMangled key) <.> "html") text + Text.writeFile ("_build/html/fragments" Text.unpack key <.> "html") text -- | Find the original Agda file from a 1Lab module name. findModule :: MonadIO m => String -> m FilePath @@ -345,7 +347,7 @@ patchInline _ h = pure h data MarkdownState = MarkdownState { mdReferences :: [Val Text] -- ^ List of references extracted from Pandoc's "reference" div. - , mdFragments :: Map.Map Mangled [Block] + , mdFragments :: Map.Map Text [Block] -- ^ List of definition blocks } deriving (Show) @@ -377,7 +379,7 @@ patchBlock _ _ (Header i a@(ident, _, kv) inl) = do -- Replace quiver code blocks with a link to an SVG file, and depend on the SVG file. patchBlock _ mod (CodeBlock (id, classes, attrs) contents) | "quiver" `elem` classes = do let - digest = take 12 . showDigest . sha1 . LazyBS.fromStrict $ Text.encodeUtf8 contents + digest = shortDigest contents title = fromMaybe "commutative diagram" (lookup "title" attrs) lfn = mod digest <.> "light.svg" @@ -430,28 +432,37 @@ patchBlock _ _ (Div ("refs", _, _) body) = do patchBlock _ _ b@(Div (id, cls, kv) bs) | "definition" `elem` cls, not (Text.null id) = do let - isfn (Note _) = True - isfn _ = False - sel (Div (_, cls, _) bs) | "popup" `elem` cls = Unfurl True bs + sel (Div (_, cls, _) bs) + | "popup" `elem` cls || "popup-only" `elem` cls = Unfurl True bs sel x@Para{} = Unfurl False [] sel x = Unfurl False [x] Unfurl hasU blks = foldMap sel bs - frag = walk (filter (not . isfn)) if hasU then blks else bs + frag = walk (filter (not . isFootnote)) if hasU then blks else bs Div (id, cls, kv) bs <$ - tell mempty { mdFragments = Map.singleton (mangleLink id) frag } + tell mempty { mdFragments = Map.singleton id frag } patchBlock _ _ h = pure h +isFootnote :: Inline -> Bool +isFootnote (Note _) = True +isFootnote _ = False + -- | Remove any paragraphs that occur under a div with class @popup@. blankPopup :: [Block] -> [Block] blankPopup = concatMap go where - ispara (Para _) = True - ispara _ = False + ispara Para{} = True + ispara _ = False + + iscode CodeBlock{} = True + iscode _ = False - go (Div (_, [cls], _) bs) | "popup" == cls = filter (not . ispara) bs + go (Div (_, [cls], _) bs) + | "popup" == cls = filter (not . ispara) bs + | "popup-only" == cls, any iscode bs = error "code block can not appear under popup-only div." + | "popup-only" == cls = [] go b = pure b @@ -605,15 +616,15 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) = renderPlain inlines = either (error . show) id . runPure . write $ Pandoc mempty [Plain inlines] -- | Collect fragments associated with popups. -headerPopups :: [Block] -> Map.Map Mangled [Block] +headerPopups :: [Block] -> Map.Map Text [Block] headerPopups = go Nothing where go h (Header _ (id, _, kv) _:bs) - | isJust (lookup "defines" kv) = go (Just id) bs - | otherwise = go h bs + | Just k <- lookup "defines" kv, w:_ <- Text.words k = go (Just w) bs + | otherwise = go h bs go hdr (Div (_, cls, []) bs:bss) - | Just hdr <- hdr, "popup" `elem` cls - = Map.insertWith (<>) (mangleLink hdr) bs $ go (Just hdr) bss + | Just hdr <- hdr, "popup" `elem` cls || "popup-only" `elem` cls + = Map.insertWith (<>) hdr (walk (filter (not . isFootnote)) bs) $ go (Just hdr) bss | otherwise = go hdr bss diff --git a/support/web/css/components/popup.scss b/support/web/css/components/popup.scss index d3eb34705..8663a722d 100644 --- a/support/web/css/components/popup.scss +++ b/support/web/css/components/popup.scss @@ -31,6 +31,14 @@ div.hover-popup, div.hover-popup.sourceCode { width: fit-content; margin-left: 1.25em; + + > *, > div.diagram-container { + margin-block: 0.5em; + } + + div.diagram-container img.diagram { + height: calc(0.75 * var(--height)); + } } diff --git a/support/web/css/default.scss b/support/web/css/default.scss index 9398dc129..b99c51207 100644 --- a/support/web/css/default.scss +++ b/support/web/css/default.scss @@ -27,7 +27,7 @@ html, body, main, div#post-toc-container { max-width: 100vw; } -body, p { +body, p, li { font-family: var(--serif), var(--sans-serif); font-size: var(--font-size); } From e4f9994679ddb216a7573f51ba3a7e69ede54b4d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 9 Apr 2025 19:04:18 -0300 Subject: [PATCH 4/7] chore: first 190 definitions --- src/1Lab/Classical.lagda.md | 35 ++-- src/1Lab/Equiv.lagda.md | 9 ++ src/1Lab/Equiv/Biinv.lagda.md | 8 +- src/1Lab/Equiv/Fibrewise.lagda.md | 10 +- src/1Lab/Equiv/HalfAdjoint.lagda.md | 24 +-- src/1Lab/Function/Embedding.lagda.md | 7 + src/1Lab/Function/Surjection.lagda.md | 4 +- src/1Lab/HIT/Truncation.lagda.md | 12 +- src/1Lab/HLevel.lagda.md | 39 ++++- src/1Lab/Path.lagda.md | 18 ++- src/1Lab/Path/IdentitySystem.lagda.md | 4 +- src/1Lab/Resizing.lagda.md | 10 ++ src/1Lab/Type/Pointed.lagda.md | 5 +- src/1Lab/Univalence.lagda.md | 8 +- src/Algebra/Group.lagda.md | 15 +- src/Algebra/Group/Ab.lagda.md | 5 + src/Algebra/Group/Ab/Abelianisation.lagda.md | 18 ++- src/Algebra/Group/Ab/Tensor.lagda.md | 3 +- src/Algebra/Group/Action.lagda.md | 6 + src/Algebra/Group/Cayley.lagda.md | 14 +- src/Algebra/Group/Concrete.lagda.md | 151 ++++++++++-------- src/Algebra/Group/Concrete/Abelian.lagda.md | 7 +- src/Algebra/Group/Free.lagda.md | 19 ++- src/Algebra/Group/Homotopy.lagda.md | 20 ++- src/Algebra/Group/Homotopy/BAut.lagda.md | 14 +- src/Algebra/Group/Instances/Cyclic.lagda.md | 4 +- src/Algebra/Group/Instances/Integers.lagda.md | 9 +- .../Group/Instances/Symmetric.lagda.md | 8 +- src/Algebra/Group/Semidirect.lagda.md | 11 +- src/Algebra/Group/Subgroup.lagda.md | 14 +- src/Algebra/Monoid.lagda.md | 2 +- src/Algebra/Ring.lagda.md | 14 +- src/Algebra/Ring/Ideal.lagda.md | 42 ++--- src/Algebra/Ring/Module/Category.lagda.md | 10 +- src/Algebra/Ring/Quotient.lagda.md | 2 +- src/Cat/Abelian/Base.lagda.md | 33 ++-- src/Cat/Allegory/Base.lagda.md | 12 ++ src/Cat/Allegory/Instances/Mat.lagda.md | 3 +- src/Cat/Base.lagda.md | 11 +- src/Cat/CartesianClosed/Locally.lagda.md | 2 - src/Cat/Diagram/Biproduct.lagda.md | 33 ++-- src/Cat/Diagram/Coend.lagda.md | 29 ++-- src/Cat/Diagram/Coend/Sets.lagda.md | 4 +- src/Cat/Diagram/Colimit/Base.lagda.md | 7 + src/Cat/Diagram/Colimit/Cocone.lagda.md | 9 ++ src/Cat/Diagram/Coproduct/Copower.lagda.md | 29 ++-- src/Cat/Diagram/Image.lagda.md | 24 +-- src/Cat/Diagram/Initial.lagda.md | 18 ++- src/Cat/Diagram/Limit/Base.lagda.md | 7 + src/Cat/Diagram/Limit/Cone.lagda.md | 13 +- src/Cat/Diagram/Monad.lagda.md | 11 ++ src/Cat/Diagram/Monad/Extension.lagda.md | 30 +++- src/Cat/Diagram/Monad/Relative.lagda.md | 17 +- src/Cat/Diagram/Product.lagda.md | 13 +- src/Cat/Diagram/Pullback.lagda.md | 32 +++- src/Cat/Diagram/Sieve.lagda.md | 4 +- src/Cat/Diagram/Terminal.lagda.md | 6 +- src/Cat/Diagram/Zero.lagda.md | 11 +- src/Cat/Displayed/Bifibration.lagda.md | 12 +- src/Cat/Displayed/Cartesian.lagda.md | 10 +- src/Cat/Displayed/Cocartesian.lagda.md | 4 +- src/Cat/Displayed/Fibre.lagda.md | 7 + src/Cat/Displayed/GenericObject.lagda.md | 9 +- src/Cat/Displayed/Instances/Family.lagda.md | 3 +- src/Cat/Displayed/Instances/Opposite.lagda.md | 13 +- .../Displayed/Instances/Subobjects.lagda.md | 13 ++ src/Cat/Displayed/Total.lagda.md | 19 ++- src/Cat/Displayed/Total/Op.lagda.md | 10 ++ src/Cat/Functor/Adjoint.lagda.md | 28 +++- src/Cat/Functor/Adjoint/Hom.lagda.md | 13 +- src/Cat/Functor/Algebra.lagda.md | 7 +- src/Cat/Functor/Amnestic.lagda.md | 2 + src/Cat/Functor/Equivalence.lagda.md | 12 +- src/Cat/Functor/Kan/Adjoint.lagda.md | 2 - src/Cat/Functor/Monadic/Beck.lagda.md | 25 +-- src/Cat/Functor/Morphism.lagda.md | 16 +- src/Cat/Functor/Properties.lagda.md | 12 +- src/Cat/Functor/Pullback.lagda.md | 2 + src/Cat/Gaunt.lagda.md | 12 +- src/Cat/Groupoid.lagda.md | 4 +- src/Cat/Instances/Comma.lagda.md | 10 ++ src/Cat/Instances/Delooping.lagda.md | 3 +- src/Cat/Instances/Elements/Covariant.lagda.md | 11 +- src/Cat/Instances/Free.lagda.md | 4 +- src/Cat/Instances/Monads.lagda.md | 4 +- src/Cat/Instances/Shape/Join.lagda.md | 15 +- src/Cat/Morphism.lagda.md | 16 +- src/Cat/Regular.lagda.md | 4 +- src/Cat/Skeletal.lagda.md | 7 +- src/Cat/Strict.lagda.md | 14 +- src/Data/Fin/Base.lagda.md | 2 + src/Data/Fin/Finite.lagda.md | 4 + src/Data/Int/Universal.lagda.md | 18 ++- src/Data/Set/Coequaliser.lagda.md | 14 ++ src/Data/Set/Projective.lagda.md | 13 +- src/Data/Set/Truncation.lagda.md | 10 ++ src/Homotopy/Conjugation.lagda.md | 5 + src/Homotopy/Connectedness.lagda.md | 4 + src/Homotopy/Space/Circle.lagda.md | 20 ++- src/Homotopy/Space/Delooping.lagda.md | 11 ++ src/Homotopy/Space/Suspension.lagda.md | 2 + src/Order/Diagram/Bottom.lagda.md | 14 +- src/Order/Diagram/Join.lagda.md | 13 +- src/Order/Diagram/Meet.lagda.md | 13 +- src/Order/Semilattice/Join.lagda.md | 13 +- src/Order/Semilattice/Meet.lagda.md | 13 +- 106 files changed, 975 insertions(+), 456 deletions(-) diff --git a/src/1Lab/Classical.lagda.md b/src/1Lab/Classical.lagda.md index 42220d040..29e890567 100644 --- a/src/1Lab/Classical.lagda.md +++ b/src/1Lab/Classical.lagda.md @@ -22,16 +22,22 @@ module 1Lab.Classical where While we do not assume any classical principles in the 1Lab, we can still state them and explore their consequences. -The **law of excluded middle** (LEM) is the defining principle of classical logic, -which states that any proposition is either true or false (in other words, -[[decidable]]). Of course, assuming this as an axiom requires giving up canonicity: -we could prove that, for example, any Turing machine either halts or does not halt, -but this would not give us any computational information. +The **law of excluded middle** (LEM) is the defining principle of +classical logic, which states that any proposition is either true or +false (in other words, [[decidable]]). Of course, assuming this as an +axiom requires giving up canonicity: we could prove that, for example, +any Turing machine either halts or does not halt, but this would not +give us any computational information. + +::: popup +The **law of excluded middle** says that every [[proposition]] is +[[decidable]]. ```agda LEM : Type LEM = ∀ (P : Ω) → Dec ∣ P ∣ ``` +::: Note that we cannot do without the assumption that $P$ is a proposition: the statement that all types are decidable is [[inconsistent with univalence|LEM-infty]]. @@ -65,14 +71,16 @@ LEM≃DNE = prop-ext LEM-is-prop DNE-is-prop LEM→DNE DNE→LEM ## Weak excluded middle {defines="weak-excluded-middle"} +::: {.popup .keep} The **weak law of excluded middle** (WLEM) is a slightly weaker variant -of excluded middle which asserts that every proposition is either false -or not false. +of [[excluded middle]], which asserts that every proposition is either +false or not false. ```agda WLEM : Type WLEM = ∀ (P : Ω) → Dec (¬ ∣ P ∣) ``` +::: As the name suggests, the law of excluded middle implies the weak law of excluded middle. @@ -91,8 +99,11 @@ WLEM-is-prop = hlevel 1 ## The axiom of choice {defines="axiom-of-choice"} -The **axiom of choice** is a stronger classical principle which allows us to commute -propositional truncations past Π types. +::: {.popup .keep} +The **axiom of choice** is a stronger classicality principle, which says +we can commute [[propositional truncations]] over dependent product +types (over [[sets]]). +::: ```agda Axiom-of-choice : Typeω @@ -112,9 +123,9 @@ _ = Fibration-equiv ``` --> -An equivalent and sometimes useful statement is that all surjections between sets -merely have a section. This is essentially jumping to the other side of the -`fibration equivalence`{.Agda ident=Fibration-equiv}. +An equivalent and sometimes useful statement is that all surjections +between sets merely have a section. This is essentially jumping to the +other side of the `fibration equivalence`{.Agda ident=Fibration-equiv}. ```agda Surjections-split : Typeω diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md index faaf0c27f..f1de8ea89 100644 --- a/src/1Lab/Equiv.lagda.md +++ b/src/1Lab/Equiv.lagda.md @@ -34,6 +34,7 @@ that page has a formalisation of its failure. [provably not the case]: 1Lab.Counterexamples.IsIso.html +:::{.definition #good-notion-of-equivalence} We must therefore define a property of functions which refines being an isomorphism but *is* an isomorphism: functions satisfying this property will be called equivalences. More specifically, we're looking for a @@ -51,6 +52,7 @@ family $\isequiv(f)$ which and its inverse map. - and finally, is an actual [[proposition]]. +::: Put concisely, we're looking to define a [[propositional truncation]] of $\isiso(f)$ --- one which allows us to conveniently project out the @@ -83,6 +85,7 @@ up by defining, and proving basic things about, isomorphisms. First, we define what it means for functions to be inverses of eachother, on both the left and the right. +::: {.popup .keep} ```agda is-left-inverse : (B → A) → (A → B) → Type _ is-left-inverse g f = (x : _) → g (f x) ≡ x @@ -94,6 +97,7 @@ is-right-inverse g f = (x : _) → f (g x) ≡ x A function $g$ which is both a left- and right inverse to $f$ is called a **two-sided inverse** (to $f$). To say that a function is an isomorphism is to equip it with a two-sided inverse. +::: ::: warning Despite the name `is-iso`{.Agda}, a two-sided inverse is actual *data* @@ -213,12 +217,17 @@ conjunction of the assertions above, just packaged in a way that does not require us to first define [[propositional truncations]]. A function is an **equivalence** if all of its fibres are contractible: +::: popup +A function $f : A \to B$ is an **equivalence** if the [[fibre]] $f^*(y)$ +over each point $y : B$ is [[contractible]]. + ```agda record is-equiv (f : A → B) : Type (level-of A ⊔ level-of B) where no-eta-equality field is-eqv : (y : B) → is-contr (fibre f y) ``` +::: -We define the **abelianisation** of a group $G$, $G^{ab}$. Rather than -defining it a quotient group (by the commutator subgroup $[G,G]$), we -directly define a group structure on a set-coequaliser. To emphasise the -difference between the groups and their underlying sets, we'll write -$G_0$ and $G^{ab}_0$ in the prose. +:::{.definition #abelianisation} +The **abelianisation** $G^{ab}$ of a [[group]] $G$ is the +[[universal|free object]] [[abelian group]] with a map from $G$: that +is, the [[reflection|reflective subcategory]] of $G$ into the category +of abelian groups. +::: + +Rather than constructing $G^{ab}$ as quotient group (by the commutator +subgroup $[G,G]$), we directly define a group structure on a +set-coequaliser. To emphasise the difference between the groups and +their underlying sets, we'll write $G_0$ and $G^{ab}_0$ in the prose. ```agda G^ab : Type ℓ diff --git a/src/Algebra/Group/Ab/Tensor.lagda.md b/src/Algebra/Group/Ab/Tensor.lagda.md index f3e0f52e3..a5e4f14cb 100644 --- a/src/Algebra/Group/Ab/Tensor.lagda.md +++ b/src/Algebra/Group/Ab/Tensor.lagda.md @@ -31,7 +31,8 @@ private variable A function $f : F \to G \to H$, where all types involved are equipped with [[abelian group]] structures, is called **bilinear** when it satisfies $f(x + y, z) = f(x, z) + f(y, z)$ and $f(x, y + z) = f(x, y) + -f(x, z)$: it is a group homomorphism in each of its arguments. +f(x, z)$: it is a [[group homomorphism]] separately in each of its +arguments. ```agda record Bilinear (A : Abelian-group ℓ) (B : Abelian-group ℓ') (C : Abelian-group ℓ'') : Type (ℓ ⊔ ℓ' ⊔ ℓ'') where diff --git a/src/Algebra/Group/Action.lagda.md b/src/Algebra/Group/Action.lagda.md index 328882469..e9e7860ff 100644 --- a/src/Algebra/Group/Action.lagda.md +++ b/src/Algebra/Group/Action.lagda.md @@ -77,6 +77,12 @@ beyond sets! We refer to a "self-isomorphism" as an [isomorphisms]: Cat.Morphism.html#isos +::: popup +The **automorphism group** of an object $X$ in some category $\cC$ is +the [[set]] of all [[isomorphisms]] $X \cong X$, with the group +operation being composition. +::: + ```agda module _ {o ℓ} (C : Precategory o ℓ) where private module C = Cat C diff --git a/src/Algebra/Group/Cayley.lagda.md b/src/Algebra/Group/Cayley.lagda.md index f59eaab83..3edda8d93 100644 --- a/src/Algebra/Group/Cayley.lagda.md +++ b/src/Algebra/Group/Cayley.lagda.md @@ -16,12 +16,14 @@ open Group-on (G .snd) renaming (underlying-set to G-set) # Cayley's theorem {defines="cayleys-theorem"} -Cayley's theorem says that any group $G$ admits a representation as a -subgroup of a [[symmetric group]], specifically the symmetric group acting -on the underlying set of $G$. - -First, recall that we get a family of equivalences $G \simeq G$ by multiplication -on the left, the [[principal action]] of $G$ on itself: +::: {.popup .keep} +Cayley's theorem says that any [[group]] $G$ admits a representation as a +subgroup of a [[symmetric group]], specifically the symmetric group +acting on the underlying [[set]] of $G$. +::: + +First, recall that we get a family of equivalences $G \simeq G$ by +multiplication on the left, the [[principal action]] of $G$ on itself: ```agda Cayley : ⌞ G ⌟ → ⌞ G ⌟ ≃ ⌞ G ⌟ diff --git a/src/Algebra/Group/Concrete.lagda.md b/src/Algebra/Group/Concrete.lagda.md index 20d739f07..4f64274c6 100644 --- a/src/Algebra/Group/Concrete.lagda.md +++ b/src/Algebra/Group/Concrete.lagda.md @@ -37,14 +37,16 @@ private variable # Concrete groups {defines="concrete-group"} -In homotopy type theory, we can give an alternative definition of [[groups]]: -they are the [[pointed|pointed type]], [[connected]] [[groupoids]]. -The idea is that those groupoids contain exactly the same information as their -[[fundamental group]]. +:::{.popup .keep} +In homotopy type theory, we can give an alternative definition of +[[groups]]: they are the [[pointed|pointed type]], [[connected]] +[[groupoids]]. The idea is that those groupoids contain exactly the same +information as their [[fundamental group]]. -Such groups are dubbed **concrete**, because they represent the groups of symmetries -of a given object (the base point); by opposition, "algebraic" `Group`{.Agda}s are -called **abstract**. +Such groups are dubbed **concrete**, because they represent the groups +of symmetries of a given object (the base point); by opposition, +"algebraic" `Group`{.Agda}s are called **abstract**. +::: ```agda record ConcreteGroup ℓ : Type (lsuc ℓ) where @@ -59,13 +61,14 @@ record ConcreteGroup ℓ : Type (lsuc ℓ) where pt = B .snd ``` -Given a concrete group $G$, the underlying pointed type is denoted $\B{G}$, by analogy -with the [[delooping]] of an abstract group; note that, here, the delooping *is* the -chosen representation of $G$, so `B`{.Agda} is just a record field. -We write $\point{G}$ for the base point. +Given a concrete group $G$, the underlying pointed type is denoted +$\B{G}$, by analogy with the [[delooping]] of an abstract group; note +that, here, the delooping *is* the chosen representation of $G$, so +`B`{.Agda} is just a record field. We write $\point{G}$ for the base +point. -Concrete groups are pointed connected types, so they enjoy the following elimination -principle, which will be useful later: +Concrete groups are pointed connected types, so they enjoy the following +elimination principle, which will be useful later: ```agda B-elim-contr : {P : ⌞ B ⌟ → Type ℓ'} @@ -99,8 +102,8 @@ ConcreteGroup-path {G = G} {H} p = go prop! prop! where ``` --> -The [[delooping]] of a group is a concrete group. In fact, we will prove later that -*all* concrete groups arise as deloopings. +The [[delooping]] of a group is a concrete group. In fact, we will prove +later that *all* concrete groups arise as deloopings. ```agda Concrete : ∀ {ℓ} → Group ℓ → ConcreteGroup ℓ @@ -109,8 +112,8 @@ Concrete G .has-is-connected = Deloop-is-connected Concrete G .has-is-groupoid = squash ``` -Another important example of a concrete group is the [[circle]]: the delooping of -the [[integers]]. +Another important example of a concrete group is the [[circle]]: the +delooping of the [[integers]]. ```agda opaque @@ -125,11 +128,12 @@ S¹-concrete .has-is-groupoid = S¹-is-groupoid ## The category of concrete groups -The notion of group *homomorphism* between two groups $G$ and $H$ gets translated -to, on the "concrete" side, [[*pointed* maps]] $\B{G} \to^\bullet \B{H}$. +The notion of group *homomorphism* between two groups $G$ and $H$ gets +translated to, on the "concrete" side, [[*pointed* maps]] $\B{G} +\to^\bullet \B{H}$. -The pointedness condition ensures that these maps behave like abstract group -homomorphisms; in particular, that they form a *set*. +The pointedness condition ensures that these maps behave like abstract +group homomorphisms; in particular, that they form a *set*. ```agda ConcreteGroups-Hom-set @@ -160,8 +164,9 @@ ConcreteGroups _ .Hom-set = ConcreteGroups-Hom-set
-The rest of the categorical structure is inherited from pointed functions, and -univalence follows from the [[univalence]] of the universe of groupoids. +The rest of the categorical structure is inherited from pointed +functions, and univalence follows from the [[univalence]] of the +universe of groupoids. ```agda @@ -190,12 +195,12 @@ ConcreteGroups-is-category {ℓ} .to-path-over im = ≅-pathp (ConcreteGroups ## Concrete vs. abstract -Our goal is now to prove that concrete groups and abstract groups are equivalent, -in the sense that there is an [[equivalence of categories]] between `ConcreteGroups`{.Agda} -and `Groups`{.Agda}. +Our goal is now to prove that concrete groups and abstract groups are +equivalent, in the sense that there is an [[equivalence of categories]] +between `ConcreteGroups`{.Agda} and `Groups`{.Agda}. -Since we're dealing with groupoids, we can use the alternative definition of -the fundamental group that avoids set truncations. +Since we're dealing with groupoids, we can use the alternative +definition of the fundamental group that avoids set truncations. ```agda module _ (G : ConcreteGroup ℓ) where @@ -204,11 +209,12 @@ module _ (G : ConcreteGroup ℓ) where public ``` -We define a [[functor]] from concrete groups to abstract groups. -The object mapping is given by taking the `fundamental group`{.Agda ident=π₁B}. -Given a pointed map $f : \B{G} \to^\bullet \B{H}$, we can `ap`{.Agda}ply it to a loop -on $\point{G}$ to get a loop on $f(\point{G})$; then, we use the fact that $f$ -is pointed to get a loop on $\point{H}$ by [[conjugation]]. +We define a [[functor]] from concrete groups to abstract groups. The +object mapping is given by taking the `fundamental group`{.Agda +ident=π₁B}. Given a pointed map $f : \B{G} \to^\bullet \B{H}$, we can +`ap`{.Agda}ply it to a loop on $\point{G}$ to get a loop on +$f(\point{G})$; then, we use the fact that $f$ is pointed to get a loop +on $\point{H}$ by [[conjugation]]. ```agda π₁F : Functor (ConcreteGroups ℓ) (Groups ℓ) @@ -216,8 +222,8 @@ is pointed to get a loop on $\point{H}$ by [[conjugation]]. π₁F .F₁ (f , ptf) .hom x = conj ptf (ap f x) ``` -By some simple path yoga, this preserves multiplication, and the construction is -functorial: +By some simple path yoga, this preserves multiplication, and the +construction is functorial: ```agda π₁F .F₁ (f , ptf) .preserves .pres-⋆ x y = @@ -232,10 +238,10 @@ functorial: conj ptf (ap f (conj ptg (ap g x))) ∎ ``` -We start by showing that `π₁F`{.Agda} is [[split essentially surjective]]. This is the -easy part: to build a concrete group out of an abstract group, we simply take its -`Deloop`{.Agda}ing, and use the fact that the fundamental group of the delooping -recovers the original group. +We start by showing that `π₁F`{.Agda} is [[split essentially +surjective]]. This is the easy part: to build a concrete group out of an +abstract group, we simply take its `Deloop`{.Agda}ing, and use the fact +that the fundamental group of the delooping recovers the original group. -# Subgroups +# Subgroups {defines="subgroup"} -A **subgroup** $m$ of a group $G$ is a [[monomorphism]] $H \xto{m} G$, -that is, an object of the [[poset of subobjects]] $\Sub(G)$. Since group -homomorphisms are injective exactly when their underlying function is an -[[embedding]], we can alternatively describe this as a condition on a -predicate $G \to \prop$. +::: {.popup .keep} +A **subgroup** $m$ of a group $G$ is a [[monomorphism]] $H \xmono{m} G$, +that is, an object of the [[poset of subobjects]] $\Sub(G)$. Since +[[group homomorphisms]] are injective exactly when their underlying +function is an [[embedding]], we can alternatively describe this as a +condition on a predicate $G \to \prop$. ```agda Subgroup : Group ℓ → Type (lsuc ℓ) @@ -45,6 +46,7 @@ Subgroup {ℓ = ℓ} G = Subobject G A proposition $H : G \to \prop$ of a group $(G, \star)$ **represents a subgroup** if it contains the group `unit`{.Agda}, is closed under multiplication, and is closed under inverses. +::: ```agda record represents-subgroup (G : Group ℓ) (H : ℙ ⌞ G ⌟) : Type ℓ where diff --git a/src/Algebra/Monoid.lagda.md b/src/Algebra/Monoid.lagda.md index 4125ac027..34a9ed0c6 100644 --- a/src/Algebra/Monoid.lagda.md +++ b/src/Algebra/Monoid.lagda.md @@ -20,7 +20,7 @@ private variable # Monoids {defines="monoid"} -A **monoid** is a semigroup equipped with a _two-sided identity_ +A **monoid** is a [[semigroup]] equipped with a _two-sided identity_ element: An element $e \in M$ such that $e \star x = x = x \star e$. For any particular choice of binary operator $\star$, if a two-sided identity exists, then it is unique; In this sense, "being a monoid" diff --git a/src/Algebra/Ring.lagda.md b/src/Algebra/Ring.lagda.md index 77f320e93..035697237 100644 --- a/src/Algebra/Ring.lagda.md +++ b/src/Algebra/Ring.lagda.md @@ -34,12 +34,20 @@ include square matrices (with values in a ring) and the integral cohomology ring of a topological space: that these are so far from being "number-like" indicates the incredible generality of rings. +::: {.popup .keep} A **ring** is an [[abelian group]] $R$ (which we call the **additive group** of $R$), together with the data of a monoid on $R$ (the **multiplicative monoid**), where the multiplication of the monoid -_distributes over_ the addition. We'll see why this compatibility -condition is required afterwards. Check out what it means for a triple -$(1, *, +)$ to be a ring structure on a type: +_distributes over_ the addition, i.e. where we have +$$\begin{align*} +x(y + z) &= xy + xz \\ +(y + z)x &= yx + zx\text{.} +\end{align*}$$ +::: + +We'll see why this compatibility condition is required afterwards. Check +out what it means for a triple $(1, *, +)$ to be a ring structure on a +type: ```agda record is-ring {ℓ} {R : Type ℓ} (1r : R) (_*_ _+_ : R → R → R) : Type ℓ where diff --git a/src/Algebra/Ring/Ideal.lagda.md b/src/Algebra/Ring/Ideal.lagda.md index d5bc464b9..222680108 100644 --- a/src/Algebra/Ring/Ideal.lagda.md +++ b/src/Algebra/Ring/Ideal.lagda.md @@ -21,30 +21,27 @@ import Algebra.Ring.Reasoning as Ringr module Algebra.Ring.Ideal where ``` -# Ideals in rings - -An **ideal** in a ring $R$ is the [$\Ab$-enriched] analogue of a -[sieve], when $R$ is considered as an $\Ab$-category with a single -object, in that it picks out a sub-[$R$-module] of $R$, considered as a -[representable module], in exactly the same way that a sieve on an -object $x : \cC$ picks out a subfunctor of $\yo(x)$. Since we know that -$\baut R$'s composition is given by $R$'s multiplication, and sieves are -subsets closed under precomposition, we instantly deduce that ideals are -closed under multiplication. - -[$\Ab$-enriched]: Cat.Abelian.Base.html#ab-enriched-categories -[sieve]: Cat.Diagram.Sieve.html -[$R$-module]: Algebra.Ring.Module.html#modules +# Ideals in rings {defines="ideal"} + +An **ideal** in a ring $R$ is the [[$\Ab$-enriched|Ab-enriched +category]] analogue of a [[sieve]], when $R$ is considered as an +$\Ab$-category with a single object, in that it picks out a +sub-[[$R$-module|module]] of $R$, considered as a [representable module], in +exactly the same way that a sieve on an object $x : \cC$ picks out a +subfunctor of $\yo(x)$. Since we know that $\baut R$'s composition is +given by $R$'s multiplication, and sieves are subsets closed under +precomposition, we instantly deduce that ideals are closed under +multiplication. + [representable module]: Algebra.Ring.Module.html#representable-modules In the $\Ab$-enriched setting, however, there are some more operations -that leaves us in the same $\hom$-group: addition! More generally, the +that leave us in the same $\hom$-group: addition! More generally, the [[abelian group]] operations, i.e. addition, inverse, and the zero morphism. Putting these together we conclude that an ideal in $R$ is a subset of $R$ containing the identity, which is closed under multiplication and addition. - ```agda module _ {ℓ} (R : Ring ℓ) where private module R = Ringr R @@ -59,7 +56,14 @@ module _ {ℓ} (R : Ring ℓ) where has-*ᵣ : ∀ x {y} → y ∈ 𝔞 → (y R.* x) ∈ 𝔞 ``` -:::{.note} +::: popup +An **ideal** of a [[ring]] $R$ (generally [[commutative|ring]]) is a +subset $I \sube R$ which is a [[subgroup]] of $R$'s additive group, and +is furthermore closed under multiplication: if $y \in I$, then so are +$xy$ and $yx$. +::: + +::: note Since most of the rings over which we want to consider ideals are _commutative_ rings, we will limit ourselves to the definition of _two-sided_ ideals: Those for which we have, for $y \in \mathfrak{a}$ @@ -82,13 +86,11 @@ and any element $x : R$, $xy \in \mathfrak{a}$ and $yx \in ``` --> -Since an ideal is a [subgroup] of $R$'s additive group, its total space +Since an ideal is a [[subgroup]] of $R$'s additive group, its total space inherits a group structure, and since multiplication in $R$ distributes over addition in $R$, the group structure induced on $\mathfrak{a}$ carries a canonical $R$-module structure. -[subgroup]: Algebra.Group.Subgroup.html - ```agda ideal→module : (𝔞 : ℙ ⌞ R ⌟) → is-ideal 𝔞 → Module R ℓ ideal→module 𝔞 x = g .fst , mod where diff --git a/src/Algebra/Ring/Module/Category.lagda.md b/src/Algebra/Ring/Module/Category.lagda.md index 2aa1a9ee2..1789a6312 100644 --- a/src/Algebra/Ring/Module/Category.lagda.md +++ b/src/Algebra/Ring/Module/Category.lagda.md @@ -183,11 +183,11 @@ R-Mod-ab-category .∘-linear-r {B = B} {C} f g h = ext λ x → ## Finite biproducts -Let's now prove that $R$-Mod is a preadditive category. This is exactly -as in $\Ab$: The zero object is the zero group, equipped with its unique -choice of $R$-module structure, and direct products $M \oplus N$ are -given by direct products of the underlying groups $M_G \oplus N_G$ with -the canonical choice of $R$-module structure. +Let's now prove that $R$-Mod is an [[additive category]]. This is +exactly as in $\Ab$: The [[zero object]] is the [[zero group]], equipped +with its unique choice of $R$-module structure, and direct products $M +\oplus N$ are given by direct products of the underlying groups $M_G +\oplus N_G$ with the canonical choice of $R$-module structure. The zero object is simple, because the unit type is so well-behaved^[and `Lift` types, too] when it comes to definitional equality: Everything is diff --git a/src/Algebra/Ring/Quotient.lagda.md b/src/Algebra/Ring/Quotient.lagda.md index e67e4811c..b3231c6ae 100644 --- a/src/Algebra/Ring/Quotient.lagda.md +++ b/src/Algebra/Ring/Quotient.lagda.md @@ -28,7 +28,7 @@ private module R = Kit R # Quotient rings -Let $R$ be a [[ring]] and $I \sube R$ be an ideal. Because rings have an +Let $R$ be a [[ring]] and $I \sube R$ be an [[ideal]]. Because rings have an underlying [[abelian group]], the ideal $I \sube R$ determines a normal subgroup $I$ of $R$'s additive group, so that we may form the quotient group $R/I$. And since ideals are closed under multiplication^[recall diff --git a/src/Cat/Abelian/Base.lagda.md b/src/Cat/Abelian/Base.lagda.md index 5a685afff..7c967b1f7 100644 --- a/src/Cat/Abelian/Base.lagda.md +++ b/src/Cat/Abelian/Base.lagda.md @@ -36,21 +36,23 @@ abelian categories: Ab-enriched categories, pre-additive categories, pre-abelian categories, and abelian categories. Each concept builds on the last by adding a new categorical property on top of a precategory. -## Ab-enriched categories {defines="ab-enriched-category"} +## Ab-enriched categories +:::{.definition #ab-enriched-category} An $\Ab$-enriched category is one where each $\hom$ set carries the structure of an [[Abelian group]], such that the composition map is _bilinear_, hence extending to an Abelian group homomorphism - $$ \hom(b, c) \otimes \hom(a, b) \to \hom(a, c) $$, - where the term on the left is the [[tensor product|tensor product of -abelian groups]] of the corresponding $\hom$-groups. As the name -implies, every such category has a canonical $\Ab$-enrichment (made -monoidal using $- \otimes -$), but we do not use the language of -enriched category theory in our development of Abelian categories. +abelian groups]] of the corresponding $\hom$-groups. +::: + +As the name implies, every such category has a canonical +$\Ab$-enrichment (made monoidal using $- \otimes -$), but we do not use +the language of enriched category theory in our development of Abelian +categories. [zero object]: Cat.Diagram.Zero.html @@ -184,6 +186,11 @@ module _ where ## Additive categories {defines="additive-category"} +::: popup +An [[$\Ab$-category|ab-enriched category]] $\cC$ is **additive** when +$\cC$ has finite [[biproducts]] and a [[zero object]]. +::: + An $\Ab$-category is **additive** when its underlying category has a [[terminal object]] and finite [[products]]; By the yoga above, this implies that the terminal object is also a zero object, and the finite @@ -211,27 +218,23 @@ record is-additive {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ lsuc ℓ) where Coincidence of finite products and finite coproducts leads to an object commonly called a (finite) **[[biproduct]]**. The coproduct coprojections are given by the pair of maps - $$ \begin{align*} &\langle \id , 0 \rangle : A \to A \times B \\ &\langle 0 , \id \rangle : B \to A \times B\text{,} \end{align*} $$ - respectively, and the comultiplication of $f$ and $g$ is given by $f\pi_1 + g\pi_2$. We can calculate, for the first coprojection followed by comultiplication, - $$ \begin{align*} -& (f\pi_1+g\pi_2) \langle \id , 0 \rangle \\ -=& f\pi_1\langle \id , 0 \rangle + g\pi_2\langle \id , 0 \rangle \\ -=& f\id + g0 \\ -=& f\text{,} +(f\pi_1+g\pi_2) \langle \id , 0 \rangle + & = f\pi_1\langle \id , 0 \rangle + g\pi_2\langle \id , 0 \rangle \\ + & = f\id + g0 \\ + & = f\text{,} \end{align*} $$ - and analogously for the second coprojection followed by comultiplication. diff --git a/src/Cat/Allegory/Base.lagda.md b/src/Cat/Allegory/Base.lagda.md index beaf66251..6f68f7aaf 100644 --- a/src/Cat/Allegory/Base.lagda.md +++ b/src/Cat/Allegory/Base.lagda.md @@ -112,6 +112,18 @@ monoids.^[as a hint: _joins_ in your lattice become composition] → (g ∘ f) ∩ h ≤ g ∘ (f ∩ (g † ∘ h)) ``` +:::{.popup .summary} +An **allegory** $\cA$ is a locally [[thin|thin category]] [[bicategory]] +where each of the [[posets]] $\hom_\cA(x, y)$ has [[binary meets|meet]]; +we write $x \rel y$ for $\hom_\cA(x, y)$. Additionally, $\cA$ must be +equipped with an [[order-preserving|monotone map]] **duality** +involution $(-)\dag$, sending $x \rel y$ to $y \rel x$, compatible with +composition, and which satisfies the **modular law** +$$ +(g \circ f) \cap h \le g \circ (f \cap (g\dag \circ h)) +$$. +::: + ## Quick theorems The first thing we observe about allegories is a Yoneda-type lemma for diff --git a/src/Cat/Allegory/Instances/Mat.lagda.md b/src/Cat/Allegory/Instances/Mat.lagda.md index 537fa3925..34e28d799 100644 --- a/src/Cat/Allegory/Instances/Mat.lagda.md +++ b/src/Cat/Allegory/Instances/Mat.lagda.md @@ -18,11 +18,10 @@ module Cat.Allegory.Instances.Mat where Let $L$ be a [frame]: it could be the frame of opens of a locale, for example. It turns out that $L$ has enough structure that we can define -an [allegory], where the objects are sets, and the morphisms $A \rel B$ +an [[allegory]], where the objects are sets, and the morphisms $A \rel B$ are given by $A \times B$-matrices valued in $L$. [frame]: Order.Frame.html -[allegory]: Cat.Allegory.Base.html -# Products +# Products {defines="product"} -:::{.definition #product} The **product** $P$ of two objects $A$ and $B$, if it exists, is the smallest object equipped with "projection" maps $P \to A$ and $P \to B$. This situation can be visualised by putting the data of a product into a @@ -28,7 +27,12 @@ commutative diagram, as the one below: To express that $P$ is the _smallest_ object with projections to $A$ and $B$, we ask that any other object $Q$ with projections through $A$ and $B$ factors uniquely through $P$: -::: + +::: popup +The **product** $P$ of two objects $A, B : \cC$ is the [[terminal]] +object equipped with maps $A \xot{p} P \xto{q} Q$, i.e. such that if $Q$ +is as in the diagram below, there exists a [[unique|contractible]] +dotted arrow making both outer triangles commute. ~~~{.quiver} \[\begin{tikzcd} @@ -41,10 +45,11 @@ $P$: \arrow[from=1-2, to=2-3] \end{tikzcd}\] ~~~ +::: In the sense that [[(univalent) categories|univalent category]] generalise posets, the product of $A$ and $B$ --- if it exists --- -generalises the binary meet $A \wedge B$. Since products are +generalises the binary [[meet]] $A \wedge B$. Since products are [unique](#uniqueness) when they exist, we may safely denote any product of $A$ and $B$ by $A \times B$. diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md index 23c61336e..2544ad888 100644 --- a/src/Cat/Diagram/Pullback.lagda.md +++ b/src/Cat/Diagram/Pullback.lagda.md @@ -22,11 +22,35 @@ module _ {o ℓ} (C : Precategory o ℓ) where ``` --> +::: {.popup .keep} A **pullback** $X \times_Z Y$ of $f : X \to Z$ and $g : Y \to Z$ is the -[[product]] of $f$ and $g$ in the category $\cC/Z$, the category of -objects fibred over $Z$. We note that the fibre of $X \times_Z Y$ over -some element $x$ of $Z$ is the product of the fibres of $f$ and $g$ over -$x$; Hence the pullback is also called the **fibred product**. +[[product]] of $f$ and $g$ in the [[slice category]] $\cC/Z$, the +category of objects fibred over $Z$. We note that the [[fibre]] of $X +\times_Z Y$ over some element $x$ of $Z$ is the product of the fibres of +$f$ and $g$ over $x$; Hence the pullback is also called the **fibred +product**. +::: + +::: popup-only +Put another way, the pullback $X \times_Z Y$ is the [[terminal]] object +of $\cC$ equipped with maps $X \xot{p} X \times_Z Y \xto{q} Y$ making +the square + +~~~{.quiver} +\[\begin{tikzcd}[ampersand replacement=\&] + {X \times_Z Y} \&\& X \\ + \\ + X \&\& Z + \arrow["p", from=1-1, to=1-3] + \arrow["q"', from=1-1, to=3-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3] + \arrow["f", from=1-3, to=3-3] + \arrow["g"', from=3-1, to=3-3] +\end{tikzcd}\] +~~~ + +commute. +::: ```agda record is-pullback {P} (p₁ : Hom P X) (f : Hom X Z) (p₂ : Hom P Y) (g : Hom Y Z) diff --git a/src/Cat/Diagram/Sieve.lagda.md b/src/Cat/Diagram/Sieve.lagda.md index b4d2906dd..6b432d95d 100644 --- a/src/Cat/Diagram/Sieve.lagda.md +++ b/src/Cat/Diagram/Sieve.lagda.md @@ -26,10 +26,12 @@ module _ {o κ : _} (C : Precategory o κ) (c : ⌞ C ⌟) where # Sieves {defines="sieve"} +::: {.popup .keep} Given a category $\cC$, a **sieve** on an object $c$ Is a subset of -the maps $a \to c$ closed under composition: If $f \in S$, then $(f +the maps $a \to c$ closed under composition: if $f \in S$, then $(f \circ g) \in S$. The data of a sieve on $c$ corresponds to the data of a subobject of $\yo(c)$, considered as an object of $\psh(\cC)$. +::: Here, the subset is represented as the function `arrows`{.agda}, which, given an arrow $f : a \to c$ (and its domain), yields a proposition diff --git a/src/Cat/Diagram/Terminal.lagda.md b/src/Cat/Diagram/Terminal.lagda.md index ba9a405ab..d459f2066 100644 --- a/src/Cat/Diagram/Terminal.lagda.md +++ b/src/Cat/Diagram/Terminal.lagda.md @@ -22,13 +22,17 @@ module _ {o h} (C : Precategory o h) where # Terminal objects {defines="terminal-object terminal"} +::: {.popup .keep} An object $\top$ of a category $\mathcal{C}$ is said to be **terminal** -if it admits a _unique_ map from any other object: +if it admits a _unique_ map $! : X \to \top$ into any other object. ```agda is-terminal : Ob → Type _ is-terminal ob = ∀ x → is-contr (Hom x ob) +``` +::: +```agda record Terminal : Type (o ⊔ h) where field top : Ob diff --git a/src/Cat/Diagram/Zero.lagda.md b/src/Cat/Diagram/Zero.lagda.md index 0149f671d..50d2df4c0 100644 --- a/src/Cat/Diagram/Zero.lagda.md +++ b/src/Cat/Diagram/Zero.lagda.md @@ -22,8 +22,10 @@ module _ {o h} (C : Precategory o h) where # Zero objects {defines="zero-object"} -In some categories, `Initial`{.Agda} and `Terminal`{.Agda} objects +::: {.popup .keep} +In some categories, [[initial]] and [[terminal]] objects coincide. When this occurs, we call the object a **zero object**. +::: ```agda record is-zero (ob : Ob) : Type (o ⊔ h) where @@ -49,9 +51,10 @@ coincide. When this occurs, we call the object a **zero object**. ``` ::: {.definition #zero-morphism} -A curious fact about zero objects is that their existence implies that -every hom set is inhabited! Between any objects $x$ and $y$ the morphism -$0 = ¡ \circ ! : x \to y$ is called the **zero morphism**. +If $\cC$ has a [[zero object]] $\emptyset$, then every $\hom$-set +$\cC(x, y)$ is [[pointed]], by the composite $$x \xto{!} \emptyset +\xto{¡} y$$; we refer to a map which factors through a zero object as a +**zero morphism**. ::: ```agda diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md index f5c9a7c35..b215901ae 100644 --- a/src/Cat/Displayed/Bifibration.lagda.md +++ b/src/Cat/Displayed/Bifibration.lagda.md @@ -45,11 +45,13 @@ private # Bifibrations {defines="bifibration"} +::: {.popup .keep} A [[displayed category]] $\cE \liesover \cB$ is a **bifibration** if is -it both a [[fibration|cartesian fibration]] and an opfibration. This -means that $\cE$ is equipped with both [reindexing] and [opreindexing] -functors, which allows us to both restrict and extend along morphisms $X -\to Y$ in the base. +it both a [[fibration|cartesian fibration]] and an +[[opfibration|cocartesian fibration]]. This means that $\cE$ is equipped +with both [reindexing] and [opreindexing] functors, which allows us to +both restrict and extend along morphisms $X \to Y$ in the base. +::: Note that a bifibration is *not* the same as a "profunctor valued in categories". Those are a distinct concept, called **two-sided @@ -66,7 +68,7 @@ when that page is written. ```agda record is-bifibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where field - fibration : Cartesian-fibration + fibration : Cartesian-fibration opfibration : Cocartesian-fibration module fibration = Cartesian-fibration fibration diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md index c5e68ebf4..0e17c2ecf 100644 --- a/src/Cat/Displayed/Cartesian.lagda.md +++ b/src/Cat/Displayed/Cartesian.lagda.md @@ -650,10 +650,12 @@ cartesian→postcompose-equiv cart = ## Cartesian lifts {defines="cartesian-lift"} -We call an object $y'$ over $y$ together with a Cartesian arrow $f' : x' -\to y'$ a _Cartesian lift_ of $f$. Cartesian lifts, defined by universal -property as they are, are unique when they exist, so that "having -Cartesian lifts" is a _property_, not a structure. +::: {.popup .keep} +We call an object $y'$ over $y$ together with a [[Cartesian morphism]] +$f' : x' \to y'$ a **Cartesian lift** of $f$. Cartesian lifts, defined +by universal property as they are, are unique when they exist, so that +"having Cartesian lifts" is a [[property]], not structure. +::: ```agda record diff --git a/src/Cat/Displayed/Cocartesian.lagda.md b/src/Cat/Displayed/Cocartesian.lagda.md index 32c233e44..2c55c1723 100644 --- a/src/Cat/Displayed/Cocartesian.lagda.md +++ b/src/Cat/Displayed/Cocartesian.lagda.md @@ -179,11 +179,9 @@ record Cocartesian-morphism As noted before, cocartesian maps the are duals to [[cartesian maps]]. We can make this correspondence precise by showing that cartesian maps -in the [total opposite] of $\ca{E}$ are cocartesian maps, and vice +in the [[total opposite]] of $\ca{E}$ are cocartesian maps, and vice versa. -[total opposite]: Cat.Displayed.Total.Op.html - ```agda co-cartesian→cocartesian : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'} diff --git a/src/Cat/Displayed/Fibre.lagda.md b/src/Cat/Displayed/Fibre.lagda.md index a0d60011f..083e3dd50 100644 --- a/src/Cat/Displayed/Fibre.lagda.md +++ b/src/Cat/Displayed/Fibre.lagda.md @@ -74,6 +74,13 @@ $\id\circ\id=\id$ from the base category, implies that the set of vertical arrows over an object $x$ contain identities and are closed under composition, the **fibre (pre)category over $x$**. +::: popup +The **fibre category** $\cE^*(X)$ of a [[displayed category]] $\cE +\liesover \cB$ over an object $X : \cB$ is the category with type of +objects $\cE(X)$, and with morphisms $$\hom(x, y) = \cE_{\id}(x, y)$$ +the set of **vertical maps** between $x$ and $y$. +::: + ```agda Fibre' : (X : Ob) diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md index 2b6bf5c84..fa6a05a64 100644 --- a/src/Cat/Displayed/GenericObject.lagda.md +++ b/src/Cat/Displayed/GenericObject.lagda.md @@ -192,11 +192,10 @@ $u$ be generated by the structure we have equipped $t'$ with, but $u'$ must, as well. We can also expand on what this means for the family fibration: -$\rm{Fam}({\cC})$ has a gaunt generic object if and only if $\cC$ is itself -[gaunt] (See [here](Cat.Displayed.Instances.Family.html#gaunt-generic-objects) -for the proof). - -[gaunt]: Cat.Gaunt.html +$\rm{Fam}({\cC})$ has a gaunt generic object if and only if $\cC$ is +itself [[gaunt]] (See +[here](Cat.Displayed.Instances.Family.html#gaunt-generic-objects) for +the proof). -# Adjoint functors +# Adjoint functors {defines="adjoint-functor adjunction left-adjoint right-adjoint adjoint"} Category theory is, in general, the study of how things can be related. For instance, structures at the level of sets (e.g. the collection of @@ -127,12 +127,13 @@ commutative diagrams: -:::{.definition .summary #adjoint-functor alias="adjunction left-adjoint right-adjoint adjoint"} +:::{.popup .summary} A pair of functors $F : \cC \to \cD$, $G : \cD \to \cC$ are **adjoints**, written $F \dashv G$, when we have natural transformations $\eta : \Id \To GF$ and $\eps : FG \To \Id$ satisfying the **triangle -identities** $\eps \circ F\eta = \id$ and $R\eps \circ \eta = \id$. In -this situation, $F$ is the **left adjoint** and $G$ is the **right +identities** $\eps \circ F\eta = \id$ and $R\eps \circ \eta = \id$. + +In this situation, $F$ is the **left adjoint** and $G$ is the **right adjoint**. ::: @@ -194,6 +195,17 @@ module _ {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) where ``` --> +::: popup +If $L \dashv R$ are [[adjoint functors]], the **adjunct** of a morphism +$f : \hom_\cD(La, b)$ is the composite $$ a \xto{\eta} RLx \xto{R(f)} Rb +$$. Symmetrically, the adjunct of a morphism $g : \hom_\cD(a, Rb)$ is +the composite $$ La \xto{L(g)} LRb \xto{\eps} b $$. + +These assignments are [[natural|natural transformation]] inverse +[[equivalences]] between the $\hom$-functors $$\hom_\cC(L(-), -) \cong +\hom_\cD(-, R(-))$$. +::: + ```agda L-adjunct : ∀ {a b} → D.Hom (L.₀ a) b → C.Hom a (R.₀ b) L-adjunct f = R.₁ f C.∘ adj.η _ @@ -201,6 +213,7 @@ module _ {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) where R-adjunct : ∀ {a b} → C.Hom a (R.₀ b) → D.Hom (L.₀ a) b R-adjunct f = adj.ε _ D.∘ L.₁ f ``` +::: The important part that the actual data of an adjunction gets you is these functions are inverse _equivalences_ between the hom-sets @@ -369,15 +382,18 @@ module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} (U : ``` --> -::: {.definition #free-object} +::: {.definition .popup #free-object} A **free object** on $X : \cC$, relative to $U : \cD \to \cC$, consists of an object $F(X) : \cD$ and an arrow $\eta : X \to UF(X)$, such that every $f : X \to UY$, $f$ factors uniquely through $\eta$. Expanding -this to an *operations-and"properties" presentation, we could say that: +this to an *operations-and-properties* presentation, we could say that: * There is a map `fold`{.Agda} from $\cD(X, UY)$ to $\cC(FX, Y)$, and * for every $f$, we have $U(\operatorname{fold} f)\eta = f$, and * for every $f$ and $g$, if $U(g)\eta = f$, then $g = \operatorname{fold} f$. + +If these conditions are satisfied, we refer to $\eta$ as a **universal +morphism from $X$ into $F$**. ::: ```agda diff --git a/src/Cat/Functor/Adjoint/Hom.lagda.md b/src/Cat/Functor/Adjoint/Hom.lagda.md index f14b6f2a8..9fd9fdc39 100644 --- a/src/Cat/Functor/Adjoint/Hom.lagda.md +++ b/src/Cat/Functor/Adjoint/Hom.lagda.md @@ -40,13 +40,22 @@ module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} # Adjoints as hom-isomorphisms {defines="adjoints-as-hom-isomorphisms"} +::: popup +An [[adjunction]] between functors $F : \cC \to \cD$ and $G : \cC \to +\cD$ can also be defined as a [[natural isomorphism]] of [[$\hom$ +functors]] +$$ +a : \hom_\cC(F(-), -) \cong \hom_\cD(-, G(-)) +$$ +whence the adjunction unit and counit are given componentwise as the +[[adjuncts]] of identity morphisms. +::: + Recall from the page on [[adjoint functors|adjuncts]] that an adjoint pair $L \dashv R$ induces an isomorphism - $$ \hom_\cC(L(x), y) \cong \hom_\cD(x, R(y)) $$ - of $\hom$-sets, sending each morphism to its left and right _adjuncts_, respectively. What that page does not mention is that any functors $L, R$ with such a correspondence --- as long as the isomorphism is diff --git a/src/Cat/Functor/Algebra.lagda.md b/src/Cat/Functor/Algebra.lagda.md index 2a55daa74..4fba4ac90 100644 --- a/src/Cat/Functor/Algebra.lagda.md +++ b/src/Cat/Functor/Algebra.lagda.md @@ -52,9 +52,12 @@ point and an endomap $X \to X$, the functor $X \mapsto A \times X + 1$ adds an extra point and a copy of $A$, etc. Consequently, a map $\cC(F(A), A)$ picks out a suitably structured $A$; e.g. writing a map $\cC(A + 1, A)$ requires $A$ to be equipped with a global element and an endomap $\cC(A,A)$. -In analogy to [[monad algebras]], a map $\cC(F(A),A)$ is called an + +:::{.popup .keep} +In analogy with [[monad algebras]], a map $\cC(F(A),A)$ is called an **F-algebra** on $A$^[Alternatively, we can view $F$-algebras as monad algebras over functors that lack algebraic structure.]. +::: Likewise, a map $f : \cC(A,B)$ between two $F$-algebras $\alpha : \cC(F(A),A)$ and $\beta : \cC(F(B), B)$ is an **F-algebra homomorphism** if it commutes @@ -175,7 +178,7 @@ $\Sets$, this initial algebra is the natural numbers! In general, initial $F$-algebras are how we give a categorical semantics to non-indexed inductive datatypes like `Nat`{.Agda} or `List`{.Agda}. -## Adámek's fixpoint theorem {defines="adameks-theorem"} +## Adámek's fixpoint theorem Note that initial $F$-algebras need not exist for a given functor $F$. Nevertheless, **Adámek's fixpoint theorem** lets us construct some diff --git a/src/Cat/Functor/Amnestic.lagda.md b/src/Cat/Functor/Amnestic.lagda.md index f9243cb5c..6f0d94012 100644 --- a/src/Cat/Functor/Amnestic.lagda.md +++ b/src/Cat/Functor/Amnestic.lagda.md @@ -62,12 +62,14 @@ module _ (F : Functor C D) where ``` --> +::: {.popup .keep} Let $f$ be an identity, i.e. it is such that $(a, b, f) \cong (c, c, \id)$. Any functor $F$ induces an identification $(Fa, Fb, Ff) \cong (Fc, Fc, id)$, meaning that it _preserves being an identity_. A functor is **amnestic** if it additionally _reflects_ being an identity: the natural map we have implicitly defined above (called `action`{.Agda}) is an equivalence. +::: ```agda action : ∀ {a b : C.Ob} (f : C.Hom a b) diff --git a/src/Cat/Functor/Equivalence.lagda.md b/src/Cat/Functor/Equivalence.lagda.md index 3982715cf..3f90f3fba 100644 --- a/src/Cat/Functor/Equivalence.lagda.md +++ b/src/Cat/Functor/Equivalence.lagda.md @@ -24,13 +24,13 @@ open _=>_ hiding (op) # Equivalences {defines="equivalence-of-categories"} +::: {.popup .keep} A functor $F : \cC \to \cD$ is an **equivalence of categories** when it has a [[right adjoint]] $G : \cD \to \cD$, with the unit and -counit natural transformations being [natural isomorphisms]. This +counit natural transformations being [[natural isomorphisms]]. This immediately implies that our adjoint pair $F \dashv G$ extends to an adjoint triple $F \dashv G \dashv F$. - -[natural isomorphisms]: Cat.Functor.Naturality.html +::: ```agda record is-equivalence (F : Functor C D) : Type (adj-level C D) where @@ -518,10 +518,11 @@ is-cat-equivalence→equiv-on-objects {C = C} {D = D} {F = F} ccat dcat eqv = ## Isomorphisms {defines="isomorphism-of-precategories"} +::: {.popup .keep} Another, more direct way of proving that a functor is an equivalence of precategories is proving that it is an **isomorphism of precategories**: -It's fully faithful, thus a typal equivalence of morphisms, and in -addition its action on objects is an equivalence of types. +It's [[fully faithful]], thus a typal equivalence of morphisms, and in +addition its action on objects is an [[equivalence]] of types. ```agda record is-precat-iso (F : Functor C D) : Type (adj-level C D) where @@ -531,6 +532,7 @@ record is-precat-iso (F : Functor C D) : Type (adj-level C D) where has-is-ff : is-fully-faithful F has-is-iso : is-equiv (F .F₀) ``` +::: Such a functor is (immediately) fully faithful, and the inverse `has-is-iso`{.Agda} means that it is split essentially surjective; For diff --git a/src/Cat/Functor/Kan/Adjoint.lagda.md b/src/Cat/Functor/Kan/Adjoint.lagda.md index 5e6769382..16b4eea78 100644 --- a/src/Cat/Functor/Kan/Adjoint.lagda.md +++ b/src/Cat/Functor/Kan/Adjoint.lagda.md @@ -31,11 +31,9 @@ private One way to think about [[Kan extensions]] is that, when they exist, they allow us to "compose" two functors when one of them is going the wrong way: given a span - $$ D \xot{F} C \xto{H} E $$ - we get a "composite" $\Lan_F(H) : D \to E$. With this perspective in mind, it's reasonable to expect that, if $F$ has an [inverse] $G : D \to C$, the composite we get should be the actual composite $H \circ G$. diff --git a/src/Cat/Functor/Monadic/Beck.lagda.md b/src/Cat/Functor/Monadic/Beck.lagda.md index ccab377c9..8e76d2de9 100644 --- a/src/Cat/Functor/Monadic/Beck.lagda.md +++ b/src/Cat/Functor/Monadic/Beck.lagda.md @@ -52,42 +52,33 @@ open Total-hom Let $F : \cC \to \cD$ be a functor admitting a [[right adjoint]] $U : \cD \to \cC$. Recall that every adjunction [induces] a -[monad] $UF$ (which we will call $T$ for short) on the category +[[monad]] $UF$ (which we will call $T$ for short) on the category $\cC$, and a "[comparison]" functor $K : \cD \to \cC^{T}$ into the [Eilenberg-Moore category] of $T$. In this module we will lay out a sufficient condition for the functor $K$ to have a left adjoint, which we call $K\inv$ (`Comparison-EM⁻¹`). Let us first establish a result about -the presentation of $T$-[algebras] by "generators and relations". +the presentation of $T$-[[algebras|monad algebra]] by "generators and relations". -[monad]: Cat.Diagram.Monad.html [induces]: Cat.Functor.Adjoint.Monad.html [comparison]: Cat.Functor.Adjoint.Monadic.html -[algebras]: Cat.Diagram.Monad.html#algebras-over-a-monad [Eilenberg-Moore category]: Cat.Diagram.Monad.html#eilenberg-moore-category Suppose that we are given a $T$-algebra $(A, \nu)$. Note that $(TA, \mu)$ is also a $T$-algebra, namely the free $T$-algebra on the object $A$. Let us illustrate this with a concrete example: Suppose we have the cyclic group $\bb{Z}/n\bb{Z}$, for some natural number $n$, which we -regard as a quotient group of $\bb{Z}$. The corresponding algebra $(TA, \mu)$ -would be the [free group] on $n$ generators -whence^[I was feeling pretentious when I wrote this sentence] we -conclude that, in general, this "free-on-underlying" $(TA, \mu)$ algebra -is very far from being the $(A, \nu)$ algebra we started with. - -[free group]: Algebra.Group.Free.html +regard as a quotient group of $\bb{Z}$. The corresponding algebra $(TA, +\mu)$ would be the [[free group]] on $n$ generators, whence we conclude +that, in general, this "free-on-underlying" $(TA, \mu)$ algebra is very +far from being the $(A, \nu)$ algebra we started with. Still, motivated by our $\bb{Z}/n\bb{Z}$ example, it feels like we -should be able to [quotient] the algebra $(TA, \mu)$ by some set of +should be able to [[quotient]] the algebra $(TA, \mu)$ by some set of _relations_ and get back the algebra $(A, \nu)$ we started with. This is absolutely true, and it's true even when the category of $T$-algebras is lacking in quotients! In particular, we have the following theorem: -[quotient]: Data.Set.Coequaliser.html#quotients - -**Theorem**. Every $T$-algebra $(A, \nu)$ is the [coequaliser] of the diagram - -[coequaliser]: Cat.Diagram.Coequaliser.html +**Theorem**. Every $T$-algebra $(A, \nu)$ is the [[coequaliser]] of the diagram ~~~{.quiver} \[\begin{tikzcd} diff --git a/src/Cat/Functor/Morphism.lagda.md b/src/Cat/Functor/Morphism.lagda.md index 391849849..17c96634e 100644 --- a/src/Cat/Functor/Morphism.lagda.md +++ b/src/Cat/Functor/Morphism.lagda.md @@ -39,14 +39,15 @@ private variable ``` --> -# Actions of functors on morphisms {defines="preserves-monos preserves-epis reflects-monos reflects-epis"} +# Actions of functors on morphisms This module describes how various classes of functors act on designated collections of morphisms. -First, some general definitions. Let $H$ be a collection of morphisms in $\cC$. -A functor $F : \cC \to \cD$ **preserves** $H$-morphisms if $f \in H$ implies -that $F(f) \in H$. +::: {.definition defines="preserves-monos preserves-epis"} +First, some general definitions. Let $H$ be a collection of morphisms in +$\cC$. A functor $F : \cC \to \cD$ **preserves** $H$-morphisms if $f \in +H$ implies that $F(f) \in H$. ```agda preserves-monos : Type _ @@ -57,6 +58,7 @@ preserves-epis : Type _ preserves-epis = ∀ {a b : 𝒞.Ob} {f : 𝒞.Hom a b} → 𝒞.is-epic f → 𝒟.is-epic (F₁ f) ``` +::: -Likewise, a functor $F : \cC \to \cD$ **reflects** $H$-morphisms -if $F(f) \in H$ implies that $f \in H$. +::: {.definition defines="reflects-monos reflects-epis"} +Likewise, a functor $F : \cC \to \cD$ **reflects** $H$-morphisms if +$F(f) \in H$ implies that $f \in H$. ```agda reflects-monos : Type _ @@ -78,6 +81,7 @@ reflects-epis : Type _ reflects-epis = ∀ {a b : 𝒞.Ob} {f : 𝒞.Hom a b} → 𝒟.is-epic (F₁ f) → 𝒞.is-epic f ``` +::: Functors that reflect invertible morphisms are called [[conservative]], and are notable enough to deserve their own name and page! diff --git a/src/Cat/Functor/Properties.lagda.md b/src/Cat/Functor/Properties.lagda.md index 3234239c9..b652eff53 100644 --- a/src/Cat/Functor/Properties.lagda.md +++ b/src/Cat/Functor/Properties.lagda.md @@ -180,22 +180,23 @@ the domain category to serve as an inverse for $f$: ## Essential fibres {defines="essential-fibre"} -The **essential fibre** of a functor $F : C \to D$ over an object $y : -D$ is the space of objects of $C$ which $F$ takes, up to isomorphism, to -$y$. +::: {.popup .keep} +The **essential fibre** of a [[functor]] $F : C \to D$ over an object $y +: D$ is the space of objects of $C$ which $F$ takes, up to +[[isomorphism]], to $y$. ```agda Essential-fibre : Functor C D → D .Ob → Type _ Essential-fibre {C = C} {D = D} F y = Σ[ x ∈ C ] (F · x ≅ y) where open import Cat.Morphism D ``` +::: :::{.definition #split-eso-functor alias="eso-functor essentially-surjective essential-surjection split-essential-surjection split-essentially-surjective"} A functor is **split essentially surjective** (abbreviated **split eso**) if there is a procedure for finding points in the essential fibre over any object. It's **essentially surjective** if this procedure -_merely_, i.e. truncatedly, finds a point: -::: +[[merely]] finds a point: ```agda is-split-eso : Functor C D → Type _ @@ -204,6 +205,7 @@ is-split-eso F = ∀ y → Essential-fibre F y is-eso : Functor C D → Type _ is-eso F = ∀ y → ∥ Essential-fibre F y ∥ ``` +::: Given a monoid $M$, we build a pointed, [[connected|connected category]] -precategory $\B{M}$, where the endomorphism monoid of the point recovers $M$. +precategory $\B{M}$, where the endomorphism monoid of the point recovers +$M$. ```agda module _ {ℓ} {M : Type ℓ} (mm : Monoid-on M) where diff --git a/src/Cat/Instances/Elements/Covariant.lagda.md b/src/Cat/Instances/Elements/Covariant.lagda.md index dba6b7253..38ff9b775 100644 --- a/src/Cat/Instances/Elements/Covariant.lagda.md +++ b/src/Cat/Instances/Elements/Covariant.lagda.md @@ -24,14 +24,15 @@ module _ {o ℓ s} {C : Precategory o ℓ} (P : Functor C (Sets s)) where # The covariant category of elements {defines="covariant-category-of-elements"} -While the [[category of elements]] comes up most often in the context of presheaves -(i.e., contravariant functors into $\Sets$), the construction makes sense for -covariant functors as well. +While the [[category of elements]] comes up most often in the context of +presheaves (i.e., contravariant functors into $\Sets$), the construction +makes sense for covariant functors as well. Sadly, we cannot simply reuse the contravariant construction, instantiating $\cC$ as $\cC\op$: the resulting category would be the -[[opposite|opposite category]] of what we want. Indeed, in both the covariant and -contravariant cases, we want the projection $\pi : \int F \to \cC$ to be covariant. +[[opposite|opposite category]] of what we want. Indeed, in both the +covariant and contravariant cases, we want the projection $\pi : \int F +\to \cC$ to be covariant. Thus we proceed to dualise the whole construction. diff --git a/src/Cat/Instances/Free.lagda.md b/src/Cat/Instances/Free.lagda.md index 80d470a3c..b913d9e89 100644 --- a/src/Cat/Instances/Free.lagda.md +++ b/src/Cat/Instances/Free.lagda.md @@ -255,14 +255,12 @@ module _ {o ℓ} (G : Graph o ℓ) where Path-category .assoc f g h = ++-assoc h g f ``` -Moreover, free categories are always _[gaunt]_: they are automatically +Moreover, free categories are always _[[gaunt]]_: they are automatically strict and, as can be seen with a bit of work, univalent. Univalence follows because any non-trivial isomorphism would have to arise as a `cons`{.Agda}, but `cons`{.Agda} can never be `nil`{.Agda} --- which would be required for a composition to equal the identity. -[gaunt]: Cat.Gaunt.html - While types prevent us from directly stating "if a map is invertible, it is `nil`{.Agda}", we can nevertheless pass around some equalities to make this induction acceptable. diff --git a/src/Cat/Instances/Monads.lagda.md b/src/Cat/Instances/Monads.lagda.md index 29f301225..e03a727c8 100644 --- a/src/Cat/Instances/Monads.lagda.md +++ b/src/Cat/Instances/Monads.lagda.md @@ -29,12 +29,14 @@ private variable # Categories of monads {defines="category-of-monads"} +::: {.popup} The **category of monads** of a category $\cC$ consists of [[monads]] -on $\cC$ and natural transformations preserving the monadic structure. +on $\cC$, and natural transformations preserving the monadic structure. In terms of the bicategory of [[monads in $\Cat$|monad in]], a morphism in the 1-categorical version always has the identity functor as the underlying 1-cell. That is, this 1-category of monads on $\cC$ is the fibre of the displayed bicategory of monads in $\Cat$ over $\cC$. +::: +## Epis {defines="epimorphism epic"} + +::: {.popup .keep} Conversely, a morphism is said to be **epic** when it is -right-cancellable. An **epimorphism** from $A$ to $B$, written $A \epi +right-cancellable. An **epimorphism** from $A$ to $B$, written $A \epi B$, is an epic morphism. -## Epis {defines="epimorphism epic"} - ```agda is-epic : Hom a b → Type _ is-epic {b = b} f = ∀ {c} → (g h : Hom b c) → g ∘ f ≡ h ∘ f → g ≡ h +``` +::: +```agda is-epic-is-prop : ∀ {a b} (f : Hom a b) → is-prop (is-epic f) is-epic-is-prop f x y i {c} g h p = Hom-set _ _ _ _ (x g h p) (y g h p) i @@ -464,11 +472,13 @@ split-epic→epic = rec! has-section→epic ## Isos {defines="isomorphism invertible"} +::: {.popup .keep} Maps $f : A \to B$ and $g : B \to A$ are **inverses** when we have $f \circ g$ and $g \circ f$ both equal to the identity. A map $f : A \to B$ **is invertible** (or **is an isomorphism**) when there exists a $g$ for which $f$ and $g$ are inverses. An **isomorphism** $A \cong B$ is a choice of map $A \to B$, together with a specified inverse. +::: ```agda record Inverses (f : Hom a b) (g : Hom b a) : Type h where diff --git a/src/Cat/Regular.lagda.md b/src/Cat/Regular.lagda.md index 4168cf7e1..0619418a6 100644 --- a/src/Cat/Regular.lagda.md +++ b/src/Cat/Regular.lagda.md @@ -21,15 +21,13 @@ module Cat.Regular where A **regular category** is a category with [[pullback]]-stable [[image factorisations]]. To define regular categories, we use the theory of -[orthogonal morphisms], specifically [strong epimorphisms]: A regular +[orthogonal morphisms], specifically [[strong epimorphisms]]: A regular category is one where every morphism factors as a strong epimorphism followed by a monomorphism, and strong epimorphisms are stable under pullback. -[image]: Cat.Diagram.Image.html [regular epi]: Cat.Diagram.Coequaliser.RegularEpi.html [orthogonal morphisms]: Cat.Morphism.Orthogonal.html -[strong epimorphisms]: Cat.Morphism.Strong.Epi.html At face value, it's a bit weird to take the definition of regular categories to talk about strong, rather than _regular_, epimorphisms. diff --git a/src/Cat/Skeletal.lagda.md b/src/Cat/Skeletal.lagda.md index 9cefb1d7c..593efcc90 100644 --- a/src/Cat/Skeletal.lagda.md +++ b/src/Cat/Skeletal.lagda.md @@ -59,9 +59,7 @@ module _ {o ℓ} (C : Precategory o ℓ) where --> One of the reasons skeletality is unnatural is it implies the category -is [strict]. - -[strict]: Cat.Strict.html +is [[strict|strict category]]. ```agda skeletal→strict : is-skeletal C → is-strict C @@ -71,7 +69,6 @@ is [strict]. Furthermore, skeletality does *not* imply univalence, as objects in $\cC$ may have non-trivial automorphisms. The [walking involution] is the simplest example of a non-univalent, skeletal precategory. In -general, we prefer to work with [gaunt], not skeletal, categories. +general, we prefer to work with [[gaunt]], not skeletal, categories. [walking involution]: Cat.Instances.Shape.Involution.html -[gaunt]: Cat.Gaunt.html diff --git a/src/Cat/Strict.lagda.md b/src/Cat/Strict.lagda.md index 172118594..f1d4a590d 100644 --- a/src/Cat/Strict.lagda.md +++ b/src/Cat/Strict.lagda.md @@ -10,26 +10,22 @@ module Cat.Strict where # Strict precategories {defines="strict-category strict-categories"} -We call a precategory **strict** if its type of objects is a `Set`{.Agda -ident=is-set}. +::: {.popup .keep} +We call a precategory $\cC$ **strict** if its type of objects is a [[set]]. ```agda is-strict : ∀ {o ℓ} → Precategory o ℓ → Type o is-strict C = is-set ⌞ C ⌟ ``` +::: Strictness is a very strong condition to impose on categories, since it classifies the "categories-as-algebras", or _petit_, view on categories, which regards categories _themselves_ as set-level structures, which -could be compared to [monoids] or [groups]. For example, the [path -category] on a directed graph is naturally regarded as strict. Moreover, +could be compared to [[monoids]] or [[groups]]. For example, the [[free +category]] on a directed [[graph]] is naturally regarded as strict. Moreover, [[strict categories form a precategory|category of strict categories]]. -[strcat]: Cat.Instances.StrictCat.html -[path category]: Cat.Instances.Free.html -[monoids]: Algebra.Monoid.html -[groups]: Algebra.Group.html - This is in contrast with the "categories-as-universes", or _gros_, view on categories. From this perspective, categories serve to organise objects at the set-level, like [$\thecat{Mon}$] or [$\Grp$]. These diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md index 3d6940b0b..5e1c27e31 100644 --- a/src/Data/Fin/Base.lagda.md +++ b/src/Data/Fin/Base.lagda.md @@ -24,6 +24,7 @@ module Data.Fin.Base where # Finite sets {defines=standard-finite-set} +::: {.popup .keep} The type $\operatorname{Fin}(n)$ is the type with exactly $n$ elements. We define it as a record type, packaging a natural number $k$ with a proof that $k \lt n$. @@ -35,6 +36,7 @@ record Fin (n : Nat) : Type where lower : Nat ⦃ bounded ⦄ : Irr (lower Nat.< n) ``` +::: While the type $k \lt n$ is a [[homotopy proposition|proposition]], we would like to enforce that constructions on $\operatorname{Fin}(n)$ diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md index 6fd10ef5b..97c0151ac 100644 --- a/src/Data/Fin/Finite.lagda.md +++ b/src/Data/Fin/Finite.lagda.md @@ -594,10 +594,14 @@ type is finite if it is merely listed. This is a proposition, and (because listed types satisfy choice) inherits all the closure properties above. +::: popup +A type $A$ is **finite** if it is [[merely]] [[listing]]. + ```agda Finite : Type ℓ → Type ℓ Finite A = ∥ Listing A ∥ ``` +::: ```agda instance diff --git a/src/Data/Int/Universal.lagda.md b/src/Data/Int/Universal.lagda.md index 969fde23a..543b82ef3 100644 --- a/src/Data/Int/Universal.lagda.md +++ b/src/Data/Int/Universal.lagda.md @@ -15,11 +15,19 @@ module Data.Int.Universal where # Universal property of the integers {defines="universal-property-of-the-integers"} -We define and prove a type-theoretic universal property of the integers, -which characterises them as the initial pointed set equipped with an -auto-equivalence, in much the same way that the natural numbers are -characterised as being the initial pointed type equipped with an -endomorphism. +::: popup +The **universal property of the [[integers]]** says that the type $\bZ$ +is the [[initial]] [[pointed]] type with an auto-[[equivalence]], in +that if $(X, *, e)$ is another such type, the space of maps $f : \bZ \to +X$ equipped with [[paths]] $p : f(0) = *$ and [[homotopies]] $f \circ +\operatorname{suc} = e \circ f$ is [[contractible]]. +::: + +We define and prove a type-theoretic universal property of the +[[integers]], which characterises them as the [[initial]] [[pointed]] +[[set]] equipped with an auto-[[equivalence]], in much the same way that +the natural numbers are characterised as being the initial pointed type +equipped with an endomorphism. ```agda record Integers (ℤ : Type) : Typeω where diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md index ab36dcbca..19aefbc87 100644 --- a/src/Data/Set/Coequaliser.lagda.md +++ b/src/Data/Set/Coequaliser.lagda.md @@ -260,6 +260,20 @@ of the possible related elements in $A$. By coequalising these projections, we obtain a space where any related objects are identified: the **quotient** $A/R$. +::: popup +The ([[set]]) **quotient** of a type $A$ by a relation $R$ is the type +$A/R$ equipped with a constructor `inc`{.Agda} and a generating path +`quot`{.Agda} sending $R(x, y)$ to $\operatorname{inc} x = +\operatorname{inc} y$, in the sense that if $f : A \to B$ is a function +into a set $B$ which "respects $R$" in that we have +$$ \forall\ a\ b,\ R(a, b) \to f(a) = f(b) $$, then there is a unique +$f' : A/R \to B$ satisfying $f'(\operatorname{inc} x) = f(x)$. + +It can be constructed as the [[set coequaliser]] of the two projections +onto $A$ from the total space $\Sigma_{(a, b) : A \times A} R(a, b)$ of +$R$. +::: + ```agda private tot : ∀ {ℓ} → (A → A → Type ℓ) → Type (level-of A ⊔ ℓ) diff --git a/src/Data/Set/Projective.lagda.md b/src/Data/Set/Projective.lagda.md index 28e1fdfc0..4e2fa0d74 100644 --- a/src/Data/Set/Projective.lagda.md +++ b/src/Data/Set/Projective.lagda.md @@ -27,9 +27,8 @@ private variable --> :::{.definition #set-projective} -A type $A$ is **set-projective** if we can commute [[propositional truncation]] -past $A$-indexed families. -::: +A type $A$ is **set-projective** if we can commute [[propositional +truncation]] past the product of an $A$-indexed family of [[sets]]. ```agda is-set-projective : ∀ {ℓ} (A : Type ℓ) → (κ : Level) → Type _ @@ -39,12 +38,12 @@ is-set-projective A κ = → (∀ a → ∥ P a ∥) → ∥ (∀ a → P a) ∥ ``` +::: Intuitively, a type $A$ is set-projective if it validates a sort of -$A$-indexed version of the [[axiom of choice]]. - -If $A$ is a set, then $A$ is set-projective if and only if every -surjection $E \to A$ from a set $E$ splits. +$A$-indexed version of the [[axiom of choice]]. If $A$ is a set, then +$A$ is set-projective if and only if every surjection $E \to A$ from a +set $E$ splits. ```agda surjections-split→set-projective diff --git a/src/Data/Set/Truncation.lagda.md b/src/Data/Set/Truncation.lagda.md index 94d0e539a..26d6fe6f3 100644 --- a/src/Data/Set/Truncation.lagda.md +++ b/src/Data/Set/Truncation.lagda.md @@ -115,6 +115,16 @@ using `is-set→squarep`{.Agda}. i j ``` +:::{.popup .summary} +The **set truncation** $\| A \|_0$ of a type $A$ is the universal +[[set]] equipped with a map `inc`{.Agda} mapping $A \to \| A \|$. + +Its elimination principle says that if $P(-)$ is a family of sets over +$\| A \|_0$, then any function $f : (a : A) \to P(\operatorname{inc} a)$ +can be extended to a section $f' : (a : \| A \|_0) \to P(a)$ satisfying +$f'(\operatorname{inc} a) = f(a)$. +::: + # Paths in the set truncation ```agda diff --git a/src/Homotopy/Conjugation.lagda.md b/src/Homotopy/Conjugation.lagda.md index 98e73c357..69b7982cb 100644 --- a/src/Homotopy/Conjugation.lagda.md +++ b/src/Homotopy/Conjugation.lagda.md @@ -29,6 +29,11 @@ usual way. However, since we know ahead-of-time what transport in a type of paths computes to, we can take a short-cut and define the equivalence directly: it is given by **conjugation** with $p$. +::: popup +The **conjugation** of a [[path]] $q : y \is y$ by a path $p : y \is x$ +is the composite $p\inv \dcomp q \dcomp p$. +::: + ```agda opaque conj : ∀ {ℓ} {A : Type ℓ} {x y : A} → y ≡ x → y ≡ y → x ≡ x diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md index 72fbc2a99..f0b36271a 100644 --- a/src/Homotopy/Connectedness.lagda.md +++ b/src/Homotopy/Connectedness.lagda.md @@ -25,8 +25,10 @@ private variable # Connectedness {defines="connected connectedness connectivity simply-connected"} +::: {.popup .keep} We say that a type is **$n$-connected** if its $n$-[[truncation]] is [[contractible]]. +::: While being $n$-[[truncated]] expresses that all homotopy groups above $n$ are trivial, being $n$-connected means that all homotopy groups @@ -56,8 +58,10 @@ is-n-connected-is-prop 2 = is-contr-is-prop is-n-connected-is-prop (suc (suc (suc n))) = is-contr-is-prop ``` +::: {.popup .keep} For short, we say that a type is **connected** if it is $0$-connected, and **simply connected** if it is $1$-connected: +::: ```agda is-connected : ∀ {ℓ} → Type ℓ → Type _ diff --git a/src/Homotopy/Space/Circle.lagda.md b/src/Homotopy/Space/Circle.lagda.md index 5d2c99c6a..e5f4c294d 100644 --- a/src/Homotopy/Space/Circle.lagda.md +++ b/src/Homotopy/Space/Circle.lagda.md @@ -25,8 +25,12 @@ module Homotopy.Space.Circle where The first example of nontrivial space one typically encounters when studying synthetic homotopy theory is the circle: it is, in a sense, the perfect space to start with, having exactly one nontrivial path space, -which is a [[free group|free group construction]], and the simplest -nontrivial [[free group|free group construction]] at that: the integers. +which is a [[free group]], and the simplest nontrivial [[free group]] at +that: the integers. + +::: popup +The **circle** is the [[pointed]], [[connected]] higher inductive type +with a basepoint and a single generating loop. ```agda data S¹ : Type where @@ -37,6 +41,8 @@ S¹∙ : Type∙ lzero S¹∙ = S¹ , base ``` +::: + Diagrammatically, we can picture the circle as being the $\infty$-groupoid generated by the following diagram: @@ -113,6 +119,16 @@ always-loop = S¹-elim loop (double-connection loop loop) ## Fundamental group {defines="loop-space-of-the-circle"} +::: popup +The [[loop space]] of the [[circle]] $S^1$ at the basepoint +`base`{.Agda} is the type of [[integers]] $\bZ$, with path composition +taken to addition. + +Additionally, this can be shown for any $\bZ$ which satisfies the +[[universal property of the integers]] as the [[initial]] [[pointed]] +type with an auto-[[equivalence]]. +::: + We now calculate the loop space of the circle, relative to an _arbitrary_ implementation of the integers: any type that satisfies their type-theoretic universal property. We call this a _HoTT take_: the diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md index 733fc579a..a73be0dc8 100644 --- a/src/Homotopy/Space/Delooping.lagda.md +++ b/src/Homotopy/Space/Delooping.lagda.md @@ -30,6 +30,17 @@ annoying way that questions like these tend to be answered: Given any group $G$, we construct a type $\B{G}$ with $\pi_1(\B{G}) \equiv G$. We call $\B{G}$ the **delooping** of $G$. +::: popup +The **delooping** of a [[group]] $G$ is the [[groupoid]] $\B{G}$ with +[[fundamental group]] $\pi_1(\B{G}) = G$. As it is [[pointed]] and +[[connected]], $\B{G}$ is a [[concrete group]]. + +It can be constructed as the 1-truncated higher inductive type +`Deloop`{.Agda} with a generating `path`{.Agda} for each $x : G$, and a +square connecting $\operatorname{path}(xy) = \operatorname{path}(x) +\cdot \operatorname{path}(y)$. +::: + " `Text.isInfixOf` txt || "–>" `Text.isInfixOf` txt - = fail $ "[WARN] " ++ file ++ " contains misplaced " -checkMarkup _ _ = pure () diff --git a/support/shake/app/HTML/Render.hs b/support/shake/app/HTML/Render.hs index 54cd1dacf..932eb900d 100644 --- a/support/shake/app/HTML/Render.hs +++ b/support/shake/app/HTML/Render.hs @@ -15,12 +15,13 @@ import Agda.Utils.Function import Control.DeepSeq import Control.Monad -import qualified Data.HashMap.Strict as Hm +import qualified Data.IntMap.Strict as IntMap import qualified Data.Text.Lazy as Tl import qualified Data.Text as Text -import Data.HashMap.Strict (HashMap) +import Data.IntMap.Strict (IntMap) import Data.Foldable import Data.Hashable +import Data.Binary (Binary) import Data.Aeson import Data.Maybe import Data.Text (Text) @@ -66,7 +67,7 @@ renderToHtml = finish . Ppr.fullRenderAnn Ppr.PageMode 100 1.5 cont [] where toBlaze (Mark _) = __IMPOSSIBLE__ toBlaze (Text t) = Html.text t toBlaze (Node a t) = Html.span do - aspectsToHtml Nothing mempty Nothing a $ + aspectsToHtml mempty Nothing Nothing a $ traverse_ toBlaze t unless (null (note a)) do Html.span (string (note a)) !! [Attr.class_ "Note"] @@ -81,7 +82,13 @@ data Identifier = Identifier , idType :: Text , idTooltip :: Text } - deriving (Eq, Show, Ord, Generic, ToJSON, FromJSON, NFData) + deriving (Eq, Show, Ord, Generic, ToJSON, FromJSON, NFData, Binary) + +data HtmlModule = HtmlModule + { htmlModIdentifiers :: IntMap Identifier + , htmlModImports :: [String] + } + deriving (Show, Generic, NFData, Binary) instance Hashable Identifier where hashWithSalt s = hashWithSalt s . idAnchor @@ -98,8 +105,9 @@ modToFile m ext = Network.URI.Encode.encode $ render (pretty m) <.> ext -- We put a fail safe numeric anchor (file position) for internal references -- (issue #2756), as well as a heuristic name anchor for external references -- (issue #2604). -aspectsToHtml :: Maybe TopLevelModuleName -> HashMap Text.Text (Int, Identifier) -> Maybe Int -> Aspects -> Html -> Html -aspectsToHtml ourmod types pos mi = +aspectsToHtml + :: IntMap Identifier -> Maybe TopLevelModuleName -> Maybe Int -> Aspects -> Html -> Html +aspectsToHtml locals ourmod pos mi = applyWhen hereAnchor (anchorage nameAttributes mempty <>) . anchorage posAttributes where -- Warp an anchor ( tag) with the given attributes around some HTML. @@ -154,15 +162,10 @@ aspectsToHtml ourmod types pos mi = link :: DefinitionSite -> [Html.Attribute] link ds@(DefinitionSite m defPos _here _aName) = - let - anchor :: String - anchor = definitionSiteToAnchor ds - - ident_ :: Maybe Int - ident_ = fst <$> Hm.lookup (Text.pack anchor) types - in [ Attr.href $ stringValue $ anchor ] - ++ maybeToList (Html.dataAttribute "module" . stringValue . show . pretty <$> ourmod) - ++ maybeToList (Html.dataAttribute "identifier" . stringValue . show <$> ident_) + (Attr.href $ stringValue $ definitionSiteToAnchor ds):do + guard $ Just m /= ourmod || defPos `IntMap.member` locals + pure $ Html.dataAttribute "type" $ stringValue "true" + definitionSiteToAnchor :: DefinitionSite -> String definitionSiteToAnchor (DefinitionSite m defPos _ _) = diff --git a/support/shake/app/Main.hs b/support/shake/app/Main.hs index 071ce0084..7c0ed5679 100755 --- a/support/shake/app/Main.hs +++ b/support/shake/app/Main.hs @@ -5,9 +5,11 @@ import Control.Concurrent.STM import Control.Monad.IO.Class import Control.Monad.Writer import Control.Exception +import Control.DeepSeq import Control.Monad import qualified Data.Map.Strict as Map +import qualified Data.Text as Text import qualified Data.Set as Set import Data.Aeson hiding (Options, defaultOptions) import Data.Bifunctor @@ -27,21 +29,25 @@ import System.Time.Extra import System.Process import System.Exit -import Shake.Options +import Shake.Markdown.Reader import Shake.AgdaCompile import Shake.SearchData import Shake.LinkGraph import Shake.Markdown import Shake.Modules +import Shake.Options import Shake.Diagram import Shake.Digest import Shake.KaTeX -import Shake.Git import Shake.Utils +import Shake.Git + +import Text.DocTemplates (ToContext(toVal), Context(..)) import Definitions import Timer import Shake.Recent (recentAdditions) +import Text.Show.Pretty (ppShow) {- Welcome to the Horror That Is 1Lab's Build Script. @@ -50,13 +56,17 @@ import Shake.Recent (recentAdditions) -} rules :: Rules () rules = do + moduleRules + + reader <- markdownReader + glossaryRules reader + diagramRules reader + agdaRules digestRules gitRules katexRules - moduleRules linksRules - glossaryRules {- Write @_build/all-pages.agda@. This imports every module in the source tree @@ -74,6 +84,16 @@ rules = do writeFileLines out $ ["open import " ++ toOut x | x <- modules] + digest <- newCache \() -> do + cssDigest <- Text.pack <$> getFileDigest "_build/html/css/default.css" + startJsDigest <- Text.pack <$> getFileDigest "_build/html/start.js" + mainJsDigest <- Text.pack <$> getFileDigest "_build/html/main.js" + rnf (cssDigest, startJsDigest, mainJsDigest) `seq` pure . Context . Map.fromList $ + [ ("css", toVal cssDigest) + , ("start-js", toVal startJsDigest) + , ("main-js", toVal mainJsDigest) + ] + {- For each 1Lab module, read the emitted file from @_build/html0@. If it's HTML, we just copy it to @_build/html@. Otherwise we compile the markdown @@ -98,18 +118,12 @@ rules = do _ -> if skipAgda then "agda" else "html" case modKind of - Just WithText -> buildMarkdown modName (input <.> inext) out + Just WithText -> buildMarkdown (digest ()) reader modName (input <.> inext) out _ -> copyFile' (input <.> inext) out -- Wrong, but eh! unless skipAgda $ need ["_build/html/types" modName <.> "json"] "_build/search/*.json" %> \out -> need ["_build/html" takeFileName out -<.> "html"] - "_build/html/types/*.json" %> \out -> do - let - mn = takeFileName out - it = "_build/html0/" mn -<.> "used" - need [it] - copyFile' it $ "_build/html/types/" mn "_build/html/static/search.json" %> \out -> do skipAgda <- getSkipAgda @@ -117,22 +131,7 @@ rules = do let searchFiles = (if skipAgda then [] else ["_build/all-types.json"]) ++ map (\(x, _) -> "_build/search" x <.> "json") modules searchData :: [[SearchTerm]] <- traverse readJSONFile searchFiles - traced "Writing search data" $ encodeFile out (concat searchData) - - -- Compile Quiver to SVG. This is used by 'buildMarkdown'. - "_build/html/**/*.light.svg" %> \out -> do - let - inp = "_build/diagrams" - takeFileName (takeDirectory out) - takeBaseName out -<.> "tex" - buildDiagram (getPreambleFor False) inp out False - - "_build/html/**/*.dark.svg" %> \out -> do - let - inp = "_build/diagrams" - takeFileName (takeDirectory out) - takeBaseName out -<.> "tex" - buildDiagram (getPreambleFor True) inp out True + traced "writing search data" $ encodeFile out (concat searchData) "_build/html/css/*.css" %> \out -> do let inp = "support/web/css/" takeFileName out -<.> "scss" @@ -177,7 +176,7 @@ rules = do static <- getDirectoryFiles "support/static/" ["**/*"] >>= \files -> pure ["_build/html/static" f | f <- files] need $ - static ++ agda ++ + agda ++ static ++ [ "_build/html/favicon.ico" , "_build/html/static/links.json" , "_build/html/static/search.json" @@ -191,7 +190,7 @@ rules = do -- ??? phony "clean" do - removeFilesAfter "_build" ["html0/*", "html/*", "diagrams/*", "*.agda", "*.md", "*.html"] + removeFilesAfter "_build" ["**/*.bin", "**/*.json", "html0/*", "html/*", "diagrams/*", "*.agda", "*.md", "*.html"] phony "really-clean" do need ["clean"] diff --git a/support/shake/app/Shake/AgdaCompile.hs b/support/shake/app/Shake/AgdaCompile.hs index 786fbada1..9f0cc0aad 100644 --- a/support/shake/app/Shake/AgdaCompile.hs +++ b/support/shake/app/Shake/AgdaCompile.hs @@ -8,20 +8,25 @@ import System.FilePath import Control.Monad.Except import Control.Monad -import qualified Data.List.NonEmpty as List1 import qualified Data.HashMap.Strict as Hm +import qualified Data.IntMap.Strict as IntMap +import qualified Data.List.NonEmpty as List1 import qualified Agda.Utils.BiMap as BiMap -import qualified Data.Map as Map import qualified Data.Text as T -import Data.Aeson (eitherDecodeFileStrict', encodeFile) +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.IntMap.Strict (IntMap) import Data.Maybe (fromMaybe) import Data.Foldable import Data.IORef +import qualified Data.Binary as Binary +import qualified Data.Aeson as Aeson + import Development.Shake.Classes import Development.Shake -import Shake.Options (getSkipTypes, getWatching) +import Shake.Options (getSkipTypes, getWatching, getBaseUrl) import Agda.Compiler.Backend hiding (getEnv) import Agda.Interaction.FindFile (SourceFile(..)) @@ -39,14 +44,21 @@ import Agda.Syntax.TopLevelModuleName , hashRawTopLevelModuleName ) import Agda.Syntax.Position (noRange) + import qualified Agda.Utils.Maybe.Strict as S import qualified Agda.Utils.Trie as Trie +import Agda.Utils.Impossible import Agda.Utils.FileName import Agda.Utils.Hash (Hash) -import Agda.Utils.Lens ((^.)) +import Agda.Utils.Lens ((^.), (<&>)) + +import GHC.Compact + +import Shake.Modules (getOurModules) import HTML.Backend import HTML.Base +import Debug.Trace (traceMarkerIO) ------------------------------------------------------------------------ -- Oracles @@ -104,32 +116,55 @@ agdaRules = do let hash = iFullHash . getInterface state $ toTopLevel state m pure (CompileA state hash) - -- Create a cache for the per-module type information. - getTypes <- newCache \modName -> do - let path = "_build/html0" modName <.> ".json" - need [path] - - result :: Either String (Hm.HashMap T.Text Identifier) <- - quietly . traced "read types" $ eitherDecodeFileStrict' path - either fail pure result - - -- In order to write the JSON, we first compile the required module (which - -- gives us the TC environment) and then emit the HTML/Markdown and type JSON. - "_build/html0/*.json" %> \file -> do + -- In order to write the types, we first compile the required module + -- (which gives us the TC environment) and then emit the HTML/Markdown + -- and type JSON. + "_build/html0/*.bin" %> \file -> do let modName = T.pack . dropExtension $ takeFileName file compileResult <- askOracle (ModuleCompileQ modName) - emitAgda compileResult getTypes modName + emitAgda compileResult modName -- Add a couple of forwarding rules for emitting the actual HTML/MD - "_build/html0/*.html" %> \file -> need [file -<.> "json"] - "_build/html0/*.used" %> \file -> need [file -<.> "json"] - "_build/html0/*.md" %> \file -> need [file -<.> "json"] + "_build/html0/*.html" %> \file -> need [file -<.> "bin"] + "_build/html0/*.md" %> \file -> need [file -<.> "bin"] - -- We generate the all-types JSON from the all-pages types JSON - it's just a - -- schema change. + let + decodeModule mn = do + let it = "_build/html0/" mn <.> "bin" + need [it] + liftIO do + inp :: Either a HtmlModule <- Binary.decodeFileOrFail it + out <- either (fail . show) pure inp + rnf out `seq` pure out + + "_build/html/types/*.json" %> \out -> do + let mn = dropExtension (takeFileName out) + mod <- decodeModule mn + liftIO do + Aeson.encodeFile ("_build/html/types/" mn <.> "json") $ Map.fromDistinctAscList + [ (k, idTooltip id) | (k, id) <- IntMap.toAscList (htmlModIdentifiers mod) ] + + -- Generating the all-types JSON requires chasing the import tree + -- reported in the all-pages 'HtmlModule'. "_build/all-types.json" %> \file -> do - types <- getTypes "all-pages" - liftIO $ encodeFile file $ map (\t -> t{idTooltip = ""}) (Hm.elems types) + mods <- getOurModules + need [ "_build/html0" mod <.> "bin" | mod <- Map.keys mods ] + + mod <- decodeModule "all-pages" + + let + visit !seen !out (other:mods) | other `Set.member` seen = visit seen out mods + visit !seen !out (other:mods) = do + HtmlModule{htmlModIdentifiers = ids, htmlModImports = imps} <- decodeModule other + let elts = IntMap.elems ids <&> \t -> t{ idTooltip = "" } + visit + (Set.insert other seen) + (foldr Set.insert out elts) + (mods ++ imps) + visit !seen !out [] = pure out + + idents <- Set.toList <$> visit mempty mempty (htmlModImports mod) + liftIO $ Aeson.encodeFile file idents -- | Compile the top-level Agda file. compileAgda :: IORef (Maybe TCState) -> Action CompileA @@ -151,6 +186,7 @@ compileAgda stateVar = do Nothing -> (["_build/all-pages.agda"],) <$> initStateIO Just state -> pure (if watching then changed else ["_build/all-pages.agda"], state) + traceMarkerIO "agda starts" ((), state) <- runTCMPrettyErrors initEnv state do -- We preserve the old modules and restore them at the end, as otherwise -- we forget them, and will fail if we need to rebuild other HTML pages. @@ -170,34 +206,30 @@ compileAgda stateVar = do modifyTCLens stVisitedModules (`Map.union` oldVisited) writeIORef stateVar (Just state) + traceMarkerIO "agda ends" -- TODO: Catch errors and pretty-print failures pure (CompileA state 0) - -- | Emit an Agda file as HTML or Markdown. -emitAgda - :: CompileA - -> (String -> Action (Hm.HashMap T.Text Identifier)) - -> T.Text -> Action () -emitAgda (CompileA tcState _) getTypes modName = do +emitAgda :: CompileA -> T.Text -> Action () +emitAgda (CompileA tcState _) modName = do basepn <- filePath <$> liftIO (absolute "src/") + baseUrl <- getBaseUrl + skipTypes <- getSkipTypes + let tlModName = toTopLevel tcState modName iface = getInterface tcState tlModName + opts = (defaultHtmlOptions baseUrl) { htmlOptGenTypes = not skipTypes } - types <- parallel . map (getTypes . render . pretty . fst) $ iImportedModules iface - - skipTypes <- getSkipTypes - ((), _) <- quietly . traced "agda html" + ((), _) <- traced "generating html" . runTCM initEnv tcState . withScope_ (iInsideScope iface) . locallyTC eActiveBackendName (const $ Just "HTML") $ do - compileOneModule basepn defaultHtmlOptions { htmlOptGenTypes = not skipTypes } - (mconcat types) - iface + compileOneModule basepn opts iface pure () diff --git a/support/shake/app/Shake/Diagram.hs b/support/shake/app/Shake/Diagram.hs index 2ef6ad10e..2b5f26b89 100644 --- a/support/shake/app/Shake/Diagram.hs +++ b/support/shake/app/Shake/Diagram.hs @@ -1,17 +1,27 @@ -{-# LANGUAGE TemplateHaskellQuotes, OverloadedStrings, ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskellQuotes, OverloadedStrings, ScopedTypeVariables, BlockArguments, LambdaCase #-} -module Shake.Diagram (buildDiagram, diagramHeight) where +module Shake.Diagram (diagramRules, diagramHeight) where + +import Control.Monad import qualified Data.Text.IO as Text import qualified Data.Text as Text import Data.ByteString.Lazy (ByteString) import Data.Text (Text) +import Text.Pandoc.Definition import Text.HTML.TagSoup +import Text.Pandoc.Walk import Development.Shake.FilePath import Development.Shake +import Shake.Modules (markdownSource) +import Shake.Digest +import Shake.KaTeX (getPreambleFor) + +import qualified System.Directory as Dir + -- | Render a LaTeX diagram to SVG. This renders the diagram using the -- @support/diagram.tex@ template, and then uses pdflatex and pdftocairo -- to convert it to SVG. @@ -72,3 +82,45 @@ maybeDarken True = Text.unlines . map mkdark . Text.lines where templatePath :: FilePath templatePath = "support/diagram.tex" + +diagramRules :: (FilePath -> Action Pandoc) -> Rules () +diagramRules reader = do + -- Compile Quiver to SVG. This is used by 'buildMarkdown'. + "_build/html/**/*.light.svg" %> \out -> do + let + inp = "_build/diagrams" + takeFileName (takeDirectory out) + takeBaseName out -<.> "tex" + need [inp] + buildDiagram (getPreambleFor False) inp out False + + "_build/html/**/*.dark.svg" %> \out -> do + let + inp = "_build/diagrams" + takeFileName (takeDirectory out) + takeBaseName out -<.> "tex" + need [inp] + buildDiagram (getPreambleFor True) inp out True + + -- Extract the diagram with the given digest from the module source + -- file; even if the module uses many diagrams, only one will be written. + -- + -- It's faster to traverse the markdown many times looking for each of + -- the needed diagrams than it is to lock the folder associated with + -- the module (since we process blocks in parallel when rendering a + -- file). + "_build/diagrams/*/*.tex" %> \out -> do + let + mod = takeFileName (takeDirectory out) + want = dropExtensions (takeFileName out) + + md <- markdownSource mod + need [ md ] + + liftIO $ Dir.createDirectoryIfMissing True $ "_build/diagrams" mod + + reader md >>= query \case + (CodeBlock (_, classes, _) contents) | "quiver" `elem` classes -> do + when (shortDigest contents == want) . liftIO $ + Text.writeFile ("_build/diagrams" mod want <.> "tex") contents + _ -> mempty diff --git a/support/shake/app/Shake/Highlights.hs b/support/shake/app/Shake/Highlights.hs index 71ab86302..95a394f55 100644 --- a/support/shake/app/Shake/Highlights.hs +++ b/support/shake/app/Shake/Highlights.hs @@ -25,8 +25,8 @@ import Debug.Trace -- icon under @support/web/highlights@ is supported; the @definition@ -- icon will additionally include the principal label being defined (the -- id of the element) in the text. -renderHighlights :: [Tag Text] -> Action [Tag Text] -renderHighlights stream = do +renderHighlights :: FilePath -> [Tag Text] -> Action [Tag Text] +renderHighlights input stream = do let tree = tagTree stream icons <- fmap (Text.pack . map toLower . dropExtension) diff --git a/support/shake/app/Shake/LinkReferences.hs b/support/shake/app/Shake/LinkReferences.hs index e53c15221..2caf83f38 100644 --- a/support/shake/app/Shake/LinkReferences.hs +++ b/support/shake/app/Shake/LinkReferences.hs @@ -42,14 +42,10 @@ linkReferences modname (Pandoc meta blocks) = Pandoc meta (walk link blocks) link x = x renderReference :: Reference -> Text -> Inline -renderReference (Reference href cls ty) t = - Span ("", ["Agda"], []) [Link ("", [cls], maybeToList (("data-identifier",) <$> ty)) [Code nullAttr t] (href, "")] +renderReference (Reference href cls) t = + Span ("", ["Agda"], []) [Link ("", [cls], [("data-type", "true")]) [Code nullAttr t] (href, "")] -data Reference = - Reference { refHref :: Text - , refClass :: Text - , refType :: Maybe Text - } +data Reference = Reference { refHref :: Text , refClass :: Text } deriving (Eq, Show) -- | Find all links in Agda code blocks (represented as HTML not @@ -66,7 +62,7 @@ parseSymbolRefs = go mempty . concatMap getHTML where go map (TagOpen "a" meta:TagText t:TagClose "a":xs) | Just cls <- lookup "class" meta , Just href <- lookup "href" meta - = go (addIfNotPresent t (Reference href cls (lookup "data-identifier" meta)) map) xs + = go (addIfNotPresent t (Reference href cls) map) xs | otherwise = go map xs diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs index a5c65e6f4..ab550ab5d 100644 --- a/support/shake/app/Shake/Markdown.hs +++ b/support/shake/app/Shake/Markdown.hs @@ -5,13 +5,15 @@ post-processing steps and rendered to HTML using the @support/web/template.html@ template. -} -module Shake.Markdown (buildMarkdown, readLabMarkdown) where +module Shake.Markdown (buildMarkdown) where import Control.Monad.Error.Class import Control.Monad.IO.Class import Control.Monad.Writer import Control.Monad.State import Control.Applicative +import Control.Exception +import Control.DeepSeq import Control.Monad import qualified Data.ByteString.Lazy as LazyBS @@ -35,12 +37,15 @@ import qualified System.Directory as Dir import Development.Shake.FilePath import Development.Shake +import GHC.Generics (Generic) + import qualified Citeproc as Cite import Text.DocTemplates import Text.HTML.TagSoup import Text.HTML.TagSoup.Match import Text.HTML.TagSoup.Tree +import qualified Text.DocLayout as Doclayout import Text.Pandoc.Builder (Inlines) import Text.Pandoc.Citeproc import Text.Pandoc.Shared @@ -48,6 +53,7 @@ import Text.Collate.Lang (Lang (..)) import Text.Pandoc.Walk import Text.Pandoc +import Shake.Markdown.Reader import Shake.LinkReferences import Shake.SearchData import Shake.Highlights @@ -58,153 +64,29 @@ import Shake.Digest import Shake.KaTeX import Shake.Git -import HTML.Emit - import Definitions -import System.IO.Unsafe import Text.Show.Pretty (ppShow) - -labReaderOptions :: ReaderOptions -labReaderOptions = - let - good = [ Ext_wikilinks_title_before_pipe ] - bad = [Ext_definition_lists, Ext_compact_definition_lists] - exts = foldr disableExtension - (foldr enableExtension (getDefaultExtensions "markdown") good) - bad - in def { readerExtensions = exts } - -readLabMarkdown :: MonadIO m => FilePath -> m Pandoc -readLabMarkdown fp = liftIO cont where - - unParaMath :: Block -> Block - unParaMath (Para [Math DisplayMath m]) = Plain [Math DisplayMath m] - unParaMath x = x - - cont :: IO Pandoc - cont = do - contents <- mangleMarkdown <$> Text.readFile fp - either (fail . show) pure =<< runIO do - doc <- readMarkdown labReaderOptions [(fp, contents)] - pure $ walk unParaMath $ walk postParseInlines doc - --- | Patch a sequence of inline elements. `patchInline' should be preferred --- where possible, this is only useful when you cannot modify inlines in --- isolation. -postParseInlines :: [Inline] -> [Inline] - --- Float text that occurs directly after a mathematics span *inside* the --- span. This allows the entire expression to reflow but preserves the --- intended semantics of having e.g. `$n$-connected` be a single logical --- unit (which should be line-wrapped together). --- --- The text is attached naïvely, so if the entire expression is a single --- group (i.e. something like `${foo}$`), it will probably not work. --- However, the naïve solution does have the benefit of automatically --- attaching the non-wrapping text to the last "horizontal unit" in the --- span. --- --- However, note that the glue between the original mathematics and the --- attached text is treated as an opening delimiter. This is to have --- correct spacing in case the maths ends with an operatorname, e.g. id. -postParseInlines (Math ty mtext:s@(Str txt):xs) - | not (Text.isPrefixOf " " txt) - = - let - glue = "\\mathopen{\\nobreak}\\textnormal{" <> txt <> "}" - mtext' = Text.stripEnd mtext <> glue - in postParseInlines (Math ty mtext':xs) - --- Parse the contents of wikilinks as markdown. While Pandoc doesn't --- read the title part of a wikilink, it will always consist of a single --- Str span. We call the Pandoc parser in a pure context to read the --- title part as an actual list of inlines. -postParseInlines (Link attr [Str contents] (url, "wikilink"):xs) = - link' `seq` link':postParseInlines xs where - - try = either (const Nothing) Just . runPure - fail = error $ - "Failed to parse contents of wikilink as Markdown:" <> Text.unpack contents - - link' = fromMaybe fail do - -- The contents of a link are valid if they consist of a single list - -- of inlines. Pandoc doesn't let us parse a list of inlines, but we - -- can still parse it as a document and ensure that (a) everything - -- got bunched in the same paragraph and (b) there was no metadata. - parsed@(Pandoc (Meta m) [Para is]) <- try (readMarkdown labReaderOptions contents) - guard (null m) -- I don't foresee this ever failing. - - -- Rendering the contents as plain text will strip all the - -- decorations, thus recovering the "underlying page" that was meant - -- to be linked to. Of course, we should only try changing the - -- target if the link looks like [[foo]], rather than [[foo|bar]]. - let - target = if url == contents - then stringify parsed - else url - - -- Note that Pandoc doesn't distinguish between [[foo]] and - -- [[foo|foo]], so really the only way is checking whether the URL - -- is equal to the contents string. If that was the case, then - -- stripping formatting is the right thing, otherwise e.g. [[*path - -- induction*]] would fail since the target "*path-induction*" - -- doesn't exist. - pure (Link attr is (target, "wikilink")) - -postParseInlines (x:xs) = x:postParseInlines xs -postParseInlines [] = [] - --- | Pandoc's wiki-link extension does not support splitting the guts of --- a wikilink over multiple lines. The function 'mangleMarkdown' --- pre-processes the input file so that any invalid space characters --- inside a wikilink are replaced by the safe ASCII space @ @. -mangleMarkdown :: Text -> Text -mangleMarkdown = Text.pack . toplevel . Text.unpack where - toplevel ('[':'[':cs) = '[':'[':wikilink toplevel cs - toplevel ('<':'!':'-':'-':cs) = startcomment cs - toplevel (c:cs) = c:toplevel cs - toplevel [] = [] - - startcomment ('[':'T':'O':'D':'O':cs) = comment False 1 cs - startcomment (c:cs) - | isSpace c = startcomment cs - | otherwise = "
\n" ++ comment True 1 (c:cs) - startcomment [] = error "Unterminated comment" - - comment e 0 cs = concat ["\n
" | e] ++ toplevel cs - comment e n [] = error "Unterminated comment" - - comment e n ('-':'-':'>':cs) = comment e (n - 1) cs - comment e n ('<':'!':'-':'-':cs) = comment e (n + 1) cs - - comment True n ('[':'[':cs) = '[':'[':wikilink (comment True n) cs - comment e n (c:cs) - | e = c:comment e n cs - | otherwise = comment e n cs - - wikilink k (']':']':cs) = ']':']':k cs - - wikilink k ('\n':cs) = ' ':wikilink k cs - wikilink k ('\t':cs) = ' ':wikilink k cs - wikilink k ('\f':cs) = ' ':wikilink k cs - wikilink k ('\r':cs) = ' ':wikilink k cs - - wikilink k (c:cs) = c:wikilink k cs - wikilink k [] = [] - -buildMarkdown :: String -- ^ The name of the Agda module. - -> FilePath -- ^ Input markdown file, produced by the Agda compiler. - -> FilePath -- ^ Output HTML file. - -> Action () -buildMarkdown modname input output = do +import Debug.Trace (traceEventIO) + +buildMarkdown + :: Action (Context Text) + -> (FilePath -> Action Pandoc) + -> String -- ^ The name of the Agda module. + -> FilePath -- ^ Input markdown file, produced by the Agda compiler. + -> FilePath -- ^ Output HTML file. + -> Action () +buildMarkdown digest reader modname input output = do + liftIO $ traceEventIO $ "start buildMarkdown " <> modname gitCommit <- gitCommit skipAgda <- getSkipAgda + digest <- digest need [bibliographyName, input] modulePath <- findModule modname authors <- gitAuthors modulePath + let permalink = gitCommit modulePath @@ -222,14 +104,12 @@ buildMarkdown modname input output = do . Map.insert "link-citations" (MetaBool True) . unMeta - (markdown, references) <- traced "pandoc" do - Pandoc meta markdown <- readLabMarkdown input + Pandoc meta markdown <- reader input + (markdown, references) <- traced "citeproc" do let pandoc = addPageTitle (Pandoc (patchMeta meta) markdown) either (fail . show) pure =<< runIO do (,) <$> processCitations pandoc <*> getReferences Nothing pandoc - liftIO $ Dir.createDirectoryIfMissing True $ "_build/diagrams" modname - let refMap = Map.fromList $ map (\x -> (Cite.unItemId . Cite.referenceId $ x, x)) references (display, inline) = flip query markdown \case @@ -254,28 +134,16 @@ buildMarkdown modname input output = do filtered <- parallel $ map (runWriterT . walkM (patchBlock baseUrl modname)) blocks let - (bs, fold -> MarkdownState references defs) = unzip filtered + (bs, fold -> MarkdownState references defs) = unzip $!! filtered defs' = headerPopups bs markdown = walk blankPopup $ Pandoc meta bs - digest <- do - cssDigest <- getFileDigest "_build/html/css/default.css" - startJsDigest <- getFileDigest "_build/html/start.js" - mainJsDigest <- getFileDigest "_build/html/main.js" - pure . Context . Map.fromList $ - [ ("css", toVal (Text.pack cssDigest)) - , ("start-js", toVal (Text.pack startJsDigest)) - , ("main-js", toVal (Text.pack mainJsDigest)) - ] - text <- liftIO $ either (fail . show) pure =<< runIO (renderMarkdown authors references modname baseUrl digest markdown) - let tags = foldEquations False (parseTags text) - tags <- renderHighlights tags - traverse_ (checkMarkup input) tags + tags <- renderHighlights input $ foldEquations False $ parseTags text - traced "writing" do + traced "writing" $ do Dir.createDirectoryIfMissing False "_build/html/fragments" Dir.createDirectoryIfMissing False "_build/search" @@ -289,6 +157,7 @@ buildMarkdown modname input output = do runIO (renderMarkdown authors references modname baseUrl digest (Pandoc mempty bs)) Text.writeFile ("_build/html/fragments" Text.unpack key <.> "html") text + liftIO $ traceEventIO $ "end buildMarkdown " <> modname -- | Find the original Agda file from a 1Lab module name. findModule :: MonadIO m => String -> m FilePath @@ -350,7 +219,26 @@ data MarkdownState = MarkdownState , mdFragments :: Map.Map Text [Block] -- ^ List of definition blocks } - deriving (Show) + deriving (Show, Generic) + +instance NFData MarkdownState where + rnf (MarkdownState refs frags) = rnf frags `seq` go refs where + go [] = () + go (v:vs) = case v of + SimpleVal d -> rnf (Doclayout.render Nothing d) `seq` go vs + ListVal vs' -> go (vs' ++ vs) + MapVal ctx -> go (Map.elems (unContext ctx) ++ vs) + BoolVal b -> rnf b + NullVal -> () + +instance NFData a => NFData (Tag a) where + rnf = \case + TagOpen a b -> rnf a `seq` rnf b + TagClose a -> rnf a + TagText a -> rnf a + TagComment a -> rnf a + TagWarning a -> rnf a + TagPosition a b -> rnf a `seq` rnf b instance Semigroup MarkdownState where MarkdownState a b <> MarkdownState a' b' = MarkdownState (a <> a') (b <> b') @@ -358,10 +246,6 @@ instance Semigroup MarkdownState where instance Monoid MarkdownState where mempty = MarkdownState mempty mempty -diagramResource :: Resource -diagramResource = unsafePerformIO $ newResourceIO "diagram" 1 -{-# NOINLINE diagramResource #-} - -- | Patch a Pandoc block element. patchBlock :: (MonadIO f, MonadFail f, MonadWriter MarkdownState f, MonadTrans t, f ~ t Action) @@ -392,9 +276,6 @@ patchBlock _ mod (CodeBlock (id, classes, attrs) contents) | "quiver" `elem` cla -- This isn't the best in terms of atomicity, but it does preserve -- the nice property that diagrams are globally shared by their -- contents. - withResource diagramResource 1 $ liftIO do - Text.writeFile ("_build/diagrams" mod digest <.> "tex") contents - need [ "_build/html" lfn, "_build/html" dfn ] diagramHeight ("_build/html" lfn) @@ -631,6 +512,11 @@ headerPopups = go Nothing where go hdr (b:bs) = go hdr bs go hdr [] = mempty +-- | Write a HTML file, correctly handling the closing of some tags. +renderHTML5 :: [Tag Text] -> Text +renderHTML5 = renderTagsOptions renderOptions{ optMinimize = min } where + min = flip elem ["br", "meta", "link", "img", "hr"] + htmlInl :: Text -> Inline htmlInl = RawInline "html" diff --git a/support/shake/app/Shake/Markdown.hs-boot b/support/shake/app/Shake/Markdown.hs-boot deleted file mode 100644 index 00ccb0205..000000000 --- a/support/shake/app/Shake/Markdown.hs-boot +++ /dev/null @@ -1,6 +0,0 @@ -module Shake.Markdown where - -import Control.Monad.IO.Class (MonadIO) -import Text.Pandoc.Definition (Pandoc) - -readLabMarkdown :: MonadIO m => FilePath -> m Pandoc diff --git a/support/shake/app/Shake/Markdown/Reader.hs b/support/shake/app/Shake/Markdown/Reader.hs new file mode 100644 index 000000000..bf807ce1f --- /dev/null +++ b/support/shake/app/Shake/Markdown/Reader.hs @@ -0,0 +1,313 @@ +{-# LANGUAGE BlockArguments, OverloadedStrings, LambdaCase #-} +module Shake.Markdown.Reader (markdownReader, readLabMarkdown) where + +import Control.Monad.IO.Class +import Control.Monad + +import qualified Data.Text.Lazy.Builder as Builder +import qualified Data.Text.Lazy as Lazy +import qualified Data.Sequence as Seq +import qualified Data.Text.IO as Text +import qualified Data.Text as Text +import Data.Text.Lazy.Builder (Builder) +import Data.Sequence (Seq) +import Data.Foldable +import Data.Maybe +import Data.Char +import Data.Text (Text) + +import Development.Shake + +import GHC.Compact + +import Text.Pandoc.Shared +import Text.Pandoc.Walk +import Text.Pandoc hiding (trace) +import Debug.Trace (traceShow, trace) + +-- | Patch a sequence of inline elements. `patchInline' should be preferred +-- where possible, this is only useful when you cannot modify inlines in +-- isolation. +postParseInlines :: [Inline] -> [Inline] + +-- Float text that occurs directly after a mathematics span *inside* the +-- span. This allows the entire expression to reflow but preserves the +-- intended semantics of having e.g. `$n$-connected` be a single logical +-- unit (which should be line-wrapped together). +-- +-- The text is attached naïvely, so if the entire expression is a single +-- group (i.e. something like `${foo}$`), it will probably not work. +-- However, the naïve solution does have the benefit of automatically +-- attaching the non-wrapping text to the last "horizontal unit" in the +-- span. +-- +-- However, note that the glue between the original mathematics and the +-- attached text is treated as an opening delimiter. This is to have +-- correct spacing in case the maths ends with an operatorname, e.g. id. +postParseInlines (Math ty mtext:s@(Str txt):xs) + | not (Text.isPrefixOf " " txt) + = + let + glue = "\\mathopen{\\nobreak}\\textnormal{" <> txt <> "}" + mtext' = Text.stripEnd mtext <> glue + in postParseInlines (Math ty mtext':xs) + +-- Parse the contents of wikilinks as markdown. While Pandoc doesn't +-- read the title part of a wikilink, it will always consist of a single +-- Str span. We call the Pandoc parser in a pure context to read the +-- title part as an actual list of inlines. +postParseInlines (Link attr [Str contents] (url, "wikilink"):xs) = + link' `seq` link':postParseInlines xs where + + try = either (const Nothing) Just . runPure + fail = error $ + "Failed to parse contents of wikilink as Markdown:" <> Text.unpack contents + + link' = fromMaybe fail do + -- The contents of a link are valid if they consist of a single list + -- of inlines. Pandoc doesn't let us parse a list of inlines, but we + -- can still parse it as a document and ensure that (a) everything + -- got bunched in the same paragraph and (b) there was no metadata. + parsed@(Pandoc (Meta m) [Para is]) <- try (readMarkdown labReaderOptions contents) + guard (null m) -- I don't foresee this ever failing. + + -- Rendering the contents as plain text will strip all the + -- decorations, thus recovering the "underlying page" that was meant + -- to be linked to. Of course, we should only try changing the + -- target if the link looks like [[foo]], rather than [[foo|bar]]. + let + target = if url == contents + then stringify parsed + else url + + -- Note that Pandoc doesn't distinguish between [[foo]] and + -- [[foo|foo]], so really the only way is checking whether the URL + -- is equal to the contents string. If that was the case, then + -- stripping formatting is the right thing, otherwise e.g. [[*path + -- induction*]] would fail since the target "*path-induction*" + -- doesn't exist. + pure (Link attr is (target, "wikilink")) + +postParseInlines (x:xs) = x:postParseInlines xs +postParseInlines [] = [] + +data Posn = Posn { pLine :: {-# UNPACK #-} !Int, pCol :: {-# UNPACK #-} !Int } + deriving (Show) + +startPosn :: Posn +startPosn = Posn 1 1 + +advance :: Char -> Posn -> Posn +advance c (Posn line col) = case c of + '\n' -> Posn (line + 1) 1 + '\t' -> Posn line (col + 8) + c -> Posn line (col + 1) + +cols :: Int -> Posn -> Posn +cols n (Posn line col) = Posn line (n + col) + +nl :: Posn -> Posn +nl = advance '\n' + +type Message = [(Posn, String)] +type State = Posn -> String -> (Seq Message, Builder) + +(<:) :: Char -> (a, Builder) -> (a, Builder) +c <: (m, cs) = (m,) $! Builder.singleton c <> cs + +(<+) :: String -> (a, Builder) -> (a, Builder) +s <+ (m, cs) = (m,) $! Builder.fromString s <> cs + +msg :: Monoid a => Posn -> String -> (Seq Message, a) -> (Seq Message, a) +msg pn s (msg, x) = (msg Seq.|> [(pn, s)], x) + +msgs :: Monoid a => [(Posn, String)] -> (Seq Message, a) -> (Seq Message, a) +msgs msgs (msg, x) = (msg Seq.|> msgs, x) + +-- | Pandoc's wiki-link extension does not support splitting the guts of +-- a wikilink over multiple lines. +-- +-- The function 'mangleMarkdown' pre-processes the input file so that +-- any invalid space characters inside a wikilink are replaced by the +-- safe ASCII space @ @. +-- +-- It also performs some early validation. +mangleMarkdown :: FilePath -> String -> Text +mangleMarkdown filename = finish . startfile startPosn where + + finish :: (Seq Message, Builder) -> Text + finish (msgs, b) + | null (fold msgs) = Lazy.toStrict $ Builder.toLazyText b + | otherwise = error $ Text.unpack $ Text.stripEnd $ Text.unlines $ map Text.unlines $ map (map k) $ toList msgs + where k (Posn line col, s) = Text.pack (filename <> ":" <> show line <> ":" <> show col <> ": " <> s) + + startfile :: State + startfile !pn ('-':'-':'-':cs) = "---" <+ startcodeblock "metadata block" '-' pn 3 (cols 3 pn) cs + startfile !pn cs0 = content True pn cs0 + + content :: Bool -> State + content bol !pn = \case + ('[':'[':cs) -> "[[" <+ wikilink pn body (cols 2 pn) cs + ('^':'[':cs) -> "^[" <+ footnote pn body (cols 2 pn) cs + ('[':cs) -> '[' <: link pn body (cols 1 pn) cs + + ('~':'~':'~':cs) | bol -> "~~~" <+ startcodeblock "code block" '~' pn 3 (cols 3 pn) cs + ('`':'`':'`':cs) | bol -> "```" <+ startcodeblock "code block" '`' pn 3 (cols 3 pn) cs + + ('<':'!':'-':'-':cs) -> startcomment pn (cols 4 pn) cs + + ('<':'!':'-':cs) -> msg pn "stray ':cs) -> msg pn "stray -->" $ body (cols 3 pn) cs + ('-':'>':cs) -> msg pn "stray ->" $ body (cols 2 pn) cs + + ('\n':cs) -> newline' (if bol then 1 else 0) pn ('\n':cs) + (c:cs) + | isSpace c -> c <: content bol (advance c pn) cs + | otherwise -> c <: body (advance c pn) cs + + [] -> mempty + + body :: State + body = content False + + newline' :: Int -> State + newline' !d !pn ('\n':cs) = '\n' <: newline' (d + 1) (nl pn) cs + newline' !d !pn (c:cs) = content (d > 1) pn (c:cs) + newline' !d !pn [] = mempty + + newline :: State + newline = newline' 0 + + startend :: String -> Posn -> Posn -> (Seq Message, Builder) -> (Seq Message, Builder) + startend thing start end = msgs + [ (end, thing) + , (start, " ... opened here") + ] + + startcodeblock :: String -> Char -> Posn -> Int -> State + startcodeblock desc delim !start !fence !pn = \case + c:cs | c == delim -> c <: startcodeblock desc delim start (fence + 1) (cols 1 pn) cs + cs0 -> + let + loop !pn ('\n':cs) = codeblock desc delim start fence pn ('\n':cs) + loop !pn (c:cs) = c <: loop (advance c pn) cs + loop !pn [] = startend ("unterminated " <> desc) start pn mempty + in loop pn cs0 + + codeblock :: String -> Char -> Posn -> Int -> State + codeblock desc delim !start !fence !pn cs0 = + let + bol :: State + bol !pn (c:cs) + | isSpace c = c <: bol (advance c pn) cs + | c == delim = c <: leave (fence - 1) (cols 1 pn) cs + | otherwise = c <: codeblock desc delim start fence (advance c pn) cs + bol !pn [] = startend ("unterminated " <> desc) start pn mempty + + leave :: Int -> State + leave !0 !pn ('\n':cs) = newline pn ('\n':cs) + leave !0 !pn (c:cs) = msg pn "junk after code block terminator" $ body pn (c:cs) + + leave !n !pn (c:cs) + | c == delim = c <: leave (n - 1) (cols 1 pn) cs + | otherwise = codeblock desc delim start fence pn (c:cs) + + in case cs0 of + '\n':cs -> '\n' <: bol (nl pn) cs + c:cs -> c <: codeblock desc delim start fence (advance c pn) cs + [] -> startend ("unterminated " <> desc) start pn mempty + + startcomment :: Posn -> State + startcomment !start !pn = \case + [] -> startend "unterminated comment" start pn mempty + ('[':'T':'O':'D':'O':cs) -> comment start False leavecomment pn cs + + (c:cs) + | isSpace c -> startcomment start (advance c pn) cs + | otherwise -> "
\n" <+ comment start True leavecomment pn (c:cs) + + leavecomment :: State + leavecomment !pn cs = "
" <+ body pn cs + + comment :: Posn -> Bool -> State -> State + comment !start content k !pn cs0 = case cs0 of + [] -> startend "unterminated comment" start pn mempty + + ('-':'-':'>':cs) -> k (cols 3 pn) cs + ('<':'!':'-':'-':cs) -> comment pn content (comment start content k) (cols 4 pn) cs + + ('[':'[':cs) | content -> "[[" <+ wikilink pn (comment start True k) (cols 2 pn) cs + ('^':'[':cs) | content -> "^[" <+ footnote pn (comment start True k) (cols 2 pn) cs + ('[':cs) | content -> '[' <: link pn (comment start True k) (cols 1 pn) cs + (c:cs) + | content -> c <: comment start content k (advance c pn) cs + | otherwise -> comment start content k (advance c pn) cs + + noparbreak :: Char -> String -> Posn -> State -> State + noparbreak ch thing start cont !pn = (ch <:) . loop False (nl pn) where + loop failed !pn ('\n':cs) = ch <: loop True (nl pn) cs + loop failed !pn (c:cs) + | failed = startend ("illegal paragraph break inside " <> thing) start pn $ content True pn (c:cs) + | otherwise = cont pn (c:cs) + loop failed !pn [] = startend ("unterminated " <> thing) start pn mempty + + wikilink :: Posn -> State -> State + wikilink !start k !pn = \case + ('\n':cs) -> noparbreak ' ' "wikilink" start (wikilink start k) pn cs + + (']':']':cs) -> "]]" <+ k (cols 2 pn) cs + + ('[':'[':cs) -> "[[" <+ wikilink pn (wikilink start k) (cols 1 pn) cs + ('[':cs) -> '[' <: link pn (wikilink start k) (cols 1 pn) cs + + (c:cs) + | isSpace c -> ' ' <: wikilink start k (advance c pn) cs + | otherwise -> c <: wikilink start k (advance c pn) cs + [] -> msg start "unterminated wikilink" mempty + + link' :: Bool -> Posn -> State -> State + link' footnote !start k !pn cs0 = case cs0 of + ('\n':cs) -> noparbreak '\n' (if footnote then "footnote" else "link") start (link' footnote start k) pn cs + + (']':cs) -> ']' <: k (cols 1 pn) cs + + ('[':'[':cs) -> "[[" <+ wikilink pn (link' footnote start k) (cols 1 pn) cs + ('[':cs) -> '[' <: link pn (link' footnote start k) (cols 1 pn) cs + + (c:cs) -> c <: link' footnote start k (advance c pn) cs + + [] -> msg start "unterminated wikilink" mempty + + link, footnote :: Posn -> State -> State + link = link' False + footnote = link' True + +labReaderOptions :: ReaderOptions +labReaderOptions = + let + good = [ Ext_wikilinks_title_before_pipe ] + bad = [Ext_definition_lists, Ext_compact_definition_lists] + exts = foldr disableExtension + (foldr enableExtension (getDefaultExtensions "markdown") good) + bad + in def { readerExtensions = exts } + +readLabMarkdown :: MonadIO m => FilePath -> m Pandoc +readLabMarkdown fp = liftIO cont where + + unParaMath :: Block -> Block + unParaMath (Para [Math DisplayMath m]) = Plain [Math DisplayMath m] + unParaMath x = x + + cont :: IO Pandoc + cont = do + contents <- mangleMarkdown fp <$> readFile fp + doc <- either (fail . show) compactWithSharing =<< runIO do + doc <- readMarkdown labReaderOptions [(fp, contents)] + pure $ walk unParaMath $ walk postParseInlines doc + pure $! getCompact doc + +markdownReader :: Rules (FilePath -> Action Pandoc) +markdownReader = newCache \fp -> do + need [fp] + traced "pandoc" $ readLabMarkdown fp diff --git a/support/shake/app/Shake/Modules.hs b/support/shake/app/Shake/Modules.hs index fce510811..6cc4f62df 100644 --- a/support/shake/app/Shake/Modules.hs +++ b/support/shake/app/Shake/Modules.hs @@ -1,12 +1,14 @@ -- | Rules for working with our Agda modules. -{-# LANGUAGE BlockArguments, TypeFamilies, DeriveGeneric #-} +{-# LANGUAGE BlockArguments, TypeFamilies, DeriveGeneric, LambdaCase #-} module Shake.Modules ( ModName , ModKind(..) , moduleRules , getOurModules , getAllModules + , markdownSource + , moduleName ) where import qualified Data.Map.Strict as Map @@ -16,12 +18,12 @@ import Development.Shake.Classes import Development.Shake.FilePath import Development.Shake -import GHC.Generics (Generic) +import Data.List -import HTML.Backend (moduleName) +import GHC.Generics (Generic) -import Shake.Git import Shake.Options +import Shake.Git type ModName = String @@ -42,7 +44,7 @@ instance Hashable ModKind where instance Binary ModKind where instance NFData ModKind where -newtype ModulesA = ModulesA { unModulesA :: Map ModName ModKind } +newtype ModulesA = ModulesA { unModulesA :: Map ModName (String, ModKind) } deriving (Eq, Ord, Show, Typeable, Generic) instance Hashable ModulesA where @@ -66,15 +68,15 @@ moduleRules = do else getDirectoryFiles "src" ["**/*.agda", "**/*.lagda.md"] toOut x | takeExtensions x == ".lagda.md" - = (moduleName (dropExtensions x), WithText) - toOut x = (moduleName (dropExtensions x), CodeOnly) + = (moduleName (dropExtensions x), ("src" x, WithText)) + toOut x = (moduleName (dropExtensions x), ("src" x, CodeOnly)) ModulesA . Map.fromList . map toOut <$> getFiles pure () -- | Get all 1Lab modules. getOurModules :: Action (Map ModName ModKind) -getOurModules = unModulesA <$> askOracle ModulesQ +getOurModules = fmap snd . unModulesA <$> askOracle ModulesQ -- | Get all Agda modules used within the project. getAllModules :: Action (Map ModName ModKind) @@ -82,3 +84,13 @@ getAllModules = do our <- getOurModules pure $ Map.singleton "all-pages" CodeOnly <> our + +markdownSource :: ModName -> Action FilePath +markdownSource mod = fmap (Map.lookup mod . unModulesA) (askOracle ModulesQ) >>= \case + Just (fp, WithText) -> pure fp + Just (fp, CodeOnly) -> error $ "Not a markdown module: " <> mod + Nothing -> error $ "Not a module: " <> mod + +-- | Determine the name of a module from a file like @1Lab/HIT/Torus@. +moduleName :: FilePath -> String +moduleName = intercalate "." . splitDirectories diff --git a/support/shake/app/Shake/Recent.hs b/support/shake/app/Shake/Recent.hs index 6b4cb8671..7250455b8 100644 --- a/support/shake/app/Shake/Recent.hs +++ b/support/shake/app/Shake/Recent.hs @@ -16,7 +16,7 @@ import Development.Shake import HTML.Backend -import Shake.Modules (getOurModules) +import Shake.Modules (getOurModules, moduleName) import Shake.Git (gitCommand) import qualified Text.Blaze.Html5.Attributes as A diff --git a/support/web/js/highlight-hover.ts b/support/web/js/highlight-hover.ts index 7e406a7ee..39c3a2d29 100644 --- a/support/web/js/highlight-hover.ts +++ b/support/web/js/highlight-hover.ts @@ -5,7 +5,7 @@ import { Hover } from './lib/hover'; let links: Array = []; -const paths: { module: string, baseURL: string, source: string } = window as any; +const paths: { module: string, baseUrl: string, source: string } = window as any; const page = window.location.pathname.slice(1).replace(".html", ""); @@ -22,7 +22,7 @@ const types: Map> = new Map(); async function fetchTypes(mod: string): Promise { if (types.get(mod)) return types.get(mod)!; - const prommy = fetch(`${paths.baseURL}/types/${mod}.json`, { method: 'get' }).then(async (r) => { + const prommy = fetch(`${paths.baseUrl}/types/${mod}.json`, { method: 'get' }).then(async (r) => { if (!r.ok) throw `Failed to load type-on-hover information for module ${paths.module}`; return await r.json() as string[]; }); @@ -39,14 +39,18 @@ async function fetchTypes(mod: string): Promise { * @returns The instantiated hover, or undefined if this element has no associated popup. */ function getHover(a: HTMLAnchorElement): Hover | undefined { - let target; if (Hover.get(a)) return Hover.get(a); - if (!Number.isNaN(target = Number.parseInt(a.getAttribute("data-identifier") ?? ""))) { + const href = a.getAttribute("href")?.split('/').slice(-1)[0]; + if (!href) return; + + let target: number | string | null = null; + const [mod, tgts] = a.getAttribute("data-type") ? href.split('#') : []; + + if (!Number.isNaN(target = Number.parseInt(tgts))) { let tgt = target; - const mod = a.getAttribute("data-module") ?? paths.module; - const get = fetchTypes(mod).then((tys) => { + const get = fetchTypes(mod.slice(0, -5)).then((tys) => { const element = document.createElement("div"); element.innerHTML = tys[tgt]!; element.classList.add("hover-popup", "sourceCode"); @@ -57,7 +61,7 @@ function getHover(a: HTMLAnchorElement): Hover | undefined { return new Hover(a, get, true); } else if ((target = a.getAttribute("data-target")) != null) { const tgt = target; - const get = fetch(`${paths.baseURL}/fragments/${tgt}.html`, { method: 'get' }).then(async (p) => { + const get = fetch(`${paths.baseUrl}/fragments/${tgt}.html`, { method: 'get' }).then(async (p) => { if (!p.ok) throw `Failed to load fragment ${tgt}`; const element = document.createElement("div"); diff --git a/support/web/js/lib/hover.ts b/support/web/js/lib/hover.ts index cba63350b..dd1441b0a 100644 --- a/support/web/js/lib/hover.ts +++ b/support/web/js/lib/hover.ts @@ -65,6 +65,24 @@ export class Hover { private fadeDirection?: 'up' | 'down'; + /** + * Fade the popup into the specified state. + */ + private async fade(state: 'in' | 'out') { + if (this.ephemeral) return; + + const el = await this.element, other = state === 'in' ? 'out' : 'in'; + + // Have to remove the fade class for *both* of the other states + // otherwise a popup that has changed direction will flash when + // fading in (since it'll have both e.g. `popup-fade-out-down` and + // `popup-fade-in-up` classes). + el.classList.remove(`popup-fade-${other}-up`); + el.classList.remove(`popup-fade-${other}-down`); + + el.classList.add(`popup-fade-${state}-${this.fadeDirection}`); + } + /** * Show the popup and decide on the positioning, hence in which * direction the popup will fade. @@ -77,11 +95,13 @@ export class Hover { const selfRect = this.anchor.getBoundingClientRect(); const hoverRect = el.getBoundingClientRect(); - const textRect = document.querySelector("div#post-toc-container > article")!.getBoundingClientRect(); + const textRect = document.querySelector("div#post-toc-container > article"); + + let right = textRect?.getBoundingClientRect().right ?? window.innerWidth; if (selfRect.bottom + hoverRect.height + 48 > window.innerHeight) { // Tooltip placed above anchor - el.style.top = `calc(${window.scrollY + selfRect.top - hoverRect.height}px - 1.3rem)`; + el.style.top = `calc(${window.scrollY + selfRect.top - hoverRect.height}px)`; this.fadeDirection = 'down'; } else { // Tooltip placed below anchor @@ -89,16 +109,13 @@ export class Hover { this.fadeDirection = 'up'; } - if (selfRect.left + hoverRect.width > textRect.right) { + if (selfRect.left + hoverRect.width > right) { el.style.left = `calc(${selfRect.right - hoverRect.width}px)`; } else { el.style.left = `${selfRect.left}px`; } - if (!this.ephemeral) { - el.classList.remove(`popup-fade-out-${this.fadeDirection}`); - el.classList.add(`popup-fade-in-${this.fadeDirection}`); - } + this.fade('in'); // Instead of having a boolean to indicate what's been shown, we use // the closing signal as a sentinel instead. @@ -142,15 +159,12 @@ export class Hover { if (this.shown) this.shown(); delete this.shown; - if (!this.ephemeral) { - el.classList.remove(`popup-fade-in-${this.fadeDirection}`); - el.classList.add(`popup-fade-out-${this.fadeDirection}`); - } + this.fade('out'); this.closing = new Timeout(this.ephemeral ? 0 : 250, `displace ${this.anchor}`); await this.closing.start(); - el.classList.add('popup-hidden') + el.classList.add('popup-hidden'); delete this.closing; diff --git a/support/web/js/theme.tsx b/support/web/js/theme.tsx index c5eeb5f41..8526fbf9c 100644 --- a/support/web/js/theme.tsx +++ b/support/web/js/theme.tsx @@ -3,10 +3,10 @@ import { type Theme, themeSetting, equationSetting, Setting, hiddenCodeSetting, // This is pretty evil, but a loose