blog: fix table

aya/blog/tt-in-tt-qiit.aya.md

@@ -29,6 +29,16 @@ open inductive Con : Type
 | infix ▷ (Γ : Con) (Ty Γ)
 ```
 
+An instance of the type `Con`{} corresponds to the $Γ$ in the judgment $Γ~\text{ctx}$, and these constructors correspond (on-the-nose) to:
+
+$$
+\cfrac{}{·~\text{ctx}}
+\quad
+\cfrac{Γ~\text{ctx} \quad Γ⊢A~\text{type}}{Γ\mathrel{▷}A~\text{ctx}}
+$$
+
+It uses the judgment $Γ⊢A~\text{type}$, which is defined below.
+
 ## Types
 
 ```aya
@@ -54,6 +64,21 @@ def ext {Γ Δ : Con} (δ : Γ << Δ) (A : Ty Δ) : Γ ▷ Subst A δ << Δ ▷
   δ ∘ π₁ (id refl) ∷ transport (Tm _) SubAss (π₂ (id refl))
 ```
 
+An instance of the type `Ty Γ` corresponds to the $A$ in the judgment $Γ⊢A~\text{type}$. The constructor `U`{} corresponds to the following rule:
+
+$$
+\cfrac{}{Γ⊢\mathcal{U}~\text{type}}
+$$
+
+I believe you already know how `Π`{} works.
+The constructor `El`{} computes the type corresponds to an instance of `U`{}:
+
+$$
+\cfrac{Γ⊢A:\mathcal{U}}{Γ⊢\text{El}(A)~\text{type}}
+$$
+
+Note that it uses the judgment $Γ⊢A:\mathcal{U}$, which is defined below.
+
 ## Substitution objects
 
 ```aya

src/guide/index.md

@@ -11,10 +11,14 @@ Aya is a programming language _and_ an interactive proof assistant designed for
 The type system of Aya has the following highlights:
 
 + 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].
++ Overlapping and order-independent pattern matching makes simple functions compute better,
++ Practical functional programming features similar to [Haskell] and [Idris]: dependent pattern matching, typed holes, enchanted synthesis of implicit arguments.
 
-<!-- Aya is under active development. Please be patient until future information is available. -->
+The implementation of the Aya compiler has the following highlights:
+
++ Efficient type checking by JIT-compiling well-typed definitions to JVM higher-order abstract syntax, so substitution does not traverse terms,
++ Convenient interactive tools such as a language server for VSCode, a REPL, and hyperlinked document generation ([demo](../blog/tt-in-tt-qiit)),
++ Pre-compiled binary release.
 
 [Arend]: https://arend-lang.github.io
 [redtt]: https://redprl.org

src/guide/install.md

@@ -17,7 +17,7 @@ If you chose the jlink version, the `bin` folder contains the executable scripts
 Aya is available for Windows, Linux, and macOS, as listed below.
 
 |         | 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] |

src/index.md

@@ -2,7 +2,6 @@
 layout: home
 
 title: Aya Prover
-titleTemplate: A proof assistant designed for formalizing math and type-directed programming
 
 hero:
   name: Aya Prover