Compare commits

..

1 commit

Author SHA1 Message Date
ebba251502 update
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
2024-09-14 23:33:32 -05:00
153 changed files with 3234 additions and 4894 deletions

View file

@ -1,4 +1,3 @@
public
package-lock.json
src/styles/fork-awesome
pnpm-lock.yaml
src/styles/fork-awesome

View file

@ -1,3 +0,0 @@
{
"npm.packageManager": "pnpm"
}

26
.woodpecker.yml Normal file
View file

@ -0,0 +1,26 @@
steps:
build:
image: git.mzhang.io/michael/blog-docker-builder:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
environment:
- ASTRO_TELEMETRY_DISABLED=1
commands:
- mkdir /tmp
- rm -rf node_modules
- npm i -g pnpm@9.4.0
- npx pnpm install --frozen-lockfile
- npx pnpm run build
when:
- event: push
deploy:
image: git.mzhang.io/michael/blog-docker-builder:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
commands:
- echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY
- chmod 600 SSH_SECRET_KEY
- mkdir -p ~/.ssh
- echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIO+RKFYjD8UjqhfOHFHNyijkbGzC4fJEIIhrBwHj+FsQ" >> known_hosts
- rsync -azrP -e "ssh -i SSH_SECRET_KEY -o UserKnownHostsFile=known_hosts" dist/ blogDeploy@mzhang.io:/home/blogDeploy/public
secrets: [SSH_SECRET_KEY]
when:
- branch: master
event: push

View file

@ -1,27 +0,0 @@
steps:
build:
image: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
environment:
- ASTRO_TELEMETRY_DISABLED=1
commands:
- mkdir /tmp
- rm -rf node_modules
- npm i -g pnpm@9.4.0
- npx pnpm install --frozen-lockfile
- npx pnpm run build
when:
- event: push
deploy:
image: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
commands:
- mc alias set $AWS_DEFAULT_REGION $AWS_ENDPOINT_URL $AWS_ACCESS_KEY_ID $AWS_SECRET_ACCESS_KEY --api S3v4
- mc mirror --overwrite ./dist/ $AWS_DEFAULT_REGION/mzhang-io-website/
secrets:
- AWS_ACCESS_KEY_ID
- AWS_DEFAULT_REGION
- AWS_ENDPOINT_URL
- AWS_SECRET_ACCESS_KEY
when:
- branch: master
event: push

View file

@ -2,4 +2,4 @@
https://mzhang.io
License: GPL-3.0 code / CC-BY-SA-4.0 contents
License: GPL-3.0 / CC-BY-SA-4.0

View file

