commit 038f34057b7c43781c4593a7fb782d1bb202344f Author: rhi Date: Mon Jul 31 18:54:32 2023 -0400 Update 'Home' diff --git a/Home.md b/Home.md new file mode 100644 index 0000000..dced207 --- /dev/null +++ b/Home.md @@ -0,0 +1,5 @@ +\*quox noise* + +## misc notes + +- [[agda w-type stuff]] \ No newline at end of file