fix inner links
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful

This commit is contained in:
Michael Zhang 2024-09-18 16:22:37 -05:00
parent 67e9a31def
commit c9c6365c87
3 changed files with 31 additions and 14 deletions

View file

@ -89,9 +89,7 @@ export const mkdocsConfig: Partial<Config> = {
titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)), titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)),
titleTextMap: (title: string) => { titleTextMap: (title: string) => {
console.log("title", title);
const match = title.match(TITLE_PATTERN); const match = title.match(TITLE_PATTERN);
console.log("matches", match);
const displayTitle = match?.[1] ?? ""; const displayTitle = match?.[1] ?? "";
const checkedTitle = displayTitle; const checkedTitle = displayTitle;
return { displayTitle, checkedTitle }; return { displayTitle, checkedTitle };

View file

@ -14,7 +14,7 @@ import {
writeFileSync, writeFileSync,
} from "node:fs"; } from "node:fs";
import { tmpdir } from "node:os"; 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 { visit } from "unist-util-visit";
import type { RemarkPlugin } from "@astrojs/markdown-remark"; 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); const doc = readFileSync(outputFile);
// This is the post-processed markdown with HTML code blocks replacing the Agda code blocks // 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("#"); const [href, hash, ...rest] = node.properties.href.split("#");
if (rest.length > 0) throw new Error("come look at this"); 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)) { if (referencedFiles.has(href)) {
node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`; node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`;

View file

@ -6,12 +6,20 @@ tags: [hott, cubical]
draft: true 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
<details> <details>
<summary>Imports</summary> <summary>Imports for Agda</summary>
``` ```
{-# OPTIONS --cubical #-} {-# OPTIONS --cubical #-}
@ -29,7 +37,9 @@ open import Data.Bool.Base hiding (_∧_; __)
## Two-dimensional case ## 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}$. "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: 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)$ ## 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). Suppose we want to prove that all [mere proposition]s ([h-level] 1) are [sets] ([h-level] 2).
This result exists in the cubical standard library, but let's go over it here. 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 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 = -- ... 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$. 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. If we want to find a path between $p$ and $q$, we'll want another dimension.
Let's call this $j$. Let's call this $j$.