From cece619ff02ec8f113a6b3df9c3e0a72a65be4d5 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 22 Dec 2023 18:21:29 -0500
Subject: [PATCH] docs: too hard, remove univalent

---
 package.json         |  2 +-
 pnpm-lock.yaml       | 18 +++++++++---------
 src/blog/bye-hott.md |  3 +++
 src/index.md         |  2 +-
 4 files changed, 14 insertions(+), 11 deletions(-)
 create mode 100644 src/blog/bye-hott.md

diff --git a/package.json b/package.json
index 950560a..f0d9a80 100644
--- a/package.json
+++ b/package.json
@@ -1,7 +1,7 @@
 {
   "name": "aya-prover-docs",
   "version": "1.0.0",
-  "packageManager": "pnpm@8.6.12",
+  "packageManager": "pnpm@8.12.1",
   "description": "The documentation site of the Aya prover.",
   "main": "index.js",
   "scripts": {
diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml
index 09dc4de..abc0ef1 100644
--- a/pnpm-lock.yaml
+++ b/pnpm-lock.yaml
@@ -905,8 +905,8 @@ packages:
       - supports-color
     dev: true
 
-  /@vitejs/plugin-vue@4.5.2(vite@5.0.10)(vue@3.3.13):
-    resolution: {integrity: sha512-UGR3DlzLi/SaVBPX0cnSyE37vqxU3O6chn8l0HJNzQzDia6/Au2A4xKv+iIJW8w2daf80G7TYHhi1pAUjdZ0bQ==}
+  /@vitejs/plugin-vue@4.6.0(vite@5.0.10)(vue@3.3.13):
+    resolution: {integrity: sha512-XHuyFdAikWRmHuAd89FOyUGIjrBU5KlxJtyi2hVeR9ySGFxQwE0bl5xAQju/ArMq5azdBivY4d+D2yPKwoYWUg==}
     engines: {node: ^14.18.0 || >=16.0.0}
     peerDependencies:
       vite: ^4.0.0 || ^5.0.0
@@ -1138,8 +1138,8 @@ packages:
     engines: {node: ^6 || ^7 || ^8 || ^9 || ^10 || ^11 || ^12 || >=13.7}
     hasBin: true
     dependencies:
-      caniuse-lite: 1.0.30001570
-      electron-to-chromium: 1.4.615
+      caniuse-lite: 1.0.30001571
+      electron-to-chromium: 1.4.616
       node-releases: 2.0.14
       update-browserslist-db: 1.0.13(browserslist@4.22.2)
     dev: true
@@ -1149,8 +1149,8 @@ packages:
     engines: {node: '>=10'}
     dev: true
 
-  /caniuse-lite@1.0.30001570:
-    resolution: {integrity: sha512-+3e0ASu4sw1SWaoCtvPeyXp+5PsjigkSt8OXZbF9StH5pQWbxEjLAZE3n8Aup5udop1uRiKA7a4utUk/uoSpUw==}
+  /caniuse-lite@1.0.30001571:
+    resolution: {integrity: sha512-tYq/6MoXhdezDLFZuCO/TKboTzuQ/xR5cFdgXPfDtM7/kchBO3b4VWghE/OAi/DV7tTdhmLjZiZBZi1fA/GheQ==}
     dev: true
 
   /ccount@2.0.1:
@@ -1224,8 +1224,8 @@ packages:
       dequal: 2.0.3
     dev: true
 
-  /electron-to-chromium@1.4.615:
-    resolution: {integrity: sha512-/bKPPcgZVUziECqDc+0HkT87+0zhaWSZHNXqF8FLd2lQcptpmUFwoCSWjCdOng9Gdq+afKArPdEg/0ZW461Eng==}
+  /electron-to-chromium@1.4.616:
+    resolution: {integrity: sha512-1n7zWYh8eS0L9Uy+GskE0lkBUNK83cXTVJI0pU3mGprFsbfSdAc15VTFbo+A+Bq4pwstmL30AVcEU3Fo463lNg==}
     dev: true
 
   /entities@4.5.0:
@@ -1730,7 +1730,7 @@ packages:
       '@docsearch/css': 3.5.2
       '@docsearch/js': 3.5.2(@algolia/client-search@4.22.0)(search-insights@2.13.0)
       '@types/markdown-it': 13.0.7
-      '@vitejs/plugin-vue': 4.5.2(vite@5.0.10)(vue@3.3.13)
+      '@vitejs/plugin-vue': 4.6.0(vite@5.0.10)(vue@3.3.13)
       '@vue/devtools-api': 6.5.1
       '@vueuse/core': 10.7.0(vue@3.3.13)
       '@vueuse/integrations': 10.7.0(focus-trap@7.5.4)(vue@3.3.13)
diff --git a/src/blog/bye-hott.md b/src/blog/bye-hott.md
new file mode 100644
index 0000000..1f0a06e
--- /dev/null
+++ b/src/blog/bye-hott.md
@@ -0,0 +1,3 @@
+# Moving away from univalent type theory
+
+
diff --git a/src/index.md b/src/index.md
index c2bea16..bea2568 100644
--- a/src/index.md
+++ b/src/index.md
@@ -7,7 +7,7 @@ titleTemplate: A proof assistant designed for formalizing math and type-directed
 hero:
   name: Aya Prover
   text:
-  tagline: A univalent proof assistant designed for formalizing math and type-directed programming.
+  tagline: A proof assistant designed for formalizing math and type-directed programming.
 
   # actions:
   #   - theme: brand