blog: some fixes

aya/blog/extended-pruning.aya.md

@@ -1,10 +1,15 @@
 # Extended pruning for pattern unification
 
+```aya
+prim I
+prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
+```
+
 The vanilla pattern unification is very limited.
 Consider:
 
 ```aya-hidden
-prim I prim coe prim Path
+prim coe
 variable A B : Type
 def infix = (a b : A) => Path (\i => A) a b
 def refl {a : A} : a = a => fn i => a
@@ -80,11 +85,11 @@ Note that the `i : I` binding is in-scope. So the metavariables with their spine
 Γ ­⊢ Path (fn i => Vec (+-assoc {?a Γ i} {?b Γ i} {?c Γ i} i) Nat) vecA vecB
 ```
 
-Then, we get the following tycking problems, according to the rules of PathP:
+Then, we get the following tycking problems, according to the rules of `Path`{}:
 
 ```
 vecA : Vec (+-assoc {?a Γ 0} {?b Γ 0} {?c Γ 0} 0) Nat
-vecB : Vec (+-assoc {?a Γ 1} {?b Γ 1} {?c Γ 1} 0) Nat
+vecB : Vec (+-assoc {?a Γ 1} {?b Γ 1} {?c Γ 1} 1) Nat
 ```
 
 Look at the spines of all of these metavariables. None of them are in pattern fragment.

package.json

@@ -27,7 +27,7 @@
   "devDependencies": {
     "@types/markdown-it-footnote": "^3.0.4",
     "@vitejs/plugin-vue-jsx": "^4.0.0",
-    "vitepress": "1.2.2",
+    "vitepress": "1.2.3",
     "vue": "^3.4.27"
   },
   "pnpm": {

src/.vitepress/config.mts

@@ -47,7 +47,7 @@ export default defineConfig({
           { text: 'Farewell, Univalence', link: '/blog/bye-hott' },
           { text: 'Inductive Props', link: '/blog/ind-prop' },
           { text: 'Def. projection in classes', link: '/blog/class-defeq' },
-          { text: 'Path constructor elaboration', link: '/blog/pathcon-elab' },
+          { text: 'Path cons. elaboration', link: '/blog/pathcon-elab' },
           { text: 'Path type elaboration', link: '/blog/path-elab' },
           { text: 'Binary operators', link: '/blog/binops' },
           { text: 'Index unification', link: '/blog/index-unification' },

src/.vitepress/readings.ts

@@ -158,7 +158,7 @@ export const readings: Publications = [
   },
 
   {
-    type: 'Univalent Type Theory',
+    type: 'Equality in Type Theory',
     items: [
       {
         title: 'Separating Path and Identity Types in Presheaf Models of Univalent Type Theory',

src/guide/fake-literate.md

@@ -4,7 +4,6 @@ The Aya compiler generates styled (e.g. with colors and text attributes)
 code snippets for many targets, like HTML, LaTeX, etc.,
 and it's tempting to use the same tool but for different languages.
 This is what the _fake literate_ mode is for.
-Right now it only targets LaTeX, but it can be extended to other languages.
 Let me know if you want other backend supports.
 
 To start, install the latest version of Aya, put the following code in a file named `hello.flcl`:

src/guide/install.md

@@ -16,21 +16,15 @@ If you chose the jlink version, the `bin` folder contains the executable scripts
 
 Aya is available for Windows, Linux, and macOS, as listed below.
 
-| Platform | Architecture | JLink                    | Native               |
-|----------|--------------|--------------------------|----------------------|
-| Windows  | x64          | [zip][win-zip-x64]       | [exe][win-exe-x64]   |
-| Linux    | x64          | [zip][linux-zip-x64]     | [exe][linux-exe-x64] |
-| macOS    | x64          | [zip][macos-zip-x64]     | [exe][macos-exe-x64] |
-| Windows  | aarch64      | [zip][win-zip-aarch64]   | Unavailable yet      |
-| Linux    | aarch64      | [zip][linux-zip-aarch64] | Unavailable yet      |
-| macOS    | aarch64      | [zip][macos-zip-aarch64] | Unavailable yet      |
+|         | x64                  | aarch64                  |
+|         |--------------------==|--------------------------|
+| Windows | [zip][win-zip-x64]   | [zip][win-zip-aarch64]   |
+| Linux   | [zip][linux-zip-x64] | [zip][linux-zip-aarch64] |
+| macOS   | [zip][macos-zip-x64] | [zip][macos-zip-aarch64] |
 
 [win-zip-x64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_jlink_windows-x64.zip
-[win-exe-x64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_native_windows-x64.exe
 [linux-zip-x64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_jlink_linux-x64.zip
-[linux-exe-x64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_native_linux-x64
 [macos-zip-x64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_jlink_macos-x64.zip
-[macos-exe-x64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_native_macos-x64
 
 [win-zip-aarch64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_jlink_windows-aarch64.zip
 [linux-zip-aarch64]: https://github.com/aya-prover/aya-dev/releases/download/nightly-build/aya-prover_jlink_linux-aarch64.zip
@@ -81,8 +75,8 @@ You can find the complete example [here][aya-action-example].
 Very cool! Now you can try the prebuilt jars (much smaller and platform-independent)
 or build Aya from source.
 
-We will always be using the latest release of Java.
-Not that we do not stay on LTS releases.
+We will (hopefully) always be using the latest release of Java, rather than LTS,
+unless there are breaking changes on the byte code format.
 
 ### Prebuilt binary