From c9c6365c8701e34bc3235d459feb6104ebde160b Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 18 Sep 2024 16:22:37 -0500 Subject: [PATCH] fix inner links --- plugin/remark-admonitions.ts | 2 -- plugin/remark-agda.ts | 12 ++++--- .../posts/2024-09-18-hcomp/index.lagda.md | 31 ++++++++++++++----- 3 files changed, 31 insertions(+), 14 deletions(-) diff --git a/plugin/remark-admonitions.ts b/plugin/remark-admonitions.ts index 87ee409..b6e39e2 100644 --- a/plugin/remark-admonitions.ts +++ b/plugin/remark-admonitions.ts @@ -89,9 +89,7 @@ export const mkdocsConfig: Partial = { titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)), titleTextMap: (title: string) => { - console.log("title", title); const match = title.match(TITLE_PATTERN); - console.log("matches", match); const displayTitle = match?.[1] ?? ""; const checkedTitle = displayTitle; return { displayTitle, checkedTitle }; diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts index 8e4c300..0213847 100644 --- a/plugin/remark-agda.ts +++ b/plugin/remark-agda.ts @@ -14,7 +14,7 @@ import { writeFileSync, } from "node:fs"; import { tmpdir } from "node:os"; -import { join, parse } from "node:path"; +import { join, parse, resolve, basename } from "node:path"; import { visit } from "unist-util-visit"; import type { RemarkPlugin } from "@astrojs/markdown-remark"; @@ -109,9 +109,11 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => { } } - const htmlname = parse(path).base.replace(/\.lagda.md/, ".html"); + const htmlname = basename(resolve(outputFile)).replace( + /(\.lagda)?\.md/, + ".html", + ); - console.log("Output file:", outputFile); const doc = readFileSync(outputFile); // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks @@ -131,7 +133,9 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => { const [href, hash, ...rest] = node.properties.href.split("#"); if (rest.length > 0) throw new Error("come look at this"); - if (href === htmlname) node.properties.href = `#${hash}`; + if (href === htmlname) { + node.properties.href = `#${hash}`; + } if (referencedFiles.has(href)) { node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`; diff --git a/src/content/posts/2024-09-18-hcomp/index.lagda.md b/src/content/posts/2024-09-18-hcomp/index.lagda.md index 4f47fa5..eb3d87f 100644 --- a/src/content/posts/2024-09-18-hcomp/index.lagda.md +++ b/src/content/posts/2024-09-18-hcomp/index.lagda.md @@ -6,12 +6,20 @@ tags: [hott, cubical] draft: true --- -**hcomp** is a primitive operation in [cubical type theory][cchm] that completes the _lid_ of an incomplete cube, given the bottom face and some number of side faces. +[**hcomp**][1] is a primitive operation in [cubical type theory][cubical] that completes the _lid_ of an incomplete cube, given the bottom face and some number of side faces. -[CCHM]: https://arxiv.org/abs/1611.02108 +[1]: https://agda.readthedocs.io/en/latest/language/cubical.html#homogeneous-composition +[cubical]: https://arxiv.org/abs/1611.02108 + +> [!admonition: NOTE] +> All the code samples in this document are written in _and_ checked for correctness by [Agda], a dependently typed programming language that implements cubical type theory. +> Many of the names and symbols in the names are clickable links that take you to where that symbol is defined. +> Below are all of the imports required for this page to work. + +[agda]: https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html
-Imports +Imports for Agda ``` {-# OPTIONS --cubical #-} @@ -29,7 +37,9 @@ open import Data.Bool.Base hiding (_∧_; _∨_) ## Two-dimensional case -In two dimensions, hcomp can be understood as the double-composition operation. +In two dimensions, $\mathsf{hcomp}$ can be understood as the double-composition operation. +Given three paths $p : x \equiv y$, $q : y \equiv z$ and $r : x \equiv w$, it will return a path representing the composed path $((\sim r) \cdot p \cdot q) : (w ≡ z)$. + "Single" composition (between two paths rather than three) is typically implemented as a double composition with the left leg as $\mathsf{refl}$. Without the double composition, this looks like: @@ -48,8 +58,13 @@ The `(i = i0)` case in this case is $\mathsf{refl}_x(j)$ which is definitionally ## Example: $\mathsf{isProp}(A) \rightarrow \mathsf{isSet}(A)$ -Suppose we want to prove that all mere propositions (h-level 1) are sets (h-level 2). -This result exists in the cubical standard library, but let's go over it here. +Suppose we want to prove that all [mere proposition]s ([h-level] 1) are [sets] ([h-level] 2). +This result exists in the [cubical library], but let's go over it here. + +[sets]: https://ncatlab.org/nlab/show/h-set +[mere proposition]: https://ncatlab.org/nlab/show/mere+proposition +[h-level]: https://ncatlab.org/nlab/show/homotopy+level +[cubical library]: https://github.com/agda/cubical/ ``` isProp→isSet : {A : Type} → isProp A → isSet A @@ -58,9 +73,9 @@ isProp→isSet {A} f = goal where goal x y p q j i = -- ... ``` -We're given a type $A$, some proof that it's a mere proposition, let's call it $f : \mathsf{isProp}(A)$. +We're given a type $A$, some proof that it's a [mere proposition], let's call it $f : \mathsf{isProp}(A)$. -Now let's construct an hcomp. In a set, we'd want paths $p$ and $q$ between the same points $x$ and $y$ to be equal. +Now let's construct an hcomp. In a [set][sets], we'd want paths $p$ and $q$ between the same points $x$ and $y$ to be identified. Suppose $p$ and $q$ operate over the same dimension, $i$. If we want to find a path between $p$ and $q$, we'll want another dimension. Let's call this $j$.