@ -22,7 +22,6 @@ const publicDir = "public";
// https://astro.build/config
export default defineConfig({
site: "https://mzhang.io",
prefetch: true,
integrations: [mdx(), sitemap(), markdoc()],
outDir,
@ -35,7 +34,7 @@ export default defineConfig({
shikiConfig: { theme: "css-variables" },
remarkPlugins: [
() => remarkAgda({ outDir, base, publicDir }),
[remarkMath, {}],
remarkMath,
[remarkAdmonitions, mkdocsConfig],
remarkReadingTime,
remarkTypst,

View file

@ -1,2 +1,2 @@
include: src/posts src
include: src/content/posts src
depend: standard-library cubical

BIN
bun.lockb

Binary file not shown.

View file

@ -3,16 +3,14 @@
"agda": {
"inputs": {
"flake-parts": "flake-parts",
"nixpkgs": [
"nixpkgs"
]
"nixpkgs": "nixpkgs"
},
"locked": {
"lastModified": 1729253305,
"narHash": "sha256-S7/C8VGMrXeGhFeYXx1cVBjZlNVB5L1o/SkW0hFm0Jc=",
"lastModified": 1719426791,
"narHash": "sha256-jiPGzJM+XMwb1OwyxpbY6jV0Lzr5yLKnPSMZbueFNRM=",
"owner": "agda",
"repo": "agda",
"rev": "3425ed5543d2e6f98094b834fedcdec3a2fb67a6",
"rev": "777b07f573c7526d677c18c25e44b24a849bc03b",
"type": "github"
},
"original": {
@ -44,11 +42,11 @@
"systems": "systems"
},
"locked": {
"lastModified": 1726560853,
"narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
"lastModified": 1710146030,
"narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
"rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
"type": "github"
},
"original": {
@ -58,16 +56,18 @@
},
"nixpkgs": {
"locked": {
"lastModified": 1729265718,
"narHash": "sha256-4HQI+6LsO3kpWTYuVGIzhJs1cetFcwT7quWCk/6rqeo=",
"lastModified": 1702346276,
"narHash": "sha256-eAQgwIWApFQ40ipeOjVSoK4TEHVd6nbSd9fApiHIw5A=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "ccc0c2126893dd20963580b6478d1a10a4512185",
"rev": "cf28ee258fd5f9a52de6b9865cdb93a1f96d09b7",
"type": "github"
},
"original": {
"id": "nixpkgs",
"type": "indirect"
"owner": "NixOS",
"ref": "nixos-23.11",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-lib": {
@ -88,11 +88,25 @@
"type": "github"
}
},
"nixpkgs_2": {
"locked": {
"lastModified": 1718089647,
"narHash": "sha256-COO4Xk2EzlZ3x9KCiJildlAA6cYDSPlnY8ms7pKl2Iw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "f7207adcc68d9cafa29e3cd252a18743ae512c6a",
"type": "github"
},
"original": {
"id": "nixpkgs",
"type": "indirect"
}
},
"root": {
"inputs": {
"agda": "agda",
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs"
"nixpkgs": "nixpkgs_2"
}
},
"systems": {

View file

@ -1,13 +1,12 @@
{
inputs.agda.url = "github:agda/agda";
inputs.agda.inputs.nixpkgs.follows = "nixpkgs";
outputs = { self, nixpkgs, flake-utils, agda, }:
flake-utils.lib.eachDefaultSystem (system:
let
pkgs = import nixpkgs { inherit system; overlays = [ agda.overlays.default ]; };
pkgs = import nixpkgs { inherit system; };
agda-pkg = agda.packages.x86_64-linux.default;
flakePkgs = rec {
agda-bin = pkgs.callPackage ./nix/agda-bin.nix { agda-pkg = pkgs.haskellPackages.Agda.bin; };
agda-bin = pkgs.callPackage ./nix/agda-bin.nix { inherit agda-pkg; };
docker-builder =
pkgs.callPackage ./nix/docker-builder.nix { inherit agda-bin; };
};
@ -19,9 +18,13 @@
packages = with pkgs;
with flakePkgs; [
bun
woodpecker-cli
nixfmt-rfc-style
dive
nix-tree
vips
shellcheck
agda-bin
nodejs_20
corepack

View file

@ -6,8 +6,8 @@ let
writeTextFile {
name = "agda-libraries";
text = ''
${agdaPackages.cubical.src}/cubical.agda-lib
${agdaPackages.standard-library.src}/standard-library.agda-lib
${agdaPackages.cubical}/cubical.agda-lib
${agdaPackages.standard-library}/standard-library.agda-lib
'';
};

View file

@ -1,15 +1,13 @@
{ dockerTools
, agda-bin
, bash
, corepack
, coreutils
, gitMinimal
, gnused
, minio-client
, nodejs_20
, openssh
, pkgsLinux
, rsync
, openssh
, bash
, coreutils
, nodejs_20
, gnused
, pkgsLinux
}:
dockerTools.buildLayeredImage {
@ -17,18 +15,16 @@ dockerTools.buildLayeredImage {
contents = with dockerTools; [
agda-bin
bash
caCertificates
corepack
coreutils
fakeNss
gitMinimal
gnused
minio-client
nodejs_20
openssh
rsync
openssh
bash
coreutils
nodejs_20
gnused
usrBinEnv
caCertificates
fakeNss
];
# fakeRootCommands = ''

View file

@ -12,18 +12,18 @@
"format": "prettier -w ."
},
"dependencies": {
"@astrojs/markdoc": "^0.12.4",
"@astrojs/markdown-remark": "^6.0.1",
"@astrojs/mdx": "^4.0.3",
"@astrojs/rss": "^4.0.10",
"@astrojs/sitemap": "^3.2.1",
"@astrojs/markdoc": "^0.11.1",
"@astrojs/markdown-remark": "^5.1.1",
"@astrojs/mdx": "^1.1.5",
"@astrojs/rss": "^3.0.0",
"@astrojs/sitemap": "^3.1.6",
"@justfork/rehype-autolink-headings": "^5.1.1",
"astro": "^5.1.1",
"astro": "^3.6.5",
"astro-imagetools": "^0.9.0",
"astro-remark-description": "^1.1.2",
"classnames": "^2.5.1",
"fork-awesome": "^1.2.0",
"katex": "^0.16.18",
"katex": "^0.16.10",
"lodash-es": "^4.17.21",
"mdast-util-to-string": "^4.0.0",
"nanoid": "^4.0.2",
@ -32,24 +32,22 @@
"rehype-katex": "^6.0.3",
"remark-emoji": "^4.0.1",
"remark-github-beta-blockquote-admonitions": "^2.2.1",
"remark-math": "^6.0.0",
"remark-math": "^5.1.1",
"remark-parse": "^10.0.2",
"sanitize-html": "^2.14.0",
"sharp": "^0.33.5"
"sharp": "^0.33.4"
},
"devDependencies": {
"@biomejs/biome": "^1.9.4",
"@biomejs/biome": "^1.8.2",
"@types/lodash-es": "^4.17.12",
"@types/sanitize-html": "^2.13.0",
"date-fns": "^2.30.0",
"hast-util-from-html": "^2.0.3",
"hast-util-to-html": "^9.0.4",
"hast-util-from-html": "^2.0.1",
"hast-util-to-html": "^9.0.1",
"mdast": "^3.0.0",
"mdast-util-from-markdown": "^2.0.2",
"prettier": "^3.4.2",
"mdast-util-from-markdown": "^2.0.1",
"prettier": "^3.3.2",
"prettier-plugin-astro": "^0.12.3",
"rehype-slug": "^6.0.0",
"sass": "^1.83.0",
"sass": "^1.77.6",
"shiki": "^0.14.7",
"unified": "^11.0.5",
"unist-util-visit": "^5.0.0"

View file

@ -89,7 +89,9 @@ export const mkdocsConfig: Partial<Config> = {
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 };

View file

@ -14,7 +14,7 @@ import {
writeFileSync,
} from "node:fs";
import { tmpdir } from "node:os";
import { join, parse, resolve, basename } from "node:path";
import { join, parse } from "node:path";
import { visit } from "unist-util-visit";
import type { RemarkPlugin } from "@astrojs/markdown-remark";
@ -32,10 +32,12 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
const path: string = history[history.length - 1]!;
if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
// console.log("AGDA:processing path", path);
console.log("AGDA:processing path", path);
const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
const agdaOutDir = join(tempDir, "output");
const agdaOutFilename = parse(path).base.replace(/\.lagda.md/, ".md");
const agdaOutFile = join(agdaOutDir, agdaOutFilename);
mkdirSync(agdaOutDir, { recursive: true });
const childOutput = spawnSync(
@ -50,28 +52,21 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
{},
);
// Locate output file
const directory = readdirSync(agdaOutDir);
const outputFilename = directory.find((name) => name.endsWith(".md"));
if (childOutput.status !== 0 || outputFilename === undefined) {
if (childOutput.error || !existsSync(agdaOutFile)) {
throw new Error(
`Agda output:
`Agda error:
Stdout:
${childOutput.stdout}
Stderr:
${childOutput.stderr}
`,
${childOutput.stderr}`,
{
cause: childOutput.error,
},
);
}
const outputFile = join(agdaOutDir, outputFilename);
// // TODO: Handle child output
// console.error("--AGDA OUTPUT--");
// console.error(childOutput);
@ -94,7 +89,6 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8" />
<link rel="stylesheet" href="${base}generated/agda/Agda.css" />
</head>
<body>
@ -110,9 +104,9 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
}
}
const htmlname = basename(resolve(outputFile)).replace(/(\.lagda)?\.md/, ".html");
const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
const doc = readFileSync(outputFile);
const doc = readFileSync(agdaOutFile);
// This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
const tree2 = fromMarkdown(doc);
@ -131,9 +125,7 @@ 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}` : ""}`;
@ -151,23 +143,13 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
});
let idx = 0;
try {
visit(tree, "code", (node) => {
if (!(node.lang === null || node.lang === "agda")) return;
visit(tree, "code", (node) => {
if (!(node.lang === null || node.lang === "agda")) return;
if (idx > collectedCodeBlocks.length) {
throw new Error("failed");
}
node.type = "html";
node.value = collectedCodeBlocks[idx].contents;
idx += 1;
});
} catch (e) {
// TODO: Figure out a way to handle this correctly
// Possibly by diffing?
console.log("Mismatch in number of args. Perhaps there was an empty block?");
}
node.type = "html";
node.value = collectedCodeBlocks[idx].contents;
idx += 1;
});
};
};

View file

@ -1,10 +1,10 @@
import getReadingTime from "reading-time";
import { toString as mdastToString } from "mdast-util-to-string";
import { toString } from "mdast-util-to-string";
import type { RemarkPlugin } from "@astrojs/markdown-remark";
const remarkReadingTime: RemarkPlugin = () => {
return (tree, { data }) => {
const textOnPage = mdastToString(tree);
const textOnPage = toString(tree);
const readingTime = getReadingTime(textOnPage);
// readingTime.text will give us minutes read as a friendly string,

File diff suppressed because it is too large Load diff

Binary file not shown.

Before

Width:  |  Height:  |  Size: 136 KiB

View file

@ -1,3 +1,2 @@
User-agent: *
Allow: /
Disallow: /drafts
Allow: /

View file

Before

Width:  |  Height:  |  Size: 24 KiB

After

Width:  |  Height:  |  Size: 24 KiB

View file

@ -1,27 +1,16 @@
---
import "../styles/footer.scss";
import { execSync } from "node:child_process";
const dateUpdated = new Date();
const gitRevShort = execSync("git rev-parse --short HEAD").toString().trim();
const gitRev = execSync("git rev-parse HEAD").toString().trim();
---
<footer>
<p>
Blog theme and contents written by Michael Zhang with the <a
href="https://astro.build/"
target="_blank"
rel="noreferrer noopener">Astro</a
> framework.
<br />
Last updated {dateUpdated.toLocaleString(undefined, { dateStyle: "full" })} at commit
<a
href={`https://git.mzhang.io/michael/blog/commit/${gitRev}`}
class="colorlink"
target="_blank">{gitRevShort}</a
Blog code licensed under <a href="https://www.gnu.org/licenses/gpl-3.0.txt" target="_blank"
>GPL-3.0</a
>. Post contents licensed under <a
href="https://creativecommons.org/licenses/by-sa/4.0/legalcode.txt">CC BY-SA 4.0</a
>.
<br />
<a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source code</a>.
Written by Michael Zhang.
<a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source</a>.
</p>
</footer>

View file

@ -4,31 +4,31 @@ import { Content as ShortBio } from "../content/partials/shortBio.md";
import links from "../data/links";
import { Image } from "astro:assets";
import portrait from "../assets/self.png";
// const target = Astro.url.pathname === "/" ? "/about/" : "/";
const target = "/";
---
<nav class="side-nav">
<div class="side-nav-content">
<a href={target} class="portrait" data-astro-prefetch>
<Image src={portrait} alt="portrait" class="portrait" width={350} height={350} loading="eager" />
<a href="/" class="portrait">
<Image src={portrait} alt="portrait" class="portrait" />
</a>
<div class="me">
<div class="titleContainer">
<h1 class="title">
<a href={target} data-astro-prefetch>Michael Zhang</a>
</h1>
</div>
<h1 class="title">Michael Zhang</h1>
<div class="links">
<a href="/about/">About</a>
{
links.map((link) => {
return (
<a href={link.url} title={link.description}>
{link.name}
</a>
);
})
}
</div>
</div>
<div class="bio">
<ShortBio />
<a href="/about/">More &raquo;</a>
<a href="/about">More &raquo;</a>
</div>
</div>
</nav>

View file

@ -59,7 +59,7 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
<tr class="row">
<td>
<div class="title">
<a href={`${basePath}/${post.id}/`} class="brand-colorlink">
<a href={`${basePath}/${post.slug}/`} class="brand-colorlink">
{post.data.title}
</a>
</div>
@ -79,7 +79,7 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
<style lang="scss">
.postListing {
width: 100%;
border-spacing: 0px 24px;
border-spacing: 6px 24px;
:global(.timestamp) {
font-family: var(--monofont);

View file

@ -8,7 +8,7 @@ const { extraFront, tags, extraBack } = Astro.props;
{extraFront}
{
tags.toSorted().map((tag: string) => (
<a href={`/tags/${tag}/`} class="tag">
<a href={`/tags/${tag}`} class="tag">
<i class="fa fa-tag" aria-hidden="true" />
<span class="text">#{tag}</span>
</a>

View file

@ -1,5 +1,5 @@
// Place any global data in this file.
// You can import this data from anywhere in your site by using the `import` keyword.
export const SITE_TITLE = "Michael's Blog";
export const SITE_DESCRIPTION = "Michael's Blog";
export const SITE_TITLE = "Astro Blog";
export const SITE_DESCRIPTION = "Welcome to my website!";

View file

@ -1,8 +1,7 @@
import { defineCollection, z } from "astro:content";
import { glob, file } from "astro/loaders";
const posts = defineCollection({
loader: glob({ pattern: ["**/*.md", "**/*.mdx"], base: "./src/posts" }),
type: "content",
// Type-check frontmatter using a schema
schema: ({ image }) =>

View file

@ -1,5 +1,15 @@
I'm a computer science master's student at the [University of Minnesota][1], advised by [Favonia].
My current research is in programming languages and formal methods, specifically cubical type theory and synthetic homotopy theory.
My current research is cubical type theory and its applications to formalizing some results in algebraic topology.
I also work as a researcher for [SIFT], specializing in compilers and binary analysis. Previously I worked as a software engineer at [Swoop Search] and [AWS].
Before that, I was a CTF hobbyist. I created [EasyCTF], a cybersecurity competition for high schoolers.
I also briefly played with the CTF team [Project Sekai][pjsk].
[1]: https://twin-cities.umn.edu/
[Swoop Search]: https://swoopsrch.com/
[aws]: https://aws.amazon.com/
[sift]: https://www.sift.net/
[favonia]: https://favonia.org/
[easyctf]: https://www.easyctf.com/
[pjsk]: https://sekai.team/

View file

@ -85,6 +85,6 @@ then calling something like `instance.verify()` should run all those validators
## Conclusion
This project is a work in progress! You can see how far I am [on Github](https://github.com/mzhang28/wtforms).
This project is a work in progress! You can see how far I am [on Github](https://github.com/iptq/wtforms).
[1]: https://docs.rs/serde

View file

@ -73,7 +73,7 @@ all of the objects except the two flag halves.
[blender]: https://www.blender.org
![Hiding blender objects](./blender-objects.png)
![Hiding blender objects](../../../assets/ctf/blender-objects.png)
This reveals two QR codes that can be combined into the flag.

View file

@ -1,6 +1,6 @@
---
title: "Dependent Types from First Principles"
id: "dependent-types"
slug: "dependent-types"
date: 2022-10-27
tags: ["type-theory"]
toc: true

View file

@ -1,6 +1,6 @@
---
title: "Formally proving true ≢ false in Homotopy Type Theory with Agda"
id: "proving-true-from-false"
slug: "proving-true-from-false"
date: 2023-04-21
tags: ["type-theory", "agda"]
math: true

View file

@ -1,6 +1,6 @@
---
title: "Equivalences"
id: "equivalences"
slug: "equivalences"
date: 2023-05-06
tags:
- type-theory

View file

Before

Width:  |  Height:  |  Size: 984 KiB

After

Width:  |  Height:  |  Size: 984 KiB

View file

Before

Width:  |  Height:  |  Size: 62 KiB

After

Width:  |  Height:  |  Size: 62 KiB

View file

Before

Width:  |  Height:  |  Size: 25 KiB

After

Width:  |  Height:  |  Size: 25 KiB

View file

Before

Width:  |  Height:  |  Size: 190 KiB

After

Width:  |  Height:  |  Size: 190 KiB

View file

Before

Width:  |  Height:  |  Size: 630 KiB

After

Width:  |  Height:  |  Size: 630 KiB

View file

Before

Width:  |  Height:  |  Size: 1.8 MiB

After

Width:  |  Height:  |  Size: 1.8 MiB

View file

@ -1,6 +1,6 @@
---
title: "Path induction: a GADT perspective"
id: 2023-10-23-path-induction-gadt-perspective
slug: 2023-10-23-path-induction-gadt-perspective
date: 2023-10-23
tags: ["type-theory", "pl-theory"]
---

View file

Before

Width:  |  Height:  |  Size: 704 KiB

After

Width:  |  Height:  |  Size: 704 KiB

View file

Before

Width:  |  Height:  |  Size: 25 KiB

After

Width:  |  Height:  |  Size: 25 KiB

View file

Before

Width:  |  Height:  |  Size: 37 KiB

After

Width:  |  Height:  |  Size: 37 KiB

View file

Before

Width:  |  Height:  |  Size: 37 KiB

After

Width:  |  Height:  |  Size: 37 KiB

View file

Before

Width:  |  Height:  |  Size: 46 KiB

After

Width:  |  Height:  |  Size: 46 KiB

View file

Before

Width:  |  Height:  |  Size: 44 KiB

After

Width:  |  Height:  |  Size: 44 KiB

View file

Before

Width:  |  Height:  |  Size: 34 KiB

After

Width:  |  Height:  |  Size: 34 KiB

View file

Before

Width:  |  Height:  |  Size: 44 KiB

After

Width:  |  Height:  |  Size: 44 KiB

View file

Before

Width:  |  Height:  |  Size: 99 KiB

After

Width:  |  Height:  |  Size: 99 KiB

View file

Before

Width:  |  Height:  |  Size: 478 KiB

After

Width:  |  Height:  |  Size: 478 KiB

View file

Before

Width:  |  Height:  |  Size: 28 KiB

After

Width:  |  Height:  |  Size: 28 KiB

View file

Before

Width:  |  Height:  |  Size: 2.4 MiB

After

Width:  |  Height:  |  Size: 2.4 MiB

View file

@ -1,6 +1,6 @@
---
title: "Agda syntax highlighting in my blog!"
id: 2024-06-26-agda-rendering
slug: 2024-06-26-agda-rendering
date: 2024-06-27T04:25:15.332Z
tags: ["meta", "agda"]
---

View file

@ -1,6 +1,6 @@
---
title: Boolean equivalences
id: 2024-06-28-boolean-equivalences
title: "Boolean equivalences in HoTT"
slug: 2024-06-28-boolean-equivalences
date: 2024-06-28T21:37:04.299Z
tags: ["agda", "type-theory", "hott"]
---
@ -32,7 +32,7 @@ open Σ
With just that notation, the problem may not be clear.
$2$ represents the set with only two elements in it, which is the booleans. The
elements of $2$ are $\mathsf{true}$ and $\mathsf{false}$.
elements of $2$ are $\textrm{true}$ and $\textrm{false}$.
```
data 𝟚 : Set where
@ -53,8 +53,8 @@ shown by Theorem 4.1.3 in the [HoTT book][book].
[1]: https://en.wikipedia.org/wiki/Homotopy#Homotopy_equivalence
- there exists a $g : B \rightarrow A$
- $f \circ g$ is homotopic to the identity map $\mathsf{id}_B : B \rightarrow B$
- $g \circ f$ is homotopic to the identity map $\mathsf{id}_A : A \rightarrow A$
- $f \circ g$ is homotopic to the identity map $\textrm{id}_B : B \rightarrow B$
- $g \circ f$ is homotopic to the identity map $\textrm{id}_A : A \rightarrow A$
We can write this in Agda like this:
@ -92,7 +92,7 @@ function along with proof of its equivalence properties using a dependent
pair[^dependent-pair]:
[^dependent-pair]: A dependent pair (or $\Sigma$-type) is like a regular pair $\langle x, y\rangle$, but where $y$ can depend on $x$.
For example, $\langle x , \mathsf{isPrime}(x) \rangle$.
For example, $\langle x , \textrm{isPrime}(x) \rangle$.
In this case it's useful since we can carry the equivalence information along with the function itself.
This type is rather core to Martin-Löf Type Theory, you can read more about it [here][dependent-pair].
@ -184,8 +184,8 @@ Now we need another function in the other direction. We can't case-split on
functions, but we can certainly case-split on their output. Specifically, we can
differentiate `id` from `neg` by their behavior when being called on `true`:
- $\mathsf{id}(\mathsf{true}) :\equiv \mathsf{true}$
- $\mathsf{neg}(\mathsf{true}) :\equiv \mathsf{false}$
- $\textrm{id}(\textrm{true}) :\equiv \textrm{true}$
- $\textrm{neg}(\textrm{true}) :\equiv \textrm{false}$
```
g : (𝟚𝟚) → 𝟚
@ -207,7 +207,7 @@ everything to true, since it can't possibly have an inverse.
We'll come back to this later.
First, let's show that $g \circ f \sim \mathsf{id}$. This one is easy, we can
First, let's show that $g \circ f \sim \textrm{id}$. This one is easy, we can
just case-split. Each of the cases reduces to something that is definitionally
equal, so we can use `refl`.
@ -217,7 +217,7 @@ g∘f true = refl
g∘f false = refl
```
Now comes the complicated case: proving $f \circ g \sim \mathsf{id}$.
Now comes the complicated case: proving $f \circ g \sim \textrm{id}$.
> [!admonition: NOTE]
> Since Agda's comment syntax is `--`, the horizontal lines in the code below
@ -235,9 +235,9 @@ module f∘g-case where
f∘g eqv = goal eqv
```
Now our goal is to show that for any equivalence $\mathsf{eqv} : 2 \simeq 2$,
Now our goal is to show that for any equivalence $\textrm{eqv} : 2 \simeq 2$,
applying $f ∘ g$ to it is the same as not doing anything. We can evaluate the
$g(\mathsf{eqv})$ a little bit to give us a more detailed goal:
$g(\textrm{eqv})$ a little bit to give us a more detailed goal:
```
goal2 :
@ -273,27 +273,27 @@ a syntax known as [with-abstraction]:
We can now case-split on $b$, which is the output of calling $f$ on the
equivalence returned by $g$. This means that for the `true` case, we need to
show that $f(b) = \mathsf{booleqv}$ (which is based on `id`) is equivalent to
show that $f(b) = \textrm{bool-eqv}$ (which is based on `id`) is equivalent to
the equivalence that generated the `true`.
Let's start with the `id` case; we just need to show that for every equivalence
$e$ where running the equivalence function on `true` also returned `true`, $e
\equiv f(\mathsf{true})$.
\equiv f(\textrm{true})$.
Unfortunately, we don't know if this is true unless our equivalences are _mere
propositions_, meaning if two functions are identical, then so are their
equivalences.
$$
\mathsf{isProp}(P) :\equiv \prod_{x, y \, : \, P}(x \equiv y)
\textrm{isProp}(P) :\equiv \prod_{x, y: P}(x \equiv y)
$$
<small>Definition 3.3.1 from the [HoTT book][book]</small>
Applying this to $\mathsf{isEquiv}(f)$, we get the property:
Applying this to $\textrm{isEquiv}(f)$, we get the property:
$$
\sum_{f : A → B} \left( \prod_{e_1, e_2 \, : \, \mathsf{isEquiv}(f)} e_1 \equiv e_2 \right)
\sum_{f : A → B} \left( \prod_{e_1, e_2 : \textrm{isEquiv}(f)} e_1 \equiv e_2 \right)
$$
This proof is shown later in the book, so I will use it here directly without proof[^equiv-isProp]:
@ -314,7 +314,7 @@ equivalences must not map both values to a single one.
This way, we can pin the behavior of the function on all inputs by just using
its behavior on `true`, since its output on `false` must be _different_.
We can use a proof that [$\mathsf{true} \not\equiv \mathsf{false}$][true-not-false] that I've shown previously.
We can use a proof that [$\textrm{true} \not\equiv \textrm{false}$][true-not-false] that I've shown previously.
[true-not-false]: https://mzhang.io/posts/proving-true-from-false/

View file

@ -0,0 +1,7 @@
+++
title = "Blog"
weight = 1
[cascade]
type = "posts"
+++

View file

@ -6,18 +6,24 @@ export interface Link {
}
const links: Link[] = [
{
name: "projects",
url: "https://git.mzhang.io/michael",
icon: "gitea",
description: "Check out my public open source projects on Forgejo",
},
{
name: "Matrix",
url: "https://matrix.to/#/@michael:chat.mzhang.io",
icon: "matrix-org",
description: "Come chat with me on Matrix",
},
{
name: "Git",
url: "https://git.mzhang.io",
icon: "gitea",
description: "Check out my public open source projects on Forgejo",
},
{
name: "GitHub",
url: "https://github.com/iptq",
icon: "github",
description: "See a history of my old projects on GitHub",
},
{
name: "Mastodon",
url: "https://fosstodon.org/@mzhang",
@ -36,12 +42,6 @@ const links: Link[] = [
icon: "linkedin",
description: "Connect with me on LinkedIn",
},
{
name: "GitHub",
url: "https://github.com/mzhang28",
icon: "github",
description: "See a history of my old projects on GitHub",
},
];
export default links;

Some files were not shown because too many files have changed in this diff Show more