guide: change more univalent things to set-level

aya/guide/haskeller-tutorial.aya.md

@@ -251,7 +251,7 @@ There is a famous example of dependent types in Haskell -- the sized vector type
 ```haskell
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE DataKinds #-}
--- Maybe you need more, but I don't recall. Sorry.
+-- Maybe you need more, I don't remember exactly
 
 data Vec :: Nat -> Type -> Type where
   Nil :: Vec Zero a

package.json

@@ -27,12 +27,12 @@
   "devDependencies": {
     "@types/markdown-it-footnote": "^3.0.4",
     "@vitejs/plugin-vue-jsx": "^3.1.0",
-    "vitepress": "1.0.0-rc.45",
-    "vue": "^3.4.21"
+    "vitepress": "1.2.2",
+    "vue": "^3.4.27"
   },
   "pnpm": {
     "overrides": {
-      "katex": "^0.16.9"
+      "katex": "^0.16.10"
     },
     "peerDependencyRules": {
       "ignoreMissing": [

src/.vitepress/pubs.ts

@@ -22,6 +22,11 @@ export const publications: Publications = [
   {
     type: 'Notes',
     items: [
+      {
+        title: '(Co)conditions hit the path',
+        authors: [teslaZhang],
+        links: [['arxiv', '2405.12994']],
+      },
       {
         title: 'Two tricks to trivialize higher-indexed families',
         authors: [teslaZhang],

src/guide/index.md

@@ -9,9 +9,9 @@
 
 Aya is a programming language _and_ an interactive proof assistant designed for type-directed programming _and_ formalizing math.
 
-The type system of Aya features in the following:
+The type system of Aya has the following highlights:
 
-+ Univalent features similar to Cubical [Agda], [redtt], and [Arend],
++ Set-level cubical features so `funExt` and quotients are available without axioms (like [Agda], [redtt], and [Arend] but not higher-dimensional),
 + Overlapping and order-independent pattern matching,
 + Practical functional programming features similar to [Haskell] and [Idris].
 

src/guide/project-tutorial.md

@@ -5,7 +5,7 @@ and a `src` directory for source code. Here's a sample `aya.json`:
 
 ```json
 {
-  "ayaVersion": "0.23",
+  "ayaVersion": "0.30",
   // ^ The version of Aya you are using -- for compatibility checks
   "name": "<project name>",
   "version": "<project version>",

src/pubs/index.md

@@ -1,6 +1,6 @@
 # Publications
 
-This is a list of publications about Aya by the Aya developers.
+This is a list of publications related to Aya by the Aya developers.
 
 <script setup lang="ts">
 import {publications} from '/.vitepress/pubs'