diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml
index dc7d2f3ce..93476dca8 100644
--- a/.github/workflows/mkdocs.yml
+++ b/.github/workflows/mkdocs.yml
@@ -2,7 +2,7 @@ name: MKDocs
on:
push:
- branches: [develop]
+ branches: [develop,mkdocs-*]
tags: [v*]
paths:
- .github/workflows/mkdocs.yml
@@ -37,6 +37,12 @@ jobs:
rename-to: rzk
chmod: 0755
+ - name: Check Rzk files for each language
+ run:
+ for lang_dir in $(ls -d docs/docs/*/); do
+ pushd ${lang_dir} && rzk typecheck; popd ;
+ done
+
- name: 🔨 Install MkDocs Material and mike
run: pip install -r docs/requirements.txt
@@ -46,11 +52,16 @@ jobs:
git config --local user.name "github-actions[bot]"
- name: 🚀 Deploy with mike (${{ github.ref_name }}, latest)
- if: ${{ github.ref_name != 'develop' }}
+ if: ${{ github.ref_name != 'develop' && !startsWith(github.ref_name, 'mkdocs') }}
run: |
- mike deploy --push --update-aliases --config-file docs/mkdocs.yml ${{ github.ref_name }} latest
+ for config in $(ls docs/config/*/mkdocs.yml); do
+ mike deploy --push --update-aliases --config-file ${config} ${{ github.ref_name }} latest;
+ mike set-default latest --config-file ${config} --push;
+ done
- name: 🚀 Deploy with mike (${{ github.ref_name }})
- if: ${{ github.ref_name == 'develop' }}
+ if: ${{ github.ref_name == 'develop' || startsWith(github.ref_name, 'mkdocs') }}
run: |
- mike deploy --push --config-file docs/mkdocs.yml ${{ github.ref_name }}
+ for config in $(ls docs/config/*/mkdocs.yml); do
+ mike deploy --push --config-file ${config} ${{ github.ref_name }};
+ done
diff --git a/.gitignore b/.gitignore
index 27563190a..e98831350 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,7 @@
+.cache/
.DS_Store
docs/out/
+docs/generated/
dist
dist-*
cabal-dev
@@ -33,4 +35,4 @@ __pycache__
*.fls
*.log
rzk/doc/
-/rzk-playground-release
\ No newline at end of file
+/rzk-playground-release
diff --git a/docs/docs/CONTRIBUTORS.md b/CONTRIBUTORS.md
similarity index 100%
rename from docs/docs/CONTRIBUTORS.md
rename to CONTRIBUTORS.md
diff --git a/docs/config/base.yml b/docs/config/base.yml
new file mode 100644
index 000000000..268094881
--- /dev/null
+++ b/docs/config/base.yml
@@ -0,0 +1,66 @@
+repo_url: https://github.com/rzk-lang/rzk
+repo_name: rzk-lang/rzk
+
+theme:
+ name: material
+ custom_dir: '../../overrides/'
+ favicon: assets/images/favicon.png
+ logo: assets/images/logo-1000x1000.png
+ icon:
+ repo: fontawesome/brands/github
+ edit: material/pencil
+ view: material/eye
+ features:
+ - content.code.copy
+ - content.action.edit
+ - navigation.footer
+ - navigation.tabs
+ - navigation.tabs.sticky
+ - navigation.sections
+ - navigation.prune
+ - navigation.path
+ - toc.integrate
+
+extra_javascript:
+ - javascript/mathjax.js
+ - https://polyfill.io/v3/polyfill.min.js?features=es6
+ - https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js
+
+extra_css:
+ - https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.16.7/katex.min.css
+ - https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.7.0/styles/default.min.css
+ - assets/css/rzk-render.css
+
+markdown_extensions:
+ - admonition
+ - footnotes
+ - pymdownx.details
+ - pymdownx.snippets:
+ base_path:
+ - .
+ - ..
+ check_paths: true
+ - mdx_math
+ - pymdownx.highlight:
+ anchor_linenums: true
+ line_spans: __span
+ pygments_lang_class: true
+ - pymdownx.inlinehilite
+ - pymdownx.snippets
+ - pymdownx.superfences
+ - toc:
+ permalink: true
+ - pymdownx.arithmatex:
+ generic: true
+ - attr_list
+
+extra:
+ version:
+ provider: mike
+ alternate:
+ - name: English
+ link: /rzk/en/
+ lang: en
+ - name: Русский
+ link: /rzk/ru/
+ lang: ru
diff --git a/docs/config/en/mkdocs.yml b/docs/config/en/mkdocs.yml
new file mode 100644
index 000000000..debe30b38
--- /dev/null
+++ b/docs/config/en/mkdocs.yml
@@ -0,0 +1,72 @@
+INHERIT: "../base.yml"
+site_name: "Rzk proof assistant"
+site_description: "An experimental proof assistant for simplicial type theory and synthetic ∞-categories."
+site_author: "Nikolai Kudasov"
+docs_dir: '../../docs/en'
+site_dir: '../../generated/en'
+edit_uri: edit/develop/docs/docs/en/
+
+nav:
+ - Home:
+ - About: index.md
+ - Community: community.md
+ - Tools: tools.md
+ - Contributors: CONTRIBUTORS.md
+ - Changelog: CHANGELOG.md
+ - Getting Started:
+ - Install: getting-started/install.md
+ - Quickstart: getting-started/quickstart.rzk.md
+ - Depedent Types: getting-started/dependent-types.rzk.md
+ - Setting up an Rzk project: getting-started/project.md
+ - Reference:
+ - Introduction: reference/introduction.rzk.md
+ - Cube layer: reference/cube-layer.rzk.md
+ - Tope layer: reference/tope-layer.rzk.md
+ - Dependent types: reference/type-layer.rzk.md
+ - Tope disjunction elimination: reference/tope-disjunction-elimination.rzk.md
+ - Extension types: reference/extension-types.rzk.md
+ - Organizational features:
+ - Sections and Variables: reference/sections.rzk.md
+ - Builtins:
+ - Directed interval: reference/builtins/directed-interval.rzk.md
+ - Unit type: reference/builtins/unit.rzk.md
+ - Commands:
+ - Define and Postulate: reference/commands/define-postulate.rzk.md
+ - Compute: reference/commands/compute.rzk.md
+ - Check: reference/commands/check.rzk.md
+ - Options: reference/commands/options.rzk.md
+ - Other:
+ - Rendering Diagrams: reference/render.rzk.md
+ - Examples:
+ - Weak tope disjunction elimination: examples/recId.rzk.md
+ - Playground: playground/index.html
+
+theme:
+ language: en
+ font:
+ text: Inria Sans
+ palette:
+ # Palette toggle for light mode
+ - media: "(prefers-color-scheme: light)"
+ primary: white
+ scheme: default
+ toggle:
+ icon: material/brightness-7
+ name: "Switch to dark mode"
+ # Palette toggle for dark mode
+ - media: "(prefers-color-scheme: dark)"
+ primary: black
+ scheme: slate
+ toggle:
+ icon: material/brightness-4
+ name: "Switch to light mode"
+
+plugins:
+ - social
+ - mike:
+ deploy_prefix: 'en/'
+ - search:
+ lang: en
+ - rzk:
+ render_svg: true
+ anchor_definitions: true
diff --git a/docs/config/ru/mkdocs.yml b/docs/config/ru/mkdocs.yml
new file mode 100644
index 000000000..ad3295fed
--- /dev/null
+++ b/docs/config/ru/mkdocs.yml
@@ -0,0 +1,73 @@
+INHERIT: "../base.yml"
+site_url: https://rzk-lang.github.io/rzk/ru/
+site_name: "Решатель теорем Rzk"
+site_description: "Экспериментальный решатель теорем для симплициальной теории типов и синтетических ∞-категорий."
+site_author: "Николай Кудасов"
+docs_dir: '../../docs/ru'
+site_dir: '../../generated/ru'
+edit_uri: edit/develop/docs/docs/ru/
+
+nav:
+ - Главная:
+ - О проекте: index.md
+ - Сообщество: community.md
+ - Инструменты: tools.md
+ - Участники (англ.): CONTRIBUTORS.md
+ - История изменений (англ.): CHANGELOG.md
+ - Первые шаги:
+ - Установка: getting-started/install.md
+ - Быстрое начало: getting-started/quickstart.rzk.md
+ - Введение в зависимые типы: getting-started/dependent-types.rzk.md
+ - Настройка проекта: getting-started/project.md
+ - Руководство:
+ - Введение: reference/introduction.rzk.md
+ - Слой кубов: reference/cube-layer.rzk.md
+ - Слой форм: reference/tope-layer.rzk.md
+ - Зависимые типы: reference/type-layer.rzk.md
+ - Устранение объединений форм: reference/tope-disjunction-elimination.rzk.md
+ - Типы-расширения: reference/extension-types.rzk.md
+ - Организация кода:
+ - Разделы и предпосылки: reference/sections.rzk.md
+ - Встроенные определения:
+ - Направленный интервал: reference/builtins/directed-interval.rzk.md
+ - Единичный тип: reference/builtins/unit.rzk.md
+ - Команды:
+ - Определения и постулаты: reference/commands/define-postulate.rzk.md
+ - Вычисления: reference/commands/compute.rzk.md
+ - Проверка типов: reference/commands/check.rzk.md
+ - Опции решателя: reference/commands/options.rzk.md
+ - Другое:
+ - Отрисовка диаграм: reference/render.rzk.md
+ - Примеры:
+ - Слабое устранение объединений форм: examples/recId.rzk.md
+ - Песочница: playground/index.html
+
+theme:
+ language: ru
+ font:
+ text: PT Sans
+ palette:
+ # Palette toggle for light mode
+ - media: "(prefers-color-scheme: light)"
+ primary: white
+ scheme: default
+ toggle:
+ icon: material/brightness-7
+ name: "Переключить на тёмный режим"
+ # Palette toggle for dark mode
+ - media: "(prefers-color-scheme: dark)"
+ primary: black
+ scheme: slate
+ toggle:
+ icon: material/brightness-4
+ name: "Переключить на светлый режим"
+
+plugins:
+ - social
+ - mike:
+ deploy_prefix: 'ru/'
+ - search:
+ lang: ru
+ - rzk:
+ render_svg: true
+ anchor_definitions: true
diff --git a/docs/docs/CHANGELOG.md b/docs/docs/CHANGELOG.md
deleted file mode 100644
index 3d1ab925c..000000000
--- a/docs/docs/CHANGELOG.md
+++ /dev/null
@@ -1,326 +0,0 @@
-# Changelog for `rzk`
-
-All notable changes to this project will be documented in this file.
-
-The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
-and this project adheres to the
-[Haskell Package Versioning Policy](https://pvp.haskell.org/).
-
-## v0.7.1 — 2023-12-08
-
-- Fix default build to include Rzk Language Server (`rzk lsp`) (see [`9b78a15`](https://github.com/rzk-lang/rzk/commit/9b78a15c750699afa93c4dab3735c2aa31e6faac));
-- Apply formatting to `recId.rzk.md` example (see [`4032724`](https://github.com/rzk-lang/rzk/commit/40327246954332f40cd82c48d102bf4257ad719e));
-
-## v0.7.0 — 2023-12-08
-
-Major changes:
-
-- Add an experimental `rzk format` command (by [Abdelrahman Abounegm](https://github.com/aabounegm), with feedback by [Fredrik Bakke](https://github.com/fredrik-bakke) (see [sHoTT#142](https://github.com/rzk-lang/sHoTT/pull/142)) and [Nikolai Kudasov](https://github.com/fizruk)):
- - Automatically format files, partially automating the [Code Style of the sHoTT project](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/)
- - Notable features:
- - Adds a space after the opening parenthesis to help with the [code tree structure](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/#the-tree-structure-of-constructions)
- - Puts the definition conclusion (type, starting with `:`) and construction (body, starting with `:=`) on new lines
- - Adds a space after the `\` of a lambda term and around binary operators (like `,`)
- - Moves binary operators to the beginning of the next line if they appear at the end of the previous one.
- - Replaces [common ASCII sequences](https://rzk-lang.github.io/sHoTT/STYLEGUIDE/#use-of-unicode-characters) with their Unicode equivalent
- - A CLI subcommand (`rzk format`) with `--check` and `--write` options
- - Known limitations
- - The 80 character line limit is currently not enforced due to the difficulty of determining where to add line breaks (for reference, check out [this post](https://journal.stuffwithstuff.com/2015/09/08/the-hardest-program-ive-ever-written/) by a Dart `fmt` engineer)
- - Fixing indentation is not yet implemented due to the need for more semantics than the lexer provides to determine indentation level.
- - There may be rare edge cases in which applying the formatter twice could result in additional edits that were not detected the first time.
-
-Minor changes:
-
-- Fix "latest" Rzk Playground link (see [#137](https://github.com/rzk-lang/rzk/pull/137));
-- Add more badges to README (see [#136](https://github.com/rzk-lang/rzk/pull/136));
-
-## v0.6.7 — 2023-10-07
-
-- Fix build on some systems (fix `BNFC:bnfc` executable dependency, see [#125](https://github.com/rzk-lang/rzk/pull/125))
-- Improve Rzk Playground (see [#124](https://github.com/rzk-lang/rzk/pull/124) by @deemp):
- - Add `snippet_url` parameter
- - Migrated from NextJS to Vite
- - Use `setText` on `params` attribute
-- Slightly improve documentation:
- - Add links to Rzk Zulip (see [#131](https://github.com/rzk-lang/rzk/pull/131))
- - Add `cabal update` to instructions (see [`3aa8fd3`](https://github.com/rzk-lang/rzk/commit/3aa8fd38902fc8cbb29f86122410d24398a15b0b))
-
-## v0.6.6 — 2023-10-02
-
-- Fix builds on Windows (and macOS) (see [#121](https://github.com/rzk-lang/rzk/pull/121))
-
-## v0.6.5 — 2023-10-01
-
-This version contains mostly intrastructure improvements:
-
-- Typecheck using `rzk.yaml` if it exists (see [#119](https://github.com/rzk-lang/rzk/pull/119))
-- Update Rzk Playground and Nix Flake (see [#84](https://github.com/rzk-lang/rzk/pull/84))
- - Rzk Playground now uses CodeMirror 6 and NextJS
- - `miso` dependency is dropped
- - GHCJS 9.6 is now used
- - Support `snippet={code}` or `code={code}` param (see [#118](https://github.com/rzk-lang/rzk/pull/118))
- - Support for `snippet_url={URL}` is temporarily dropped
-- Update to GHC 9.6, latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see [#116](https://github.com/rzk-lang/rzk/pull/116))
-- Add logging for Rzk Language Server (see [#114](https://github.com/rzk-lang/rzk/pull/114))
-
-Fixes:
-
-- Fix error messages in Rzk Playground (see [#115](https://github.com/rzk-lang/rzk/pull/115))
-
-## v0.6.4 — 2023-09-27
-
-This version improves the stucture of the project, in particular w.r.t dependencies:
-
-- Add custom snapshot and explicit lower bounds (see [#108](https://github.com/rzk-lang/rzk/pull/108))
-
-## v0.6.3 — 2023-09-27
-
-This version contains a fix for the command line interface of `rzk`:
-
-- Fix command line `rzk typecheck` (see [#106](https://github.com/rzk-lang/rzk/pull/106))
-
- - Previous version ignored failures in the command line
- (the bug was introced when allowing better autocompletion in LSP).
-
-## v0.6.2 — 2023-09-26
-
-This version contains some improvements in efficiency and also to the language server:
-
-- Improve efficiency of the tope solver, applying LEM for directed interval only as a fallback option (see [#102](https://github.com/rzk-lang/rzk/pull/102))
-- Support autocompleting definitions from previous modules (see [#102](https://github.com/rzk-lang/rzk/pull/103))
- - Well-typed definitions from the same module also work if the module is only partially well-typed!
-- Improve information order in the error messages given in LSP diagnostics (see [#104](https://github.com/rzk-lang/rzk/pull/104))
-
-## v0.6.1 — 2023-09-24
-
-This version contains a minor fix:
-
-- Catch exceptions in the parser, fixing LSP for files where layout resolver fails (see [#99](https://github.com/rzk-lang/rzk/pull/99)).
-
-## v0.6.0 — 2023-09-23
-
-This version introduces a proper LSP server with basic support for incremental typechecking
-and some minor improvements:
-
-1. LSP server with incremental typechecking (see [#95](https://github.com/rzk-lang/rzk/pull/95));
-2. Improve error messages for unclosed `#section` and extra `#end` (see [#91](https://github.com/rzk-lang/rzk/pull/91)).
-
-## v0.5.7 — 2023-09-21
-
-This version contains two fixes (see [#88](https://github.com/rzk-lang/rzk/pull/88)) for issues discovered in [rzk-lang/sHoTT#30](https://github.com/rzk-lang/sHoTT/pull/30#issuecomment-1729212862):
-
-1. We now only generate well-typed LEM instances in the tope solver, speeding up significantly.
-2. We fix $\eta$-rule for product cubes, to not get stopped by reflexive equality topes like $\langle \langle \pi_1 (t_{12}), \pi_2 (t_{12}) \rangle, t_3 \rangle \equiv \langle t_{12}, t_3 \rangle$.
-
-## v0.5.6 — 2023-09-19
-
-This version fixes the behaviour of glob (see [`77b7cc0`](https://github.com/rzk-lang/rzk/commit/77b7cc0494fe0bfd1c9f1aa83db20f42cfda5794)).
-
-## v0.5.5 — 2023-09-19
-
-This version contains Unicode and tope logic-related fixes:
-
-1. Fix (add missing checks) for subshapes (see [#85](https://github.com/rzk-lang/rzk/pull/85));
-2. Allow to handle wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83));
-3. Fix Unicode on machines with non-standard locales (see [#82](https://github.com/rzk-lang/rzk/pull/82));
-4. Specify `happy` and `alex` as build tools to fix cabal build from Hackage (see [#80](https://github.com/rzk-lang/rzk/pull/80)).
-5. Add configuration for MkDocs plugin for Rzk (see [#79](https://github.com/rzk-lang/rzk/pull/79)).
-
-## v0.5.4 — 2023-08-19
-
-This version contains minor improvements:
-
-1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76));
-2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)).
-
-## v0.5.3 — 2023-07-12
-
-This version contains a few minor improvements:
-
-1. Allow patterns in dependent function types (see [#67](https://github.com/rzk-lang/rzk/pull/67));
-2. Hint about possible shape coercions (see [#67](https://github.com/rzk-lang/rzk/pull/67));
-3. Enable doctests (see [#68](https://github.com/rzk-lang/rzk/pull/68));
-4. Improve documentation (add recommended installation instructions via VS Code)
-5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983));
-6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66));
-
-## v0.5.2 — 2023-07-05
-
-This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit:
-
-- Support some Unicode syntax (see [#61](https://github.com/rzk-lang/rzk/pull/61));
-- Support curly braces syntax for code blocks (see [#64](https://github.com/rzk-lang/rzk/pull/64));
-- Update documentation a bit (see [07b520a6](https://github.com/rzk-lang/rzk/commit/07b520a67eb432105fad908202949c93a1639ca8) and [7cc7f383](https://github.com/rzk-lang/rzk/commit/7cc7f383b1785130277ed79d123c1dd357162d9d));
-- Factor out Pygments highlighting to https://github.com/rzk-lang/pygments-rzk;
-- Use new cache action for Nix (see [#60](https://github.com/rzk-lang/rzk/pull/60)).
-
-## v0.5.1 — 2023-06-29
-
-This version fixes `Unit` type and makes some changes to documentation:
-
-- Fix computation for `Unit` (see [2f7d6295](https://github.com/rzk-lang/rzk/commit/2f7d6295));
-- Update documentation (see [ea2d176b](https://github.com/rzk-lang/rzk/commit/ea2d176b));
-- Use mike to deploy versioned docs (see [99cf721a](https://github.com/rzk-lang/rzk/commit/99cf721a));
-- Replace MkDocs hook with the published plugin (see [#58](https://github.com/rzk-lang/rzk/pull/58));
-- Switch to Material theme for MkDocs (see [#57](https://github.com/rzk-lang/rzk/pull/57));
-- Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b](https://github.com/rzk-lang/rzk/commit/8ba1c55b));
-
-## v0.5 — 2023-06-20
-
-This version contains the following changes:
-
-- `Unit` type (with `unit` value) (see [ede02611](https://github.com/rzk-lang/rzk/commit/ede02611) and [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9);
-- Add basic tokenizer support via `rzk tokenize` (see [#53](https://github.com/rzk-lang/rzk/pull/53));
-- Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9)).
-
-## v0.4.1 — 2023-06-16
-
-This is version contains minor changes, primarily in tools around rzk:
-
-- Add `rzk version` command (see [f1709dc7](https://github.com/rzk-lang/rzk/commit/f1709dc7));
-- Add action to release binaries (see [9286afae](https://github.com/rzk-lang/rzk/commit/9286afae));
-- Automate SVG rendering in MkDocs (see [#49](https://github.com/rzk-lang/rzk/pull/49));
-- Read `stdin` when no filepaths are given (see [936c15a3](https://github.com/rzk-lang/rzk/commit/936c15a3));
-- Add Pygments highlighting (see [01c2a017](https://github.com/rzk-lang/rzk/commit/01c2a017), [cbd656cc](https://github.com/rzk-lang/rzk/commit/cbd656cc), [5220ddf9](https://github.com/rzk-lang/rzk/commit/5220ddf9), [142ec003](https://github.com/rzk-lang/rzk/commit/142ec003), [5c7425f2](https://github.com/rzk-lang/rzk/commit/5c7425f2));
-- Update HighlightJS config for rzk v0.4.0 (see [171ee63f](https://github.com/rzk-lang/rzk/commit/171ee63f));
-
-## v0.4.0 — 2023-05-18
-
-This version introduces sections and variables. The feature is similar to `Variable` command in Coq . An important difference, however, is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental.
-
-- Variables and sections (Coq-style) (see [#38](https://github.com/rzk-lang/rzk/pull/38));
-
-Minor improvements:
-
-- Add flake, set up nix and cabal builds, cache nix store on CI (see [#39](https://github.com/rzk-lang/rzk/pull/39));
-- Apply stylish-haskell (see [7d42ef62](https://github.com/rzk-lang/rzk/commit/7d42ef62));
-
-## v0.3.0 — 2023-04-28
-
-This version introduces an experimental feature for generating visualisations for simplicial terms in SVG.
-To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):
-
-```rzk
-#set-option "render" = "svg" -- enable rendering in SVG
-```
-
-Minor changes:
-
-- Exit with non-zero code upon a type error (see b135c4fb)
-- Fix external links and some typos in the documentation
-
-Fixes:
-
-- Fixed an issue with tope solver when context was empty (see 6196af9e);
-- Fixed #33 (missing coherence check for restricted types).
-
-## v0.2.0 - 2023-04-20
-
-This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0.
-
-### Language
-
-Syntax is almost entirely backwards compatible with version 0.1.0.
-Typechecking has been fixed and improved.
-
-#### Breaking Changes
-
-The only known breaking changes are:
-
-1. Terms like `second x y` which previous have been parsed as `second (x y)`
- now are properly parsed as `(second x) y`.
-2. It is now necessary to have at least a minimal indentation in the definition of a term after a newline.
-3. Unicode syntax is temporarily disabled, except for dependent sums and arrows in function types.
-4. The restriction syntax `[ ... ]` now has a slightly different precedence, so some parentheses are required, e.g. in `(A -> B) [ phi |-> f]` or `(f t = g t) [ phi |-> f]`.
-5. Duplicate top-level definitions are no longer allowed.
-
-#### Deprecated Syntax
-
-The angle brackets for extension types are supported, but deprecated,
-as they are completely unnecessary now: `<{t : I | psi t} -> A t [ phi t |-> a t ]>` can now be written as `{t : I | psi t} -> A t [ phi t |-> a t]`
-or even `(t : psi) -> A t [ phi t |-> a t ]`.
-
-#### Syntax Relaxation
-
-Otherwise, syntax is now made more flexible:
-
-1. Function parameters can be unnamed: `A -> B` is the same as `(_ : A) -> B`.
-2. Angle brackets are now optional: `{t : I | psi t} -> A t [ phi t |-> a t ]`
-3. Nullary extension types are possible: `A t [ phi t |-> a t ]`
-4. Lambda abstractions can introduce multiple arguments:
-
- ```rzk
- #def hom : (A : U) -> A -> A -> U
- := \A x y ->
- (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]
- ```
-
-5. Parameters can be introduced simultaneously for the type and body. Moreover, multiple parameters can be introduced with the same type:
-
- ```rzk
- #def hom (A : U) (x y : A) : U
- := (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]
- ```
-
-6. Restrictions can now support multiple subshapes, effectively internalising `recOR`:
-
- ```rzk
- #def hom (A : U) (x y : A) : U
- := (t : Δ¹) -> A [ t === 0_2 |-> x, t === 1_2 |-> y ]
- ```
-
-7. There are now 3 syntactic versions of `refl` with different amount of explicit annotations:
- `refl`, `refl_{x}` and `refl_{x : A}`
-
-8. There are now 2 syntactic versions of identity types (`=`): `x = y` and `x =_{A} y`.
-
-9. `recOR` now supports alternative syntax with an arbitrary number of subshapes:
- `recOR( tope1 |-> term1, tope2 |-> term2, ..., topeN |-> termN )`
-
-10. Now it is possible to have type ascriptions: `t as T`. This can help with ensuring types of subexpressions in parts of formalisations, or to upcast types.
-
-11. New (better) commands are now supported:
-
- 1. `#define ( )* : := ` — same as `#def`, but with full spelling of the word
- 2. `#postulate ( )* : ` — postulate an axiom
- 3. `#check : ` — typecheck an expression against a given type
- 4. `#compute-whnf ` — compute (WHNF) of a term
- 5. `#compute-nf ` — compute normal form of a term
- 6. `#compute ` — alias for `#compute-whnf`
- 7. `#set-option = ` — set a (typechecker) option:
-
- - `#set-option "verbosity" = "silent"` — no log printing
- - `#set-option "verbosity" = "normal"` — log typechecking progress
- - `#set-option "verbosity" = "debug"` — log every intermediate action
- (may be useful to debug when some definition does not typecheck)
-
- 8. `#unset-option ` — revert option's value to its default
-
-#### Simple Shape Coercions
-
-In some places, shapes (cube indexed tope families) can be used directly:
-
-1. In function parameters: `(Λ -> A) -> (Δ² -> A)` is the same as `({(t, s) : 2 * 2 | Λ (t, s)} -> A) -> ({(t, s) : 2 * 2 | Δ²} -> A)`
-
-2. In parameter types of lambda abstractions: `\((t, s) : Δ²) -> ...` is the same as `\{(t, s) : 2 * 2 | Δ² (t, s)} -> ...`
-
-#### Better Type Inference
-
-1. It is now not required to annotate point variables with tope restrictions, the typechecker is finally smart enough to figure them out from the context.
-
-2. It is now possible to simply write `refl` in most situations.
-
-3. It is now possible to omit the index type in an identity type: `x = y`
-
-### Better output and error message
-
-The output and error messages have been slightly improved, but not in a major way.
-
-### Internal representation
-
-A new internal representation (a version of second-order abstract syntax)
-allows to stop worrying about name captures in substitutions,
-so the implementation is much more trustworthy.
-The new representation will also allow to bring in higher-order unification in the future, for better type inference, matching, etc.
-
-New representation also allowed annotating each (sub)term with its type to avoid recomputations and some other minor speedups. There are still some performance issues, which need to be debugged, but overall it is much faster than version 0.1.0 already.
diff --git a/docs/docs/en/CHANGELOG.md b/docs/docs/en/CHANGELOG.md
new file mode 100644
index 000000000..b9d820ec8
--- /dev/null
+++ b/docs/docs/en/CHANGELOG.md
@@ -0,0 +1 @@
+--8<-- "rzk/ChangeLog.md"
diff --git a/docs/docs/en/CONTRIBUTORS.md b/docs/docs/en/CONTRIBUTORS.md
new file mode 100644
index 000000000..2e25bbd52
--- /dev/null
+++ b/docs/docs/en/CONTRIBUTORS.md
@@ -0,0 +1 @@
+--8<-- "CONTRIBUTORS.md"
diff --git a/docs/docs/community.md b/docs/docs/en/community.md
similarity index 75%
rename from docs/docs/community.md
rename to docs/docs/en/community.md
index 46ab96599..77c5c4a60 100644
--- a/docs/docs/community.md
+++ b/docs/docs/en/community.md
@@ -1,5 +1,7 @@
# Rzk Community
+There is a small community of mathematicians and computer scientists around Rzk.
+
## Chat
A Zulip chat is available for all to join and chat about Rzk, including formalization projects, development of Rzk, and related projects:
diff --git a/docs/docs/examples/recId.rzk.md b/docs/docs/en/examples/recId.rzk.md
similarity index 97%
rename from docs/docs/examples/recId.rzk.md
rename to docs/docs/en/examples/recId.rzk.md
index 94ffcff85..96d780dce 100644
--- a/docs/docs/examples/recId.rzk.md
+++ b/docs/docs/en/examples/recId.rzk.md
@@ -7,6 +7,10 @@ Luckily, assuming relative function extensionality, we can define a weaker versi
## Prerequisites
+This file relies on some definitions, defined in
+
+- [Getting Started > Dependent Types](../getting-started/dependent-types.rzk.md)
+
We begin by introducing common HoTT definitions:
```rzk
@@ -27,11 +31,6 @@ We begin by introducing common HoTT definitions:
: U
:= ( x : A) → (y : A) → isaprop (x =_{A} y)
--- Non-dependent product of A and B
-#define prod (A : U) (B : U)
- : U
- := Σ ( x : A) , B
-
-- A function f : A → B is an equivalence
-- if there exists g : B → A
-- such that for all x : A we have g (f x) = x
diff --git a/docs/docs/en/getting-started/dependent-types.rzk.md b/docs/docs/en/getting-started/dependent-types.rzk.md
new file mode 100644
index 000000000..cfbed328a
--- /dev/null
+++ b/docs/docs/en/getting-started/dependent-types.rzk.md
@@ -0,0 +1,744 @@
+# Dependent types
+
+In this file we will look at Rzk primitives to work with dependent types.
+
+!!! info "Reference material"
+
+ This page is mostly based on the introduction of dependent types in the HoTT Book (Sections 1.2–1.6),
+ immediately introducing corresponding formalizations in Rzk and noting some differences.
+
+This is a literate Rzk file:
+
+```rzk
+#lang rzk-1
+```
+
+## Functions
+
+The type `#!rzk (x : A) → B x` is the type of (dependent)
+functions with an argument of type `A` and, for each input `x`,
+the output type `B x`.
+
+As a simple example of a dependent function,
+consider the identity function:
+
+```rzk
+#define identity
+ : ( A : U) → (x : A) → A
+ := \ A x → x
+```
+
+Since we are not using `x` in the type of `identity`,
+we can simply write the type of the argument,
+without providing its name:
+
+```rzk
+#define identity₁
+ : ( A : U) → A → A
+ := \ A x → x
+```
+
+We can write this definition differently,
+by putting `#!rzk (A : U)` into parameters (before `:`),
+and omitting it in the lambda abstraction:
+
+```rzk
+#define identity₂
+ ( A : U)
+ : A → A
+ := \ x → x
+```
+
+We could also move `x` into parameters as well,
+although this probably does not increase readability anymore:
+
+```rzk
+#define identity₃
+ ( A : U)
+ ( x : A)
+ : A
+ := x
+```
+
+Another, less trivial example of a dependent function is
+the one that swaps the arguments of another function:
+
+```rzk
+#define swap
+ ( A B C : U)
+ : ( A → B → C) → (B → A → C)
+ := \ f → \ b a → f a b
+```
+
+## Product types
+
+Rzk does not have built-in product types, since they are a special case of Σ-types,
+which we will discuss soon. For now, we give definition of product types:
+
+```rzk
+#define prod
+ ( A B : U)
+ : U
+ := Σ ( _ : A) , B
+```
+
+The type `#!rzk prod A B` corresponds to the product type $A \times B$.
+The `#!rzk Unit` type corresponds to the type $\mathbf{1}$.
+
+The intended elements of `#!rzk prod A B` are only pairs `#!rzk (a, b) : prod A B`
+where `#!rzk a : A` and `#!rzk b : B`. Similarly, intended element of `#!rzk Unit`
+is only `#!rzk unit`. However, formally, this is not immediately true and instead
+is a theorem that we can prove.
+
+### Remark on type formers
+
+Formally, we have the following constituents of the definition for product types and function types
+(for comparison):
+
+1. **Type formation**:
+
+ - `#!rzk prod A B` is a type whenever `A` and `B` are types
+ - `#!rzk A → B` is a type whenever `A` and `B` are types
+
+2. **Constructors (introduction rules)**:
+
+ - `#!rzk (x , y)` is a term of type `#!rzk prod A B` whenever `#!rzk x : A` and `#!rzk y : B`
+ - `#!rzk \ x → y` is a term of type `#!rzk A → B` whenever for any `#!rzk x : A` we have `#!rzk y : B`
+
+3. **Eliminators (elimination rules)**:
+
+ - Given `#!rzk z : prod A B`, we can _project_ the first and second components:
+ - `#!rzk first z : A` and `#!rzk second z : B`
+ - it is also possible to pattern match (deconstruct) in a function argument or when introducing a parameter, e.g.
+
+ ```rzk
+ #define swap-prod₁
+ ( A B : U)
+ : prod A B → prod B A
+ := \ (x , y) → (y , x)
+
+ #define swap-prod₂
+ ( A B : U)
+ ( (x , y) : prod A B)
+ : prod B A
+ := ( y , x)
+ ```
+
+ - more generally, eliminators come in a form of an _induction principle_, which we will discuss below
+ and can be defined in Rzk in terms of pattern matching or `#!rzk first` and `#!rzk second`:
+
+ ```rzk
+ #define ind-prod
+ ( A B : U)
+ ( C : prod A B → U)
+ ( f : (a : A) → (b : B) → C (a , b))
+ : (z : prod A B) → C z
+ := \ (a , b) → f a b
+ ```
+
+ - Given `#!rzk f : A → B`, we can _apply_ it to an argument of type `#!rzk a : A`:
+ - `#!rzk f a : B`
+
+ !!! warning "Built-in eliminators in Rzk"
+
+ Built-in eliminators in Rzk need to be **always** fully applied (e.g. `#!rzk first` without an argument is invalid syntax!).
+ Technically, this corresponds with the "second presentation" of type theory in Appendix A.2 of the HoTT Book.
+ In practice, this is not always convenient for users, as we often want to curry some of these built-ins,
+ so wrapper functions are introduced (by users), for example:
+
+ ```rzk
+ #define pr₁
+ ( A B : U)
+ : prod A B → A
+ := \ p → first p
+ ```
+
+4. **Computation rules**:
+
+ - Projecting from a pair is computed as follows for any `#!rzk x : A` and `#!rzk y : B`:
+ - `#!rzk first (x , y) ≡ x`
+ - `#!rzk second (x , y) ≡ y`
+ - Applying an lambda abstraction is computed by substituting the argument into a body:
+ - `#!rzk (\ x → y) a ≡ y{x ↦ a}` when `#!rzk a : A` and for all `#!rzk x : A`, `#!rzk y : B`.
+
+5. **Uniqueness principle (optional)**:
+
+ - For any `#!rzk z : prod A B`, we have `#!rzk z ≡ (first z, second z)`
+ - This holds definitionally for product types and Σ-types in Rzk, but is provable in a weaker (propositional) form in HoTT Book
+ - For any function `#!rzk f : A → B`, we have `#!rzk f ≡ \ x → f x`
+
+### Recursion principle
+
+Following the HoTT Book, for each type former we can formalize its _recursion principle_.
+A recursion principle for type `#!rzk T` is a function that allows to produce
+a result of arbitrary type `#!rzk C` from a value of type `#!rzk T`:
+
+```{unchecked .rzk}
+#define rec-T
+ ( C : U)
+ -- ... (parameters to the recursion principle)
+ : T → C
+```
+
+For example, for the product type `#!rzk prod A B`, recursion principle looks like this:
+
+```rzk
+#define rec-prod
+ ( A B : U)
+ ( C : U)
+ ( f : A → B → C)
+ : prod A B → C
+ := \ ( a , b) → f a b
+```
+
+For the `#!rzk Unit` type, recursion principle is trivial:
+
+```rzk
+#define rec-Unit
+ ( C : U)
+ ( c : C)
+ : Unit → C
+ := \ unit → c
+```
+
+### Induction principle
+
+To define a _dependent_ function out of a type, we use its _induction principle_,
+which can be seen as a dependent version of the recursion principle.
+An induction principle for type `#!rzk T` is a function that allows to produce
+a result of arbitrary type `#!rzk C z` from a value `#!rzk z : T`:
+
+```{unchecked .rzk}
+#define ind-T
+ ( C : T → U)
+ -- ... (parameters to the induction principle)
+ : (z : T) → C z
+```
+
+For example, for the product type `#!rzk prod A B`, induction principle looks like this:
+
+```rzk
+#define ind-prod
+ ( A B : U)
+ ( C : prod A B → U)
+ ( f : (a : A) → (b : B) → C (a , b))
+ : ( z : prod A B) → C z
+ := \ ( a , b) → f a b
+```
+
+We can use `#!rzk ind-prod` to prove the uniqueness principle for products.
+Here we use the identity type, which we will cover later, but for now it is
+sufficient to know that there is always an element `#!rzk refl_{x} : x =_{A} x`
+for any `#!rzk x : A`.
+
+```rzk
+#define uniq-prod
+ ( A B : U)
+ ( z : prod A B)
+ : ( first z , second z) =_{prod A B} z
+ := ind-prod A B
+ ( \ z' → (first z' , second z') =_{prod A B} z') -- C
+ ( \ a b → refl_{(a , b)})
+ -- C (a, b)
+ -- ≡ ( \ z' → (first z', second z') =_{prod A B} z') (a, b)
+ -- ≡ (first (a, b), second (a, b)) =_{prod A B} (a, b)
+ -- ≡ (a, second (a, b)) =_{prod A B} (a, b)
+ -- ≡ (a, b) =_{prod A B} (a, b)
+ z
+```
+
+Since in Rzk the uniqueness principle is builtin, a simpler proof also works:
+
+```rzk
+#define uniq-prod'
+ ( A B : U)
+ ( z : prod A B)
+ : ( first z , second z) =_{prod A B} z
+ := refl_{z} -- works in Rzk, not in HoTT Book, since in Rzk we have (first z, second z) ≡ z
+```
+
+For the `#!rzk Unit` type, induction principle is trivial:
+
+```rzk
+#define ind-Unit
+ ( C : Unit → U)
+ ( c : C unit)
+ : ( z : Unit) → C z
+ := \ unit → c
+```
+
+Unlike `#!rzk rec-Unit`, induction principle for `#!rzk Unit` is not useless,
+since it allows, for example, to prove the uniqueness principle:
+
+```rzk
+#define uniq-Unit
+ ( z : Unit)
+ : unit =_{Unit} z
+ := ind-Unit
+ ( \ z' → unit =_{Unit} z')
+ ( refl_{unit})
+ z
+```
+
+Again, since Rzk has a builtin uniqueness principle for `#!rzk Unit`, a simpler proof also works:
+
+```rzk
+#define uniq-Unit'
+ ( z : Unit)
+ : unit =_{Unit} z
+ := refl_{z} -- works in Rzk, not in HoTT Book, since in Rzk we have unit ≡ z
+```
+
+## Dependent pair types (Σ-types)
+
+A straightforward generalization of product types to dependent pairs `#!rzk Σ (a : A), B a`
+where `#!rzk A` is a type and `#!rzk B : A → U` is a type family indexed in `#!rzk A`.
+
+The indended values of `#!rzk Σ (a : A), B a` are pairs `#!rzk (a , b)` of
+terms `#!rzk a : A` and `#!rzk b : B a`. Note that the type of the second component
+may depend on the value of the first component.
+When the type family `#!rzk B` is constant, e.g. `#!rzk (\ _ → C)`,
+then `#!rzk Σ (a : A), B a` becomes exactly the product type `#!rzk prod A C`.
+
+To eliminate dependent pairs, we use `#!rzk first`, `#!rzk second`, or pattern
+matching on pairs. However, the types of projections are less obvious compared
+to the case of product types.
+
+### Projections
+
+The first projection can be easily defined in terms of pattern matching:
+
+```rzk
+#define pr₁
+ ( A : U)
+ ( B : A → U)
+ : ( Σ ( a : A) , B a) → A
+ := \ ( a , _) → a
+```
+
+However, second projection requires some care. For instance, we might try this:
+
+```{unchecked .rzk}
+-- NOTE: incorrect definition
+#define pr₂
+ ( A : U)
+ ( B : A → U)
+ : (Σ (a : A), B a) → B a -- ERROR!
+ := \ (_ , b) → b
+```
+
+```
+undefined variable: a
+```
+
+We get the `undefined variable` error since `a` is not visible outside of Σ-type definition.
+To access it, we need a dependent function:
+
+```rzk
+#define pr₂
+ ( A : U)
+ ( B : A → U)
+ : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
+ := \ ( _ , b) → b
+```
+
+In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types (as in "total spaces"):
+
+```rzk
+#define total-type
+ ( A : U)
+ ( B : A → U)
+ : U
+ := Σ ( a : A) , B a
+```
+
+We can use pattern matching in the function type and this new definition to write
+second projection slightly differently:
+
+```rzk
+#define pr₂'
+ ( A : U)
+ ( B : A → U)
+ ( ( a , b) : total-type A B)
+ : B a
+ := b
+```
+
+### Recursion and induction principles
+
+The recursion principle for Σ-types is a simple generalization of
+the recursion principle for product types:
+
+```rzk
+#define rec-Σ
+ ( A : U)
+ ( B : A → U)
+ ( C : U)
+ ( f : (a : A) → B a → C)
+ : total-type A B → C
+ := \ ( a , b) → f a b
+```
+
+The induction principle is, again, a generalization of the recursion
+principle to dependent types:
+
+```rzk
+#define ind-Σ
+ ( A : U)
+ ( B : A → U)
+ ( C : total-type A B → U)
+ ( f : (a : A) → (b : B a) → C (a , b))
+ : ( z : total-type A B) → C z
+ := \ ( a , b) → f a b
+```
+
+As before, using `#!rzk ind-Σ` we may prove the uniqueness principle, now for Σ-types:
+
+```rzk
+#define uniq-Σ
+ ( A : U)
+ ( B : A → U)
+ ( z : total-type A B)
+ : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
+ := ind-Σ A B
+ ( \ z → (pr₁ A B z , pr₂ A B z) =_{total-type A B} z)
+ ( \ a b → refl_{(a , b)})
+ z
+```
+
+And again, Rzk can accept a simpler proof, since uniqueness for Σ-types is already built into it:
+
+```rzk
+#define uniq-Σ'
+ ( A : U)
+ ( B : A → U)
+ ( z : total-type A B)
+ : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
+ := refl_{z} -- works in Rzk, but not in HoTT Book
+```
+
+### Type-theoretic "axiom" of choice
+
+Using `#!rzk ind-Σ` we can also prove a type-theoretic axiom of choice:
+
+```rzk
+#define AxiomOfChoice
+ : U
+ := ( A : U)
+ → ( B : U)
+ → ( R : A → B → U)
+ → ( ( x : A) → Σ (y : B) , R x y)
+ → ( Σ ( f : A → B) , (x : A) → R x (f x))
+```
+
+You are encouraged to try proving this yourself first.
+
+If you encounter problems, try looking for the proof in the HoTT Book Section 1.6 (page 32).
+
+If you still have issues formalizing it in Rzk, you may peek here:
+
+??? abstract "Proof of the type theoretic axiom of choice"
+
+ ```rzk
+ #define ac : AxiomOfChoice
+ := \ A B R g → ( \ a → first (g a) , \ x → second (g x))
+ -- g : (x : A) → Σ (y : B), R x y
+ -- x : A
+ -- g x : Σ (y : B), R x y
+ -- second (g x) : R x (first (g x))
+
+ -- f : A → B
+ -- f := \ a → first (g a)
+ --
+ -- R x (f x)
+ -- == R x ((\ a → first (g a)) x)
+ -- == R x (first (g x))
+ ```
+
+## Coproducts
+
+Given types $A$ and $B$ a coproduct type $A + B$ corresponds intuitively
+to a disjoint union of $A$ and $B$ (in set theory). We also have a nullary
+version: $\mathbf{0}$ (empty type).
+
+In Rzk, empty type and coproduct types do not exist, but a weaker version can be postulated.
+
+### Postulating the empty type
+
+For example, an empty type can be postulated as follows:
+
+```rzk
+#postulate Void
+ : U
+#postulate ind-Void
+ ( C : Void → U)
+ : ( z : Void) → C z
+```
+
+Since there should be no values of type `#!rzk Void`,
+the induction principle corresponds to the principle that from falsehood anything follows.
+A non-dependent version of that corresponds to the recursion principle,
+which we can define in terms of `#!rzk ind-Void`:
+
+```rzk
+#define rec-Void
+ ( C : U)
+ : Void → C
+ := ind-Void (\ _ → C)
+```
+
+### Postulating the coproduct type
+
+!!! warning "Postulating coproducts"
+
+ This subsection currently provides postulates with little explanation.
+ Once Rzk has support for user-defined (higher) inductive types or built-in coproducts,
+ this section will be updated.
+
+Similarly, we can postulate the coproduct:
+
+```rzk
+#postulate coprod
+ ( A B : U)
+ : U
+```
+
+There are two ways to create a term of type `#!rzk coprod A B` —
+inject a term from `#!rzk A` or a term of `#!rzk B`:
+
+```rzk
+#postulate inl
+ ( A B : U)
+ : A → coprod A B
+#postulate inr
+ ( A B : U)
+ : B → coprod A B
+```
+
+To eliminate a coproduct, we have to provide two handlers —
+one for the left case and one for the right:
+
+```rzk
+#postulate ind-coprod
+ ( A B : U)
+ ( C : coprod A B → U)
+ ( l : (a : A) → C (inl A B a))
+ ( r : (b : B) → C (inr A B b))
+ : ( z : coprod A B) → C z
+```
+
+Since we are postulating the induction principle,
+we also have to provide the computational rules explicitly.
+However, in Rzk, we can only postulate _propositional_ computational rules:
+
+```rzk
+#postulate ind-coprod-inl
+ ( A B : U)
+ ( C : coprod A B → U)
+ ( l : (a : A) → C (inl A B a))
+ ( r : (b : B) → C (inr A B b))
+ ( a : A)
+ : ind-coprod A B C l r (inl A B a) = l a
+
+#postulate ind-coprod-inr
+ ( A B : U)
+ ( C : coprod A B → U)
+ ( l : (a : A) → C (inl A B a))
+ ( r : (b : B) → C (inr A B b))
+ ( b : B)
+ : ind-coprod A B C l r (inr A B b) = r b
+```
+
+We can now define recursion for coproducts
+as a special case of induction:
+
+```rzk
+#define rec-coprod
+ ( A B : U)
+ ( C : U)
+ ( l : A → C)
+ ( r : B → C)
+ : coprod A B → C
+ := ind-coprod A B (\ _ → C) l r
+```
+
+The uniqueness principle for coproducts says
+that any coproduct is either an `#!rzk inl` or an `#!rzk inr`.
+Proving the uniqueness is fairly straightforward, except
+we have to provide some intermediate types explicitly:
+
+```rzk
+#define uniq-coprod
+ ( A B : U)
+ ( z : coprod A B)
+ : coprod
+ ( Σ ( a : A) , inl A B a = z)
+ ( Σ ( b : B) , inr A B b = z)
+ := ind-coprod A B
+ ( \ z' → coprod
+ ( Σ ( a : A) , inl A B a = z')
+ ( Σ ( b : B) , inr A B b = z'))
+ ( \ a' → inl
+ ( Σ ( a : A) , (inl A B a = inl A B a'))
+ ( Σ ( b : B) , (inr A B b = inl A B a'))
+ ( a' , refl))
+ ( \ b' → inr
+ ( Σ ( a : A) , (inl A B a = inr A B b'))
+ ( Σ ( b : B) , (inr A B b = inr A B b'))
+ ( b' , refl))
+ z
+```
+
+## Booleans
+
+!!! warning "Postulating booleans"
+
+ This subsection currently provides postulates with little explanation.
+ Once Rzk has support for user-defined (higher) inductive types or built-in booleans,
+ this section will be updated.
+
+```rzk
+#postulate Bool
+ : U
+#postulate false
+ : Bool
+#postulate true
+ : Bool
+```
+
+```rzk
+#postulate ind-Bool
+ ( C : Bool → U)
+ ( f : C false)
+ ( t : C true)
+ : ( z : Bool) → C z
+```
+
+```rzk
+#postulate ind-Bool-false
+ ( C : Bool → U)
+ ( f : C false)
+ ( t : C true)
+ : ind-Bool C f t false = f
+#postulate ind-Bool-true
+ ( C : Bool → U)
+ ( f : C false)
+ ( t : C true)
+ : ind-Bool C f t true = t
+```
+
+```rzk
+#define rec-Bool
+ ( C : U)
+ ( f t : C)
+ : Bool → C
+ := ind-Bool (\ _ → C) f t
+```
+
+```rzk
+#define uniq-Bool
+ ( z : Bool)
+ : coprod (z = false) (z = true)
+ := ind-Bool
+ ( \ z' → coprod (z' = false) (z' = true))
+ ( inl (false = false) (false = true) refl)
+ ( inr (true = false) (true = true) refl)
+ z
+```
+
+```rzk
+#define not
+ : Bool → Bool
+ := rec-Bool Bool true false
+```
+
+Unfortunately, because computation rules are postulated
+in a weak form, they do not compute automatically and have to be used explicitly,
+so the following proof does not work:
+
+```{unchecked .rzk}
+#define not-not-is-identity
+ : (z : Bool) → not (not z) = z
+ := ind-Bool
+ ( \ z → not (not z) = z)
+ ( refl)
+ ( refl)
+```
+
+There is a way to fix the proof, but we'll need to learn more about
+the identity types before we can do that.
+
+## Natural numbers
+
+!!! warning "Postulating natural numbers"
+
+ This subsection currently provides postulates without explanations.
+ Once Rzk has support for user-defined (higher) inductive types or built-in natural numbers,
+ this section will be updated.
+
+```rzk
+#postulate ℕ
+ : U
+#postulate zero
+ : ℕ
+#postulate succ (n : ℕ)
+ : ℕ
+
+#postulate ind-ℕ
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : ( n : ℕ) → C n
+
+#postulate ind-ℕ-zero
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : ind-ℕ C base step zero = base
+#postulate ind-ℕ-succ
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ ( n : ℕ)
+ : ind-ℕ C base step (succ n) = step n (ind-ℕ C base step n)
+```
+
+```rzk
+#define rec-ℕ
+ ( C : U)
+ ( base : C)
+ ( step : (n : ℕ) → C → C)
+ : ℕ → C
+ := ind-ℕ (\ _ → C) base step
+```
+
+```rzk
+#define double-ℕ
+ : ℕ → ℕ
+ := rec-ℕ ℕ zero (\ _ m → succ (succ m))
+```
+
+```rzk
+#define compute-ind-ℕ-zero
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : C zero
+ := base
+
+#define compute-ind-ℕ-one
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : C (succ zero)
+ := step zero (compute-ind-ℕ-zero C base step)
+
+#define compute-ind-ℕ-two
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : C (succ (succ zero))
+ := step (succ zero) (compute-ind-ℕ-one C base step)
+
+#compute compute-ind-ℕ-two (\ _ → ℕ) zero (\ _ m → succ (succ m))
+```
diff --git a/docs/docs/getting-started/install.md b/docs/docs/en/getting-started/install.md
similarity index 88%
rename from docs/docs/getting-started/install.md
rename to docs/docs/en/getting-started/install.md
index 2f0276ab2..d2e98d560 100644
--- a/docs/docs/getting-started/install.md
+++ b/docs/docs/en/getting-started/install.md
@@ -7,9 +7,9 @@ These instructions will walk you through setting up Rzk using the "basic" setup
1. Install [VS Code](https://code.visualstudio.com/).
2. Launch VS Code and install the [`rzk` extension](https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting).
3. Create a new file using "File > New Text File" (Ctrl+N ). Click the `Select a language` prompt, type in `rzk`, and select "Literate Rzk Markdown".
- ![VS Code rzk language selector.](../../assets/images/vscode-rzk-select-language.png)
+ ![VS Code rzk language selector.](../assets/images/vscode-rzk-select-language.png)
4. You should see the following popup:
- ![VS Code rzk install prompt.](../../assets/images/vscode-rzk-install-prompt.png)
+ ![VS Code rzk install prompt.](../assets/images/vscode-rzk-install-prompt.png)
5. Click "Yes" button.
6. While it is installing, you can paste the following literate Rzk program into the new file:
@@ -26,7 +26,7 @@ These instructions will walk you through setting up Rzk using the "basic" setup
````
7. When the installation is done you should see the following popup:
- ![VS Code rzk reload prompt.](../../assets/images/vscode-rzk-install-success-reload-prompt.png)
+ ![VS Code rzk reload prompt.](../assets/images/vscode-rzk-install-success-reload-prompt.png)
8. Click "Reload button".
9. Save your file as `example.rzk.md`.
10. Open local Terminal (Ctrl+` ).
@@ -50,7 +50,7 @@ These instructions will walk you through setting up Rzk using the "basic" setup
13. Congratulations! Now you have a working rzk setup :) Note that the rzk extension will notify you about updates of `rzk` and prompt updating to new versions.
-14. See [Quickstart](../quickstart.rzk) to get familiar with the Rzk language!
+14. See [Quickstart](quickstart.rzk.md) to get familiar with the Rzk language!
## Install binaries
diff --git a/docs/docs/en/getting-started/project.md b/docs/docs/en/getting-started/project.md
new file mode 100644
index 000000000..155627cac
--- /dev/null
+++ b/docs/docs/en/getting-started/project.md
@@ -0,0 +1,6 @@
+# Setting up an Rzk project
+
+!!! warning "Work-in-progress"
+ Guide will be here soon.
+ For now, please use the template project: .
+ Also check out for an example of a project with generated documentation.
diff --git a/docs/docs/getting-started/quickstart.rzk.md b/docs/docs/en/getting-started/quickstart.rzk.md
similarity index 82%
rename from docs/docs/getting-started/quickstart.rzk.md
rename to docs/docs/en/getting-started/quickstart.rzk.md
index 09bdc7d97..3b87f01ee 100644
--- a/docs/docs/getting-started/quickstart.rzk.md
+++ b/docs/docs/en/getting-started/quickstart.rzk.md
@@ -3,9 +3,10 @@
!!! warning "Work-in-progress"
Documentation is a work in progress.
+First, [install Rzk](install.md).
+
This is a literate `rzk` file:
```rzk
#lang rzk-1
```
-
diff --git a/docs/docs/en/index.md b/docs/docs/en/index.md
new file mode 100644
index 000000000..89e52dd36
--- /dev/null
+++ b/docs/docs/en/index.md
@@ -0,0 +1,70 @@
+# Rzk proof assistant
+
+Rzk is an experimental proof assistant,
+based on [«Type Theory for Synthetic ∞-categories»](https://arxiv.org/abs/1705.07442)[^1].
+
+[Get started with Rzk](getting-started/install.md){ .md-button .md-button--primary }
+[Try Rzk Playground](playground/index.html){ .md-button }
+
+## About this project
+
+This project has started with the idea of bringing Riehl and Shulman's 2017 paper[^1]
+to "life" by implementing a proof assistant based on their type theory with shapes.
+At the moment, Rzk provides a language that is close to the original paper,
+as well as some tooling around it (such as a VS Code extension and a language server with syntax highlighting and formatting support).
+
+### Formalizing ∞-category theory
+
+A big portion of the original paper (up to the ∞-categorical Yoneda lemma) has been formalized in Rzk (see [Yoneda for ∞-categories](https://emilyriehl.github.io/yoneda/)[^2]).
+More formalization results are under way (see [sHoTT](https://rzk-lang.github.io/sHoTT/)).
+There are also some efforts to formalize the HoTT Book in Rzk (see [hottbook](https://rzk-lang.github.io/hottbook/)).
+
+### Using Rzk
+
+The recommended way of interacting with Rzk is via VS Code (see [Getting Started](getting-started/install.md)),
+but you can also download binaries from [GitHub Releases](https://github.com/rzk-lang/rzk/releases), build [from sources](getting-started/install.md#install-from-sources),
+or try setting up the Rzk Language Server with your editor of choice.
+Additionally, for "throwaway" single-file formalizations, you can use [Rzk Online Playground](playground/index.html).
+
+### Implementation
+
+Rzk serves also as a playground for some techniques of developing proof assistants in Haskell.
+In particular, it features a version of second-order abstract syntax for handling binders and,
+in the future, dependent type inference through higher-order unification[^3] [^4].
+The idea is ultimately, to provide higher-order unification and/or dependent type inference "as a library",
+keeping the implementation of Rzk (at least its core language) small, maintainable, and safe.
+
+Another important part of Rzk is the tope layer solver[^5],
+which is a built-in intuitionistic theorem prover required for a part of the type theory.
+Although its implementation is fairly simple,
+it is sufficient to check existing proofs in synthetic ∞-categories
+without requiring any explicit proofs for the tope layer.
+
+Rzk and the tooling around it is developed by just a couple of people.
+See the list of contributors at [CONTRIBUTORS.md](CONTRIBUTORS.md).
+
+### Discussing Rzk and getting help
+
+A Zulip chat is available for all to join and chat about Rzk, including formalization projects, development of Rzk, and related projects:
+
+[Join Rzk Zulip](https://rzk-lang.zulipchat.com/register/){ .md-button .md-button--primary }
+
+[^1]:
+ Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories_.
+ Higher Structures 1(1), 147-224. 2017.
+
+[^2]:
+ Nikolai Kudasov, Emily Riehl, Jonathan Weinberger.
+ _Formalizing the ∞-categorical Yoneda lemma_. 2023.
+
+[^3]:
+ Nikolai Kudasov. _Functional Pearl: Dependent type inference via free higher-order unification_. 2022.
+
+
+[^4]:
+ Nikolai Kudasov. _E-Unification for Second-Order Abstract Syntax_. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 10:1-10:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
+
+
+[^5]:
+ Nikolai Kudasov. Experimental prover for Tope logic. SCAN 2023, pages 37–39. 2023.
+
diff --git a/docs/docs/en/playground/index.html b/docs/docs/en/playground/index.html
new file mode 100644
index 000000000..349a1670b
--- /dev/null
+++ b/docs/docs/en/playground/index.html
@@ -0,0 +1,16 @@
+
+
+
+
+ Redirecting
+
+
+
+ Redirecting...
+
+
diff --git a/docs/docs/reference/builtins/directed-interval.rzk.md b/docs/docs/en/reference/builtins/directed-interval.rzk.md
similarity index 100%
rename from docs/docs/reference/builtins/directed-interval.rzk.md
rename to docs/docs/en/reference/builtins/directed-interval.rzk.md
diff --git a/docs/docs/reference/builtins/unit.rzk.md b/docs/docs/en/reference/builtins/unit.rzk.md
similarity index 100%
rename from docs/docs/reference/builtins/unit.rzk.md
rename to docs/docs/en/reference/builtins/unit.rzk.md
diff --git a/docs/docs/reference/commands/check.rzk.md b/docs/docs/en/reference/commands/check.rzk.md
similarity index 100%
rename from docs/docs/reference/commands/check.rzk.md
rename to docs/docs/en/reference/commands/check.rzk.md
diff --git a/docs/docs/reference/commands/compute.rzk.md b/docs/docs/en/reference/commands/compute.rzk.md
similarity index 100%
rename from docs/docs/reference/commands/compute.rzk.md
rename to docs/docs/en/reference/commands/compute.rzk.md
diff --git a/docs/docs/reference/commands/define-postulate.rzk.md b/docs/docs/en/reference/commands/define-postulate.rzk.md
similarity index 100%
rename from docs/docs/reference/commands/define-postulate.rzk.md
rename to docs/docs/en/reference/commands/define-postulate.rzk.md
diff --git a/docs/docs/reference/commands/options.rzk.md b/docs/docs/en/reference/commands/options.rzk.md
similarity index 100%
rename from docs/docs/reference/commands/options.rzk.md
rename to docs/docs/en/reference/commands/options.rzk.md
diff --git a/docs/docs/reference/cube-layer.rzk.md b/docs/docs/en/reference/cube-layer.rzk.md
similarity index 77%
rename from docs/docs/reference/cube-layer.rzk.md
rename to docs/docs/en/reference/cube-layer.rzk.md
index a593f80f4..fe5f54e79 100644
--- a/docs/docs/reference/cube-layer.rzk.md
+++ b/docs/docs/en/reference/cube-layer.rzk.md
@@ -9,7 +9,7 @@ All cubes live in `#!rzk CUBE` universe.
There are two built-in cubes:
1. `#!rzk 1` cube is a unit cube with a single point `#!rzk *_1`
-2. `#!rzk 2` cube is a [directed interval](../builtins/directed-interval.rzk.md) cube with points `#!rzk 0_2` and `#!rzk 1_2`
+2. `#!rzk 2` cube is a [directed interval](builtins/directed-interval.rzk.md) cube with points `#!rzk 0_2` and `#!rzk 1_2`
It is also possible to have `#!rzk CUBE` variables and make products of cubes:
@@ -22,8 +22,7 @@ You can usually use `#!rzk (t, s)` both as a pattern, and a construction of a pa
```rzk
-- Swap point components of a point in a cube I × I
#define swap
- (I : CUBE)
- : (I * I) -> I * I
- := \(t, s) -> (s, t)
+ ( I : CUBE)
+ : ( I × I) → I × I
+ := \ ( t , s) → (s , t)
```
-
diff --git a/docs/docs/reference/extension-types.rzk.md b/docs/docs/en/reference/extension-types.rzk.md
similarity index 100%
rename from docs/docs/reference/extension-types.rzk.md
rename to docs/docs/en/reference/extension-types.rzk.md
diff --git a/docs/docs/reference/introduction.rzk.md b/docs/docs/en/reference/introduction.rzk.md
similarity index 100%
rename from docs/docs/reference/introduction.rzk.md
rename to docs/docs/en/reference/introduction.rzk.md
diff --git a/docs/docs/reference/render.rzk.md b/docs/docs/en/reference/render.rzk.md
similarity index 100%
rename from docs/docs/reference/render.rzk.md
rename to docs/docs/en/reference/render.rzk.md
diff --git a/docs/docs/reference/sections.rzk.md b/docs/docs/en/reference/sections.rzk.md
similarity index 100%
rename from docs/docs/reference/sections.rzk.md
rename to docs/docs/en/reference/sections.rzk.md
diff --git a/docs/docs/reference/tope-disjunction-elimination.rzk.md b/docs/docs/en/reference/tope-disjunction-elimination.rzk.md
similarity index 100%
rename from docs/docs/reference/tope-disjunction-elimination.rzk.md
rename to docs/docs/en/reference/tope-disjunction-elimination.rzk.md
diff --git a/docs/docs/reference/tope-layer.rzk.md b/docs/docs/en/reference/tope-layer.rzk.md
similarity index 100%
rename from docs/docs/reference/tope-layer.rzk.md
rename to docs/docs/en/reference/tope-layer.rzk.md
diff --git a/docs/docs/reference/type-layer.rzk.md b/docs/docs/en/reference/type-layer.rzk.md
similarity index 100%
rename from docs/docs/reference/type-layer.rzk.md
rename to docs/docs/en/reference/type-layer.rzk.md
diff --git a/docs/docs/en/rzk.yaml b/docs/docs/en/rzk.yaml
new file mode 100644
index 000000000..3469d50f8
--- /dev/null
+++ b/docs/docs/en/rzk.yaml
@@ -0,0 +1,3 @@
+include:
+ - getting-started/dependent-types.rzk.md
+ - examples/recId.rzk.md
diff --git a/docs/docs/en/tools.md b/docs/docs/en/tools.md
new file mode 100644
index 000000000..8e109106d
--- /dev/null
+++ b/docs/docs/en/tools.md
@@ -0,0 +1,30 @@
+# Tools
+
+Rzk proof assistant comes with built-in language server and formatter.
+
+Other tools help enhance user experience or automate things.
+
+### VS Code extension for Rzk
+
+See [rzk-lang/vscode-rzk](https://github.com/rzk-lang/vscode-rzk).
+VS Code extension offers a lot of conveniences and using VS Code is recommended for newcomers,
+as it is considered the primary use case and has most support from the developers.
+
+### MkDocs plugin for Rzk
+
+See [rzk-lang/mkdocs-plugin-rzk](https://github.com/rzk-lang/mkdocs-plugin-rzk).
+MkDocs plugin enhances documentation build from literate Rzk Markdown files:
+- adds diagram rendering (experimental)
+- adds definition anchors (helpful to have "permalinks" to definitions)
+
+### GitHub Action for Rzk
+
+See [rzk-lang/rzk-action](https://github.com/rzk-lang/rzk-action).
+This action allows to check your Rzk formalizations on GitHub automatically.
+It can also be used to check formatting (experimental).
+
+### Syntax highlighting (Pygments) for Rzk
+
+See [rzk-lang/pygments-rzk](https://github.com/rzk-lang/pygments-rzk).
+This is a simple syntax highlighter for Pygments (used by MkDocs and `minted` package in LaTeX).
+Note that VS Code extension is using the Rzk Language Server for more accurate "semantic highlighting".
diff --git a/docs/docs/examples/hom.rzk.md b/docs/docs/examples/hom.rzk.md
deleted file mode 100644
index 854fd9470..000000000
--- a/docs/docs/examples/hom.rzk.md
+++ /dev/null
@@ -1,52 +0,0 @@
-# Hom-type
-
-```rzk
-hom : (A : U) -> (x : A) -> (y : A) -> U
- := \A -> \x -> \y -> <{t : 2 | TOP} -> A [ t === 0_2 \/ t === 1_2 |-> recOR(t === 0_2, t === 1_2, x, y) ]>
-```
-
-```rzk
-RS17:Prop:3.5a : (A : U) -> (f : <{t : 2 | TOP} -> A[BOT |-> recBOT]>) -> <{ts : 2 * 2 | TOP} -> A [BOT |-> recBOT]>
- := \(A : U) -> \(f : <{t : 2 | TOP} -> A[BOT |-> recBOT]>) -> \{ts : 2 * 2 | TOP} -> recOR ((first ts) <= (second ts), (second ts) <= (first ts), f (second ts), f (first ts))
-
-RS17:Prop:3.5b : (A : U) -> (f : <{t : 2 | TOP} -> A[BOT |-> recBOT]>) -> <{ts : 2 * 2 | TOP} -> A [BOT |-> recBOT]>
- := \(A : U) -> \(f : <{t : 2 | TOP} -> A[BOT |-> recBOT]>) -> \{ts : 2 * 2 | TOP} -> recOR ((first ts) <= (second ts), (second ts) <= (first ts), f (first ts), f (second ts))
-```
-
-```rzk
-isShapeRetraction : (I : CUBE) -> (A : U) -> (phi : (t : I) -> TOPE) -> (psi : (t : I) -> TOPE) -> (f : (k : <{t : I | psi t} -> A [BOT |-> recBOT]>) -> <{t : I | phi t} -> A [BOT |-> recBOT]>) -> U
- := \(I : CUBE) -> \(A : U) -> \(phi : (t : I) -> TOPE) -> \(psi : (t : I) -> TOPE) -> \(f : (k : <{t : I | psi t} -> A [BOT |-> recBOT]>) -> <{t : I | phi t} -> A [BOT |-> recBOT]>) -> ∑ (g : (k : <{t : I | phi t} -> A [BOT |-> recBOT]>) -> <{t : I | psi t} -> A [BOT |-> recBOT]>), (k : <{t : I | phi t} -> A [BOT |-> recBOT]>) -> f (g k) =_{<{t : I | phi t} -> A [BOT |-> recBOT]>} k
-
-shapeRetract : (I : CUBE) -> (phi : (t : I) -> TOPE) -> (psi : (t : I) -> TOPE) -> U
- := \(I : CUBE) -> \(phi : (t : I) -> TOPE) -> \(psi : (t : I) -> TOPE) -> (A : U) -> ∑ (f : (k : <{t : I | psi t} -> A [BOT |-> recBOT]>) -> <{t : I | phi t} -> A [BOT |-> recBOT]>), isShapeRetraction I A phi psi f
-```
-
-```rzk
-Δ¹ : (t : 2) -> TOPE
- := \(t : 2) -> TOP
-
-Δ² : (t : 2 * 2) -> TOPE
- := \(t, s) -> s <= t
-
-Δ³ : (t : 2 * 2 * 2) -> TOPE
- := \((t1, t2), t3) -> t3 <= t2 /\ t2 <= t1
-
-shapeProd : (I : CUBE) -> (J : CUBE) -> (psi : (t : I) -> TOPE) -> (chi : (s : J) -> TOPE) -> (ts : I * J) -> TOPE
- := \I -> \J -> \psi -> \chi -> \(t, s) -> psi t /\ chi s
-
-Δ¹×Δ¹ : (t : 2 * 2) -> TOPE
- := shapeProd 2 2 Δ¹ Δ¹
-
-Δ²×Δ¹ : (t : 2 * 2 * 2) -> TOPE
- := shapeProd (2 * 2) 2 Δ² Δ¹
-```
-
-```rzk
-Δ²-is-retract-of-Δ¹×Δ¹ : shapeRetract (2 * 2) Δ² Δ¹×Δ¹
- := \A -> (\k -> \ts -> k ts, (\k -> \(t, s) -> recOR(t <= s, s <= t, k (t, s), k (t, s)), \k -> refl_{k}))
-```
-
-```rzk
-Δ³-is-retract-of-Δ²×Δ¹ : shapeRetract (2 * 2 * 2) Δ³ Δ²×Δ¹
- := \A -> (\k -> \ts -> k ((first (first ts), second ts), second (first ts)), (\k -> \ts -> recOR((second ts) <= (second (first ts)), (second (first ts)) <= (second ts) /\ (second ts) <= (first (first ts)) \/ (first (first ts)) <= second ts, k ((first (first ts), second ts), second (first ts)), recOR((second (first ts)) <= (second ts) /\ (second ts) <= (first (first ts)), (first (first ts)) <= second ts, k ((first (first ts), second ts), second (first ts)), k ((first (first ts), first (first ts)), second (first ts)))), \k -> refl_{k}))
-```
diff --git a/docs/docs/getting-started/publishing-with-mkdocs.md b/docs/docs/getting-started/publishing-with-mkdocs.md
deleted file mode 100644
index 6e9bdfba2..000000000
--- a/docs/docs/getting-started/publishing-with-mkdocs.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# Building and publishing Rzk formalisations with MkDocs
-
-!!! warning "Work-in-progress"
- Guide will be here soon. For now, please, check out https://github.com/emilyriehl/yoneda for an example with GitHub Actions.
diff --git a/docs/docs/index.md b/docs/docs/index.md
deleted file mode 100644
index 0ec6e3a0b..000000000
--- a/docs/docs/index.md
+++ /dev/null
@@ -1,23 +0,0 @@
-# rzk — an experimental proof assistant for synthetic ∞-categories
-
-`rzk` is an early prototype of a proof assistant for a family of type systems, including Riehl and Shulman's «Type Theory for Synthetic ∞-categories» ([https://arxiv.org/abs/1705.07442](https://arxiv.org/abs/1705.07442)).
-
-[Get started with Rzk](getting-started/install.md){ .md-button .md-button--primary }
-[Try Rzk Playground](playground/){ .md-button }
-
-## About this project
-
-This project has started with the idea of bringing Riehl and Shulman's 2017 paper [1] to "life" by implementing a proof assistant based on their type theory with shapes. Currently an early prototype with an [online playground](https://rzk-lang.github.io/rzk/develop/playground/) is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: and . `sHoTT` project (originally a fork of the yoneda project) aims to cover more formalisations in simplicial HoTT and ∞-categories, while `yoneda` project aims to compare different formalisations of the Yoneda lemma.
-
-Internally, `rzk` uses a version of second-order abstract syntax allowing relatively straightforward handling of binders (such as lambda abstraction). In the future, `rzk` aims to support dependent type inference relying on E-unification for second-order abstract syntax [2].
-Using such representation is motivated by automatic handling of binders and easily automated boilerplate code. The idea is that this should keep the implementation of `rzk` relatively small and less error-prone than some of the existing approaches to implementation of dependent type checkers.
-
-An important part of `rzk` is a tope layer solver, which is essentially a theorem prover for a part of the type theory. A related project, dedicated just to that part is available at . `simple-topes` supports used-defined cubes, topes, and tope layer axioms. Once stable, `simple-topes` will be merged into `rzk`, expanding the proof assistant to the type theory with shapes, allowing formalisations for (variants of) cubical, globular, and other geometric versions of HoTT.
-
-See the list of contributors at [CONTRIBUTORS.md](CONTRIBUTORS.md).
-
-## Discussing Rzk and getting help
-
-A Zulip chat is available for all to join and chat about Rzk, including formalization projects, development of Rzk, and related projects:
-
-[Join Rzk Zulip](https://rzk-lang.zulipchat.com/register/){ .md-button .md-button--primary }
diff --git a/docs/docs/related/sHoTT.md b/docs/docs/related/sHoTT.md
deleted file mode 100644
index 4e2833e13..000000000
--- a/docs/docs/related/sHoTT.md
+++ /dev/null
@@ -1,11 +0,0 @@
-# sHoTT
-
-sHoTT is a formalisation project for simplicial HoTT and ∞-categories.
-
-The project is a fork of https://github.com/emilyriehl/yoneda ,
-with a goal to grow and eventually include various
-formalisations for HoTT (e.g. HoTT book),
-synthetic fibered ∞-categories from the work of Ulrik Buchholtz and Jonathan Weinberger, variations of cubical type theories, etc.
-
-See more details in the documentation of the project at
-https://github.com/rzk-lang/sHoTT .
diff --git a/docs/docs/related/simple-topes.md b/docs/docs/related/simple-topes.md
deleted file mode 100644
index 651bb04e9..000000000
--- a/docs/docs/related/simple-topes.md
+++ /dev/null
@@ -1,6 +0,0 @@
-# simple-topes
-
-simple-topes is a playground theorem prover project for type theory with shapes that allows user-defined cubes and topes. Once stable, the project will be merged into `rzk`, extending it to a proof assistant for type theory with (user-defined) cubes, topes, and shapes.
-
-See more details in the documentation of the project at
-https://github.com/fizruk/simple-topes .
diff --git a/docs/docs/related/yoneda.md b/docs/docs/related/yoneda.md
deleted file mode 100644
index 0bab66152..000000000
--- a/docs/docs/related/yoneda.md
+++ /dev/null
@@ -1,25 +0,0 @@
-# Yoneda lemma for ∞-categories
-
-This is a formalization library for simplicial Homotopy Type Theory (sHoTT) with
-the aim of proving the Yoneda lemma for ∞-categories following the paper
-"[A type theory for synthetic ∞-categories](https://higher-structures.math.cas.cz/api/files/issues/Vol1Iss1/RiehlShulman)"
-[^1]. This formalization project could be regarded as a companion to the article
-"[Could ∞-category theory be taught to undergraduates?](https://www.ams.org/journals/notices/202305/noti2692/noti2692.html)"
-[^2].
-
-Formalizations were contributed by [Fredrik Bakke](https://github.com/fredrik-bakke),
-[Nikolai Kudasov](https://fizruk.github.io/),
-[Emily Riehl](https://emilyriehl.github.io/), and
-[Jonathan Weinberger](https://sites.google.com/view/jonathanweinberger).
-
-See more about the project at .
-
-[^1]: Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories.
- Higher Structures 1(1), 147-224. 2017.
-
-[^2]: Emily Riehl. Could ∞-category theory be taught to undergraduates? Notices of
- the AMS. May 2023.
-
-
-
-
diff --git a/docs/docs/ru/CHANGELOG.md b/docs/docs/ru/CHANGELOG.md
new file mode 100644
index 000000000..b9d820ec8
--- /dev/null
+++ b/docs/docs/ru/CHANGELOG.md
@@ -0,0 +1 @@
+--8<-- "rzk/ChangeLog.md"
diff --git a/docs/docs/ru/CONTRIBUTORS.md b/docs/docs/ru/CONTRIBUTORS.md
new file mode 100644
index 000000000..2e25bbd52
--- /dev/null
+++ b/docs/docs/ru/CONTRIBUTORS.md
@@ -0,0 +1 @@
+--8<-- "CONTRIBUTORS.md"
diff --git a/docs/docs/ru/community.md b/docs/docs/ru/community.md
new file mode 100644
index 000000000..2f2d59149
--- /dev/null
+++ b/docs/docs/ru/community.md
@@ -0,0 +1,10 @@
+# Сообщество Rzk
+
+Вокруг Rzk собралось небольшое сообщество математиков и информатиков.
+
+## Чат
+
+Для всех желающих доступен (преимущественно англоязычный) чат Zulip,
+в котором можно обсудить формализации, разработку Rzk и смежные проекты:
+
+[Присоединиться к сообществу Rzk в Zulip](https://rzk-lang.zulipchat.com/register/){ .md-button .md-button--primary }
diff --git a/docs/docs/ru/examples/recId.rzk.md b/docs/docs/ru/examples/recId.rzk.md
new file mode 100644
index 000000000..96d780dce
--- /dev/null
+++ b/docs/docs/ru/examples/recId.rzk.md
@@ -0,0 +1,212 @@
+# Tope disjuction elimination along identity paths
+
+\(\mathsf{rec}_{\lor}^{\ψ,\φ}(a_\ψ, a*\φ)\) (written `recOR(ψ, φ, a_psi, a_phi)` in the code)
+is well-typed when \(a*\ψ\) and \(a*\φ\) are \_definitionally equal* on \(\ψ \land \φ\).
+Sometimes this is too strong since many terms are not _definitionally_ equal, but only equal up to a path.
+Luckily, assuming relative function extensionality, we can define a weaker version of \(rec*{\lor}\) (`recOR`), which we call `recId`, that can work in presence of a witness of type \(\prod*{t : I \mid \ψ \land \φ} a*\ψ = a*\φ\).
+
+## Prerequisites
+
+This file relies on some definitions, defined in
+
+- [Getting Started > Dependent Types](../getting-started/dependent-types.rzk.md)
+
+We begin by introducing common HoTT definitions:
+
+```rzk
+#lang rzk-1
+
+-- A is contractible there exists x : A such that for any y : A we have x = y.
+#define iscontr (A : U)
+ : U
+ := Σ ( a : A) , (x : A) → a =_{A} x
+
+-- A is a proposition if for any x, y : A we have x = y
+#define isaprop (A : U)
+ : U
+ := ( x : A) → (y : A) → x =_{A} y
+
+-- A is a set if for any x, y : A the type x =_{A} y is a proposition
+#define isaset (A : U)
+ : U
+ := ( x : A) → (y : A) → isaprop (x =_{A} y)
+
+-- A function f : A → B is an equivalence
+-- if there exists g : B → A
+-- such that for all x : A we have g (f x) = x
+-- and for all y : B we have f (g y) = y
+#define isweq (A : U) (B : U) (f : A → B)
+ : U
+ := Σ ( g : B → A)
+ , prod
+ ( ( x : A) → g (f x) =_{A} x)
+ ( ( y : B) → f (g y) =_{B} y)
+
+-- Equivalence of types A and B
+#define weq (A : U) (B : U)
+ : U
+ := Σ ( f : A → B)
+ , isweq A B f
+
+-- Transport along a path
+#define transport
+ ( A : U)
+ ( C : A → U)
+ ( x y : A)
+ ( p : x =_{A} y)
+ : C x → C y
+ := \ cx → idJ(A , x , (\ z q → C z) , cx , y , p)
+```
+
+## Relative function extensionality
+
+We can now define relative function extensionality. There are several formulations, we provide two, following Riehl and Shulman:
+
+```rzk
+-- [RS17, Axiom 4.6] Relative function extensionality.
+#define relfunext
+ : U
+ := ( I : CUBE)
+ → ( ψ : I → TOPE)
+ → ( φ : ψ → TOPE)
+ → ( A : ψ → U)
+ → ( ( t : ψ) → iscontr (A t))
+ → ( a : ( t : φ) → A t)
+ → ( t : ψ) → A t [ φ t ↦ a t]
+
+-- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
+#define relfunext2
+ : U
+ :=
+ ( I : CUBE)
+ → ( ψ : I → TOPE)
+ → ( φ : ψ → TOPE)
+ → ( A : ψ → U)
+ → ( a : ( t : φ) → A t)
+ → ( f : (t : ψ) → A t [ φ t ↦ a t ])
+ → ( g : ( t : ψ) → A t [ φ t ↦ a t ])
+ → weq
+ ( f = g)
+ ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ])
+```
+
+## Construction of `recId`
+
+The idea is straightforward. We ask for a proof that `a = b` for all points in `ψ ∧ φ`. Then, by relative function extensionality (`relfunext2`), we can show that restrictions of `a` and `b` to `ψ ∧ φ` are equal. If we reformulate `a` as extension of its restriction, then we can `transport` such reformulation along the path connecting two restrictions and apply `recOR`.
+
+First, we define how to restrict an extension type to a subshape:
+
+```rzk
+#section construction-of-recId
+
+#variable r : relfunext2
+#variable I : CUBE
+#variables ψ φ : I → TOPE
+#variable A : (t : I | ψ t ∨ φ t) → U
+
+-- Restrict extension type to a subshape.
+#define restrict_phi
+ ( a : ( t : φ) → A t)
+ : ( t : I | ψ t ∧ φ t) → A t
+ := \ t → a t
+
+-- Restrict extension type to a subshape.
+#define restrict_psi
+ ( a : ( t : ψ) → A t)
+ : ( t : I | ψ t ∧ φ t) → A t
+ := \ t → a t
+```
+
+Then, how to reformulate an `a` (or `b`) as an extension of its restriction:
+
+```rzk
+-- Reformulate extension type as an extension of a restriction.
+#define ext-of-restrict_psi
+ ( a : ( t : ψ) → A t)
+ : ( t : ψ)
+ → A t [ ψ t ∧ φ t ↦ restrict_psi a t ]
+ := a -- type is coerced automatically here
+
+-- Reformulate extension type as an extension of a restriction.
+#define ext-of-restrict_phi
+ ( a : ( t : φ) → A t)
+ : ( t : φ)
+ → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
+ := a -- type is coerced automatically here
+```
+
+Now, assuming relative function extensionality, we construct a path between restrictions:
+
+```rzk
+-- Transform extension of an identity into an identity of restrictions.
+#define restricts-path
+ ( a_psi : (t : ψ) → A t)
+ ( a_phi : (t : φ) → A t)
+ : ( e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
+ → restrict_psi a_psi = restrict_phi a_phi
+ :=
+ first
+ ( second
+ ( r I
+ ( \ t → ψ t ∧ φ t)
+ ( \ t → BOT)
+ ( \ t → A t)
+ ( \ t → recBOT)
+ ( \ t → a_psi t)
+ ( \ t → a_phi t)))
+```
+
+Finally, we bring everything together into `recId`:
+
+```rzk
+-- A weaker version of recOR, demanding only a path between a and b:
+-- recOR(ψ, φ, a, b) demands that for ψ ∧ φ we have a == b (definitionally)
+-- (recId ψ φ a b e) demands that e is the proof that a = b (intensionally) for ψ ∧ φ
+#define recId uses (r) -- we declare that recId is using r on purpose
+ ( a_psi : (t : ψ) → A t)
+ ( a_phi : (t : φ) → A t)
+ ( e : (t : I | ψ t ∧ φ t) → a_psi t = a_phi t)
+ : ( t : I | ψ t ∨ φ t) → A t
+ := \ t → recOR(
+ ψ t ↦
+ transport
+ ( ( s : I | ψ s ∧ φ s) → A s)
+ ( \ ra → (s : ψ) → A s [ ψ s ∧ φ s ↦ ra s ])
+ ( restrict_psi a_psi)
+ ( restrict_phi a_phi)
+ ( restricts-path a_psi a_phi e)
+ ( ext-of-restrict_psi a_psi)
+ ( t)
+ , φ t ↦
+ ext-of-restrict_phi a_phi t
+ )
+
+#end construction-of-recId
+```
+
+## Gluing extension types
+
+An application of of `recId` is gluing together extension types,
+whenever we can show that they are equal on the intersection of shapes:
+
+```rzk
+-- If two extension types are equal along two subshapes,
+-- then they are also equal along their union.
+#define id-along-border
+ ( r : relfunext2)
+ ( I : CUBE)
+ ( ψ : I → TOPE)
+ ( φ : I → TOPE)
+ ( A : (t : I | ψ t ∨ φ t) → U)
+ ( a b : (t : I | ψ t ∨ φ t) → A t)
+ ( e_psi : (t : ψ) → a t = b t)
+ ( e_phi : (t : φ) → a t = b t)
+ ( border-is-a-set : (t : I | ψ t ∧ φ t) → isaset (A t))
+ : ( t : I | ψ t ∨ φ t) → a t = b t
+ :=
+ recId r I ψ φ
+ ( \ t → a t = b t)
+ ( e_psi)
+ ( e_phi)
+ ( \ t → border-is-a-set t (a t) (b t) (e_psi t) (e_phi t))
+```
diff --git a/docs/docs/ru/getting-started/dependent-types.rzk.md b/docs/docs/ru/getting-started/dependent-types.rzk.md
new file mode 100644
index 000000000..0d0a0be1b
--- /dev/null
+++ b/docs/docs/ru/getting-started/dependent-types.rzk.md
@@ -0,0 +1,773 @@
+# Зависимые типы
+
+В этом разделе мы познакомимся с основами Rzk, позволяющими нам работать с зависимыми типам.
+
+!!! info "Источники"
+
+ Эта страница основана почти целиком на введении в зависимые типы
+ в «Гомотопической теории типов»[^1] [^2] (Sections 1.2–1.6),
+ и сразу вводит соответствующие формализации на Rzk,
+ указывая на некоторые различия между "книжной" теорией и решателем Rzk.
+
+Этот раздел является литературным файлом Rzk:
+
+```rzk
+#lang rzk-1
+```
+
+## Функции
+
+Запись `#!rzk (x : A) → B x` представляет тип (зависимых)
+функций с аргументом типа `A` и, для каждого входа `x`,
+результат типа `B x`.
+
+В качестве простого примера зависимой функции,
+рассмотрим тождественную функцию:
+
+```rzk
+#define identity
+ : ( A : U) → (x : A) → A
+ := \ A x → x
+```
+
+Поскольку мы не используем переменную `x` в _типе_ функции `identity`,
+мы можем упростить тип функции, указав для второго аргумента только тип (без имени аргумента):
+
+```rzk
+#define identity₁
+ : ( A : U) → A → A
+ := \ A x → x
+```
+
+Мы можем записать это же определение по-другому,
+переместив `#!rzk (A : U)` в _параметры_ определения (до `:`),
+при этом опуская этот аргумент в теле определения (после `:=`):
+
+```rzk
+#define identity₂
+ ( A : U)
+ : A → A
+ := \ x → x
+```
+
+В принципе, мы могли бы также переместить `x` в параметры,
+но вряд ли бы это повысило читаемость:
+
+```rzk
+#define identity₃
+ ( A : U)
+ ( x : A)
+ : A
+ := x
+```
+
+Другим, менее тривиальным примером зависимой функции,
+является функция меняющая порядок аргументов в любой заданной функции
+двух аргументов:
+
+```rzk
+#define swap
+ ( A B C : U)
+ : ( A → B → C) → (B → A → C)
+ := \ f → \ b a → f a b
+```
+
+## Типы-произведения
+
+Rzk не предоставляет встроенных типов-произведений,
+поскольку они являются частным случаем Σ-типов (зависимых пар),
+о которых мы поговорим в следующем подразделе.
+Но пока мы просто дадим определение типов-произведений:
+
+```rzk
+#define prod
+ ( A B : U)
+ : U
+ := Σ ( _ : A) , B
+```
+
+Запись `#!rzk prod A B` соответствует типу-произведению $A \times B$.
+Запись `#!rzk Unit` соответствует единичному типу $\mathbf{1}$.
+
+Элементами типа `#!rzk prod A B` предполагаются только пары `#!rzk (a, b) : prod A B`
+где `#!rzk a : A` и `#!rzk b : B`. Аналогично, единственным элементом `#!rzk Unit`
+предполагается `#!rzk unit`. Технически, теория типов не гарантирует, что эти типы состоят _только_
+из упомянутых элементов, но скоро мы сможем _доказать_, что это так.
+
+### Заметка о конструкторах типов
+
+Формально, каждый новый тип (конструктор типов) состоит из следующих компонентов.
+Мы показываем примеры для типов-произведений и функций для сравнения:
+
+1. **Правила формирования (конструирования) типов**:
+
+ - `#!rzk prod A B` — это тип, если `A` и `B` типы
+ - `#!rzk A → B` — это тип, если `A` и `B` типы
+
+2. **Конструкторы (правила введения)**:
+
+ - `#!rzk (x , y)` является термом (выражением) типа `#!rzk prod A B`, если `#!rzk x : A` и `#!rzk y : B`
+ - `#!rzk \ x → y` является термом (выражением) типа `#!rzk A → B`, если для любых `#!rzk x : A` верно, что `#!rzk y : B` (`y` здесь — это произвольное выражение, возможно, содержащее `x`)
+
+3. **Правила устранения**:
+
+ - Если `#!rzk z : prod A B`, то мы можем использовать _проекцию_ чтобы получить первый или второй компоненты:
+ - `#!rzk first z : A` и `#!rzk second z : B`
+ - мы также можем использовать _сопоставление с образцом_, когда вводим аргумент, например:
+
+ ```rzk
+ #define swap-prod₁
+ ( A B : U)
+ : prod A B → prod B A
+ := \ (x , y) → (y , x)
+
+ #define swap-prod₂
+ ( A B : U)
+ ( (x , y) : prod A B)
+ : prod B A
+ := ( y , x)
+ ```
+
+ - в общем случае, правила устранения записываются как _принцип индукции_, который мы обсудим ниже,
+ и может быть определён в Rzk через сопоставление с образцом или `#!rzk first` и `#!rzk second`:
+
+ ```rzk
+ #define ind-prod
+ ( A B : U)
+ ( C : prod A B → U)
+ ( f : (a : A) → (b : B) → C (a , b))
+ : (z : prod A B) → C z
+ := \ (a , b) → f a b
+ ```
+
+ - Если `#!rzk f : A → B`, мы можем _применить_ функцию к аргументу `#!rzk a : A`:
+ - `#!rzk f a : B`
+
+ !!! warning "Встроенные проекции в Rzk"
+
+ Встроенные проекции и правила устранения в Rzk должны быть применены _ко всем аргументам_
+ (например, `#!rzk first` без аргумента считается невалидным синтаксисом!).
+ Технически, это ограничение схоже со "вторым представлением" теории типов в Приложении A.2 книги [^1] [^2].
+ На практике, это не всего удобно, поскольку часто хочется исползовать каррированные варианты,
+ поэтому пользователи часто вводят обёртки над встроенными проекциями, например:
+
+ ```rzk
+ #define pr₁
+ ( A B : U)
+ : prod A B → A
+ := \ p → first p
+ ```
+
+4. **Правила вычисления**:
+
+ - Проекция из пары вычисляется следующим образом для любых `#!rzk x : A` and `#!rzk y : B`:
+ - `#!rzk first (x , y) ≡ x`
+ - `#!rzk second (x , y) ≡ y`
+ - Применение лямбда-функции к аргументу вычисляется при помощи подстановки аргумента в тело функции:
+ - `#!rzk (\ x → y) a ≡ y{x ↦ a}` when `#!rzk a : A` and for all `#!rzk x : A`, `#!rzk y : B`.
+
+5. **Принцип уникальности (опционально)**:
+
+ - Для любых `#!rzk z : prod A B`, верно `#!rzk z ≡ (first z, second z)`
+ - В Rzk это выполняется по определению для типов-произведений и Σ-типов, но в книге[^1] [^2] это можно доказать только в слабой (пропозициональной) форме.
+ - Для любой функции `#!rzk f : A → B` верно, что `#!rzk f ≡ \ x → f x`
+
+### Принцип рекурсии
+
+Следуя книге[^1] [^2], для каждого конструктора типов мы можем сформулировать _принцип рекурсии_.
+Принцип рекурсии для типа `#!rzk T` — это способ построить функцию
+в произвольный тип `#!rzk C` из типа `#!rzk T`:
+
+```{unchecked .rzk}
+#define rec-T
+ ( C : U)
+ -- ... (параметры принципа рекурсии)
+ : T → C
+```
+
+Например, для типа-произведения `#!rzk prod A B`, принцип рекурсии выглядит следующим образом:
+
+```rzk
+#define rec-prod
+ ( A B : U)
+ ( C : U)
+ ( f : A → B → C)
+ : prod A B → C
+ := \ ( a , b) → f a b
+```
+
+Для типа `#!rzk Unit`, принцип рекурсии тривиален:
+
+```rzk
+#define rec-Unit
+ ( C : U)
+ ( c : C)
+ : Unit → C
+ := \ unit → c
+```
+
+### Принцип индукции
+
+Чтобы определить _зависимую_ функцию из типа, необходим _принцип индукции_,
+который можно рассматривать как зависимый вариант принципа рекурсии.
+Принцип индукции для типа `#!rzk T` — это способ (функция), позволяющий
+построить функцию в тип `#!rzk C z` для каждого входа `#!rzk z : T`:
+
+```{unchecked .rzk}
+#define ind-T
+ ( C : T → U)
+ -- ... (параметры принципа индукции)
+ : (z : T) → C z
+```
+
+Например, для типа-произведения `#!rzk prod A B`, принцип индукции выглядит так:
+
+```rzk
+#define ind-prod
+ ( A B : U)
+ ( C : prod A B → U)
+ ( f : (a : A) → (b : B) → C (a , b))
+ : ( z : prod A B) → C z
+ := \ ( a , b) → f a b
+```
+
+Мы можем использовать `#!rzk ind-prod` для доказательства принципа уникальности.
+Тут мы используем тип-тождество, который обсудим позже. Пока нам достаточно знать,
+что для любого `#!rzk x : A` всегда можно построить элемент`#!rzk refl_{x}` типа `x =_{A} x`.
+
+```rzk
+#define uniq-prod
+ ( A B : U)
+ ( z : prod A B)
+ : ( first z , second z) =_{prod A B} z
+ := ind-prod A B
+ ( \ z' → (first z' , second z') =_{prod A B} z') -- C
+ ( \ a b → refl_{(a , b)})
+ -- C (a, b)
+ -- ≡ ( \ z' → (first z', second z') =_{prod A B} z') (a, b)
+ -- ≡ (first (a, b), second (a, b)) =_{prod A B} (a, b)
+ -- ≡ (a, second (a, b)) =_{prod A B} (a, b)
+ -- ≡ (a, b) =_{prod A B} (a, b)
+ z
+```
+
+Поскольку принцип уникальности уже встроен в Rzk, более простое доказательство также подойдёт:
+
+```rzk
+#define uniq-prod'
+ ( A B : U)
+ ( z : prod A B)
+ : ( first z , second z) =_{prod A B} z
+ := refl_{z} -- работает в Rzk, но не в книжном HoTT, поскольку в Rzk верно (first z, second z) ≡ z
+```
+
+Для единичного типа `#!rzk Unit` принцип индукции выглядит просто:
+
+```rzk
+#define ind-Unit
+ ( C : Unit → U)
+ ( c : C unit)
+ : ( z : Unit) → C z
+ := \ unit → c
+```
+
+В отличие от `#!rzk rec-Unit`, принцип индукции для `#!rzk Unit` не бесполезен,
+поскольку он позволяет доказать принцип уникальности для единичного типа:
+
+```rzk
+#define uniq-Unit
+ ( z : Unit)
+ : unit =_{Unit} z
+ := ind-Unit
+ ( \ z' → unit =_{Unit} z')
+ ( refl_{unit})
+ z
+```
+
+Опять же, поскольку принцип уникальности уже встроен в Rzk, более простое доказательство также сработает:
+
+```rzk
+#define uniq-Unit'
+ ( z : Unit)
+ : unit =_{Unit} z
+ := refl_{z} -- работает в Rzk, но не в книжном HoTT, поскольку в Rzk верно unit ≡ z
+```
+
+## Зависимые пары (Σ-типы)
+
+Σ-типы являются обобщением типов-произведений и позволяют типу второго элемента зависеть от значения первого.
+Запись `#!rzk Σ (a : A), B a` соответствует типу зависимых пар, где
+`#!rzk A` тип и `#!rzk B : A → U` семество типов, индексируемое в типе `#!rzk A`.
+
+Предполагаемыми элементами типа `#!rzk Σ (a : A), B a` являются пары `#!rzk (a , b)`
+термов `#!rzk a : A` и `#!rzk b : B a`. Заметьте, что тип второго терма
+может зависеть от значения первого.
+Если семейство типов `#!rzk B` константное, например `#!rzk (\ _ → C)`,
+то `#!rzk Σ (a : A), B a` становится в точности типов-произведением `#!rzk prod A C`.
+
+Для устранения зависимых пар, мы используем `#!rzk first`, `#!rzk second`,
+или сопоставление с образцом для пар.
+Однако, типы проекций в этом случае не такие очевидные, как для типов-произведений.
+
+### Проекции
+
+Первая проекция может быть легко определена через сопоставление с образцом:
+
+```rzk
+#define pr₁
+ ( A : U)
+ ( B : A → U)
+ : ( Σ ( a : A) , B a) → A
+ := \ ( a , _) → a
+```
+
+Однако, для определения второй проекции нужна осторожность. В частности, следующее определение не сработает:
+
+```{unchecked .rzk}
+-- NOTE: incorrect definition
+#define pr₂
+ ( A : U)
+ ( B : A → U)
+ : (Σ (a : A), B a) → B a -- ОШИБКА ТИПОВ!
+ := \ (_ , b) → b
+```
+
+```
+undefined variable: a
+```
+
+Мы получили ошибку `undefined variable` (неизвестная переменная), поскольку переменная `a` не видна снаружи определения Σ-типа.
+Для доступа к первой компоненте зависимой пары, нам нужно использовать первую проекцию:
+
+```rzk
+#define pr₂
+ ( A : U)
+ ( B : A → U)
+ : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
+ := \ ( _ , b) → b
+```
+
+Иногда о Σ-типах удобнее говорить как о тотальных (общих?) типах (аналогично "total spaces"):
+
+```rzk
+#define total-type
+ ( A : U)
+ ( B : A → U)
+ : U
+ := Σ ( a : A) , B a
+```
+
+Мы можем переписать более компактно определение второй проекции,
+используя сопоставление с образцом в параметрах, и используя `#!rzk total-type`:
+
+```rzk
+#define pr₂'
+ ( A : U)
+ ( B : A → U)
+ ( ( a , b) : total-type A B)
+ : B a
+ := b
+```
+
+### Принципи рекурсии и индукции
+
+Принцип рекурсии для Σ-типов простым образом общает
+соответствующий принцип для типов-произведений:
+
+```rzk
+#define rec-Σ
+ ( A : U)
+ ( B : A → U)
+ ( C : U)
+ ( f : (a : A) → B a → C)
+ : total-type A B → C
+ := \ ( a , b) → f a b
+```
+
+Аналогично с принципом индукции:
+
+```rzk
+#define ind-Σ
+ ( A : U)
+ ( B : A → U)
+ ( C : total-type A B → U)
+ ( f : (a : A) → (b : B a) → C (a , b))
+ : ( z : total-type A B) → C z
+ := \ ( a , b) → f a b
+```
+
+Как и раньше, мы можем использовать `#!rzk ind-Σ` для доказательства принципа уникальности,
+теперь для Σ-типов:
+
+```rzk
+#define uniq-Σ
+ ( A : U)
+ ( B : A → U)
+ ( z : total-type A B)
+ : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
+ := ind-Σ A B
+ ( \ z → (pr₁ A B z , pr₂ A B z) =_{total-type A B} z)
+ ( \ a b → refl_{(a , b)})
+ z
+```
+
+И опять же, Rzk допускает более простое доказательство,
+поскольку уникальность для Σ-типов встроена в решатель:
+
+```rzk
+#define uniq-Σ'
+ ( A : U)
+ ( B : A → U)
+ ( z : total-type A B)
+ : ( pr₁ A B z , pr₂ A B z) =_{total-type A B} z
+ := refl_{z} -- работает в Rzk, но не в книжном HoTT
+```
+
+### Теоретико-типовая "аксима" выбора
+
+Используя принцип индукции `#!rzk ind-Σ`
+мы можем _доказать_ версию аксиомы выбора в теории типов:
+
+```rzk
+#define AxiomOfChoice
+ : U
+ := ( A : U)
+ → ( B : U)
+ → ( R : A → B → U)
+ → ( ( x : A) → Σ (y : B) , R x y)
+ → ( Σ ( f : A → B) , (x : A) → R x (f x))
+```
+
+Читалю предлагается попробовать доказать это утверждение самостоятельно:
+
+```{unchecked .rzk}
+#define axiom-of-choice
+ : AxiomOfChoice
+ := ...
+```
+
+При возникновении проблем с доказательством, вы можете обратиться к разделу 1.6 (стр. 32) в книге[^1] [^2].
+
+Если всё ещё остануться проблемы при формализации доказательства в Rzk, можете подсмотреть решение здесь:
+
+??? abstract "Доказательство теоретико-типовой аксиомы выбора"
+
+ ```rzk
+ #define ac : AxiomOfChoice
+ := \ A B R g → ( \ a → first (g a) , \ x → second (g x))
+ -- g : (x : A) → Σ (y : B), R x y
+ -- x : A
+ -- g x : Σ (y : B), R x y
+ -- second (g x) : R x (first (g x))
+
+ -- f : A → B
+ -- f := \ a → first (g a)
+ --
+ -- R x (f x)
+ -- == R x ((\ a → first (g a)) x)
+ -- == R x (first (g x))
+ ```
+
+## Копроизведения (суммы типов)
+
+Для типов $A$ и $B$, тип $A + B$ соответствует
+(интуитивно) дизъюнктивному объединению $A$ и $B$ (при интерпретации в теории множеств).
+Для полноты также разумно предположить наличие пустого типа: $\mathbf{0}$.
+
+В Rzk, пустой тип и типы-копроизведения не встроены, но мы, тем не менее,
+можем постулировать их в более слабой форме.
+
+### Пустой тип (постулированный)
+
+Например, мы можем постулировать пустой тип следующим образом:
+
+```rzk
+#postulate Void
+ : U
+#postulate ind-Void
+ ( C : Void → U)
+ : ( z : Void) → C z
+```
+
+Поскольку мы предполагаем, что в пустом типе `#!rzk Void` не должно быть элементов,
+принцип индукции соответсвует принципу абсурности (из лжи следует что угодно).
+Простая (не зависимая) версия этого принципа будет принципом рекурсии,
+который мы можем реализовать через `#!rzk ind-Void`:
+
+```rzk
+#define rec-Void
+ ( C : U)
+ : Void → C
+ := ind-Void (\ _ → C)
+```
+
+### Тип-копроизведение (постулированный)
+
+!!! warning "Постулированный тип"
+
+ В этом подразделе представлен только постулированный тип
+ без достаточных пояснений.
+ Как только Rzk обзаведётся поддержой пользовательстких (высших) индуктивных типов
+ или встроенными типами-копроизведениями, этот подраздел будет обновлён.
+
+Аналогично, мы можем постулировать типы-копроизведения:
+
+```rzk
+#postulate coprod
+ ( A B : U)
+ : U
+```
+
+Существует два способа построить элемент типа `#!rzk coprod A B` —
+ввести терм из типа `#!rzk A` или из типа `#!rzk B`:
+
+```rzk
+#postulate inl
+ ( A B : U)
+ : A → coprod A B
+#postulate inr
+ ( A B : U)
+ : B → coprod A B
+```
+
+Чтбы устранить копроизведение, мы должны предоставить два обработчика —
+один на случай, если в копроизведении хранится левое значение,
+и один на случай правого значения:
+
+```rzk
+#postulate ind-coprod
+ ( A B : U)
+ ( C : coprod A B → U)
+ ( l : (a : A) → C (inl A B a))
+ ( r : (b : B) → C (inr A B b))
+ : ( z : coprod A B) → C z
+```
+
+Поскольку мы постулируем принцип индукции,
+мы также должны предоставить правила вычисления явно.
+Однако, Rzk позволяет нам постулировать только _пропозициональные_ правила:
+
+```rzk
+#postulate ind-coprod-inl
+ ( A B : U)
+ ( C : coprod A B → U)
+ ( l : (a : A) → C (inl A B a))
+ ( r : (b : B) → C (inr A B b))
+ ( a : A)
+ : ind-coprod A B C l r (inl A B a) = l a
+
+#postulate ind-coprod-inr
+ ( A B : U)
+ ( C : coprod A B → U)
+ ( l : (a : A) → C (inl A B a))
+ ( r : (b : B) → C (inr A B b))
+ ( b : B)
+ : ind-coprod A B C l r (inr A B b) = r b
+```
+
+Теперь мы можем определить принцип рекурсии для копроизведений
+как частный случай индукции:
+
+```rzk
+#define rec-coprod
+ ( A B : U)
+ ( C : U)
+ ( l : A → C)
+ ( r : B → C)
+ : coprod A B → C
+ := ind-coprod A B (\ _ → C) l r
+```
+
+Принцип уникальности для копроизвдений
+гласит, что любое значение в типе-копроизведении
+должно быть либо `#!rzk inl`, либо `#!rzk inr`.
+Доказательство принципа уникальности относительно простое,
+однако Rzk требует явно расписать все промежуточные типы:
+
+```rzk
+#define uniq-coprod
+ ( A B : U)
+ ( z : coprod A B)
+ : coprod
+ ( Σ ( a : A) , inl A B a = z)
+ ( Σ ( b : B) , inr A B b = z)
+ := ind-coprod A B
+ ( \ z' → coprod
+ ( Σ ( a : A) , inl A B a = z')
+ ( Σ ( b : B) , inr A B b = z'))
+ ( \ a' → inl
+ ( Σ ( a : A) , (inl A B a = inl A B a'))
+ ( Σ ( b : B) , (inr A B b = inl A B a'))
+ ( a' , refl))
+ ( \ b' → inr
+ ( Σ ( a : A) , (inl A B a = inr A B b'))
+ ( Σ ( b : B) , (inr A B b = inr A B b'))
+ ( b' , refl))
+ z
+```
+
+## Booleans
+
+!!! warning "Постулированный тип"
+
+ В этом подразделе представлен только постулированный тип
+ без достаточных пояснений.
+ Как только Rzk обзаведётся поддержой пользовательстких (высших) индуктивных типов
+ или встроенным булевым типом, этот подраздел будет обновлён.
+
+```rzk
+#postulate Bool
+ : U
+#postulate false
+ : Bool
+#postulate true
+ : Bool
+```
+
+```rzk
+#postulate ind-Bool
+ ( C : Bool → U)
+ ( f : C false)
+ ( t : C true)
+ : ( z : Bool) → C z
+```
+
+```rzk
+#postulate ind-Bool-false
+ ( C : Bool → U)
+ ( f : C false)
+ ( t : C true)
+ : ind-Bool C f t false = f
+#postulate ind-Bool-true
+ ( C : Bool → U)
+ ( f : C false)
+ ( t : C true)
+ : ind-Bool C f t true = t
+```
+
+```rzk
+#define rec-Bool
+ ( C : U)
+ ( f t : C)
+ : Bool → C
+ := ind-Bool (\ _ → C) f t
+```
+
+```rzk
+#define uniq-Bool
+ ( z : Bool)
+ : coprod (z = false) (z = true)
+ := ind-Bool
+ ( \ z' → coprod (z' = false) (z' = true))
+ ( inl (false = false) (false = true) refl)
+ ( inr (true = false) (true = true) refl)
+ z
+```
+
+```rzk
+#define not
+ : Bool → Bool
+ := rec-Bool Bool true false
+```
+
+К сожалению, поскольку правила вычисления постулированы
+только в слабой форме, они не вычисляются автоматически
+и нам необходимо использовать их явно.
+Поэтому, следующее доказательство не работает в Rzk:
+
+```{unchecked .rzk}
+#define not-not-is-identity
+ : (z : Bool) → not (not z) = z
+ := ind-Bool
+ ( \ z → not (not z) = z)
+ ( refl) -- ОШИБКА ТИПОВ! не работает из-за отсутствия "сильных" правил вычисления
+ ( refl) -- ОШИБКА ТИПОВ! не работает из-за отсутствия "сильных" правил вычисления
+```
+
+Доказательство можно построить, используя индукцию по типам-тождествам,
+но пока у нас недостаточно знаний, чтобы этого добиться.
+
+## Natural numbers
+
+!!! warning "Постулированный тип"
+
+ В этом подразделе представлен только постулированный тип
+ без достаточных пояснений.
+ Как только Rzk обзаведётся поддержой пользовательстких (высших) индуктивных типов
+ или встроенным типом натуральных чисел, этот подраздел будет обновлён.
+
+```rzk
+#postulate ℕ
+ : U
+#postulate zero
+ : ℕ
+#postulate succ (n : ℕ)
+ : ℕ
+
+#postulate ind-ℕ
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : ( n : ℕ) → C n
+
+#postulate ind-ℕ-zero
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : ind-ℕ C base step zero = base
+#postulate ind-ℕ-succ
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ ( n : ℕ)
+ : ind-ℕ C base step (succ n) = step n (ind-ℕ C base step n)
+```
+
+```rzk
+#define rec-ℕ
+ ( C : U)
+ ( base : C)
+ ( step : (n : ℕ) → C → C)
+ : ℕ → C
+ := ind-ℕ (\ _ → C) base step
+```
+
+```rzk
+#define double-ℕ
+ : ℕ → ℕ
+ := rec-ℕ ℕ zero (\ _ m → succ (succ m))
+```
+
+```rzk
+#define compute-ind-ℕ-zero
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : C zero
+ := base
+
+#define compute-ind-ℕ-one
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : C (succ zero)
+ := step zero (compute-ind-ℕ-zero C base step)
+
+#define compute-ind-ℕ-two
+ ( C : ℕ → U)
+ ( base : C zero)
+ ( step : (n : ℕ) → C n → C (succ n))
+ : C (succ (succ zero))
+ := step (succ zero) (compute-ind-ℕ-one C base step)
+
+#compute compute-ind-ℕ-two (\ _ → ℕ) zero (\ _ m → succ (succ m))
+```
+
+[^1]:
+ The Univalent Foundations Program. _Homotopy Type Theory: Univalent Foundations of Mathematics_.
+ Institute for Advanced Study. 2013.
+
+[^2]:
+ Международный коллектив авторов. _Гомотопическая теория типов: унивалентные основания математики_.
+ ИНСТИТУТ ПЕРСПЕКТИВНЫХ ИССЛЕДОВАНИЙ. Перевод и редактирование: ГЕННАДИЙ ЧЕРНЫШЕВ.
+
diff --git a/docs/docs/ru/getting-started/install.md b/docs/docs/ru/getting-started/install.md
new file mode 100644
index 000000000..caaf66928
--- /dev/null
+++ b/docs/docs/ru/getting-started/install.md
@@ -0,0 +1,107 @@
+# Установка Rzk
+
+## Через расширение VS Code (рекомендуется)
+
+Следуйте этим инструкциям, чтобы настроить работу с Rzk в редакторе VS Code.
+
+1. Установите [VS Code](https://code.visualstudio.com/).
+2. Запустите VS Code и установите [расширение `rzk`](https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting).
+3. Создайте новый файл через "Файл > Создать текстовый файл" (Ctrl+N ). Нажмите `Select a language`, введите в поиске `rzk` и выберите "Literate Rzk Markdown".
+ ![VS Code rzk language selector.](../assets/images/vscode-rzk-select-language.png)
+4. Вы должны увидеть следующее сообщение:
+ ![VS Code rzk install prompt.](../assets/images/vscode-rzk-install-prompt.png)
+5. Нажмите "Yes".
+6. Пока Rzk устанавливается, скопируйте и вставьте следующий текст в открытый файл:
+
+ ````markdown
+ # Пример литературного кода с Rzk
+
+ ```rzk
+ #lang rzk-1
+
+ -- тождественная функция
+ #define id (A : U)
+ : A -> A
+ := \ x -> x
+ ```
+ ````
+
+7. Когда установка завершится, вы должны увидеть следующее сообщение:
+ ![VS Code rzk reload prompt.](../assets/images/vscode-rzk-install-success-reload-prompt.png)
+8. Нажмите "Reload" (перезагрузить VS Code).
+9. Сохраните ваш файл (например, как `example.rzk.md`).
+10. Откройте терминал внутри VS Code (Ctrl+` ).
+
+
+
+11. В терминале запустите команду
+
+ ```sh
+ rzk typecheck example.rzk.md
+ ```
+
+12. Вы должны увидеть что-то такое:
+
+ ```text
+ Loading file example.rzk.md
+ Checking module from example.rzk.md
+ [ 1 out of 1 ] Checking #define id
+ Everything is ok!
+ ```
+
+13. Поздравляем! Теперь ваш VS Code настроен на работу с Rzk :) Заметьте, что расширение будет уведомлять вас о наличии обновлений Rzk и предлагать обновить автоматически.
+
+14. Можете перейти к [Быстрому началу](quickstart.rzk.md) чтобы познакомиться с языком Rzk!
+
+## Установка исполняемых файлов
+
+### Через страницу релизов на GitHub
+
+Вы можете скачать исполняемые файлы (для Linux, Windows, и macOS) напрямую со страницы релизов на GitHub: .
+Если ваша платформа не поддержана, вы можете попробовать установить Rzk из исходников (см. ниже)
+или оставить пожелание о расширении поддержки на странице задач: .
+
+## Сборка и установка из исходников
+
+Вы можете установить Rzk из исходников: вы можете либо скачать стабильную версию из репозитория пакетов Hackage, либо собрать самую свежую версию из ветки `develop` на GitHub.
+
+### Stack
+
+Чтобы собрать и установить Rzk при помощи Stack, из репозитория Hackage:
+
+```sh
+stack install rzk
+```
+
+Чтобы собрать и установить Rzk при помощи Stack, из исходников на GitHub:
+
+```sh
+git clone https://github.com/rzk-lang/rzk.git
+cd rzk
+git checkout develop
+stack build && stack install
+```
+
+### cabal-install
+
+Чтобы собрать и установить Rzk при помощи `cabal-install`, из репозитория Hackage:
+
+```sh
+cabal v2-update
+cabal v2-install rzk
+```
+
+Чтобы собрать и установить Rzk при помощи `cabal-install`, из исходников на GitHub:
+
+```sh
+git clone https://github.com/rzk-lang/rzk.git
+cd rzk
+git checkout develop
+cabal v2-build && cabal v2-install
+```
+
+### Nix
+
+!!! warning "Раздел в работе."
+
+ Раздел нуждается в доработке.
diff --git a/docs/docs/ru/getting-started/project.md b/docs/docs/ru/getting-started/project.md
new file mode 100644
index 000000000..927c75090
--- /dev/null
+++ b/docs/docs/ru/getting-started/project.md
@@ -0,0 +1,6 @@
+# Настройка проекта
+
+!!! warning "Раздел в работе"
+ Скоро здесь будет описание работы с проектами формализации.
+ До тех пор вы можете воспользоваться шаблонным проектом: .
+ Также см. для примера реального проекта.
diff --git a/docs/docs/ru/getting-started/quickstart.rzk.md b/docs/docs/ru/getting-started/quickstart.rzk.md
new file mode 100644
index 000000000..0921404ef
--- /dev/null
+++ b/docs/docs/ru/getting-started/quickstart.rzk.md
@@ -0,0 +1,12 @@
+# Быстрое начало
+
+!!! warning "Раздел в работе"
+ Этот раздел нуждается в доработке.
+
+Для начала, [установите Rzk](install.md).
+
+Этот раздел является литературным файлом Rzk:
+
+```rzk
+#lang rzk-1
+```
diff --git a/docs/docs/ru/index.md b/docs/docs/ru/index.md
new file mode 100644
index 000000000..9bfca47e7
--- /dev/null
+++ b/docs/docs/ru/index.md
@@ -0,0 +1,84 @@
+# Решатель теорем Rzk
+
+Rzk — это экспериментальный интерактивный решатель теорем,
+основанный на [«Теории типов для синтетических ∞-категорий](https://arxiv.org/abs/1705.07442)[^1].
+
+[Первые шаги с Rzk](getting-started/install.md){ .md-button .md-button--primary }
+[Попробовать Rzk в онлайн-песочнице](playground/index.html){ .md-button }
+
+## Об этом проекте
+
+Проект начался с идеи воплотить "в жизнь" статью Эмили Рил и Майкла Шульмана 2017 года[^1],
+реализуя решатель для их теории типов с формами (type theory with shapes).
+На момент написания этого текста, Rzk поддерживает формальный язык, близкий к теории типов в упомянутой статье,
+а также вокруг решателя существует некая инструментальная поддержка
+(например, расширение для VS Code и языковой сервер с поддержкой подсветки синтаксиса и автоформатирования).
+
+### Формализация теории ∞-категорий
+
+Большая часть статьи Рил и Шульмана (вплоть до леммы Йонеды для ∞-категорий) уже формализована на Rzk (см. [Yoneda for ∞-categories](https://emilyriehl.github.io/yoneda/)[^2]).
+Оставшие результаты, а также результаты из других работ находятся в процессе формализации (см. проект по формализации симплициальной гомопотической теории типов, [sHoTT](https://rzk-lang.github.io/sHoTT/)).
+Также некоторые усилия направлены на формализацию "книжной"[^6] [^7] гомотопической теории типов (см. [hottbook](https://rzk-lang.github.io/hottbook/)).
+
+### Работа с Rzk
+
+Рекомендуемый способ работы с Rzk — через среду разработки VS Code (см. [Первые шаги](getting-started/install.md)).
+Тем не менее, вы также можете скачать исполняемые файлы на [странице релизов на GitHub](https://github.com/rzk-lang/rzk/releases),
+собрать самостоятельно [из исходников](getting-started/install.md#install-from-sources),
+а также попытаться интегрировать языковой сервер Rzk с вашим любимым текстовым редактором.
+Для небольших формализаций, умещающихся в один файл, можно также воспользоваться [онлайн-песочницей Rzk](playground/index.html).
+
+### Реализация
+
+Помимо своей основной цели, Rzk также служит полем экспериментов для методов реализации решателей теорем (на языке Haskell).
+В частности, в реализации используется вариант абстрактного синтаксиса второго порядка
+для комфортной работы со связанными переменными и, в будущем, для вывода (зависимых) типов
+через унификацию высшего порядка[^3] [^4].
+В конечном итоге, хочется получить приемлемое общее (библиотечное) решение для унификации высшего порядка и вывода типов,
+оставив реализацию Rzk (по крайней мере, его ядра) небольшим, простым для поддержки, и надёжным.
+
+Ещё одна интересная деталь реализации Rzk — это автоматический решатель для слоя форм (tope layer)[^5].
+Это встроенный полностью автоматический решатель для варианта интуиционистской логики,
+необходимый для проверки типов.
+Хотя текущая реализация решателя относительно проста,
+её хватает на практике для проверки доказательств о синтетических ∞-категориях
+без нужды в дополнительном коде от формализующего математика.
+
+Rzk и сопутствующие инструменты разработаны всего парой человек.
+Вы можете ознакомится с участниками проекта в файле [CONTRIBUTORS.md](CONTRIBUTORS.md).
+
+### Обсуждения вокруг Rzk
+
+Для всех желающих доступен (преимущественно англоязычный) чат Zulip,
+в котором можно обсудить формализации, разработку Rzk и смежные проекты:
+
+[Присоединиться к сообществу Rzk в Zulip](https://rzk-lang.zulipchat.com/register/){ .md-button .md-button--primary }
+
+[^1]:
+ Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories_.
+ Higher Structures 1(1), 147-224. 2017.
+
+[^2]:
+ Nikolai Kudasov, Emily Riehl, Jonathan Weinberger.
+ _Formalizing the ∞-categorical Yoneda lemma_. 2023.
+
+[^3]:
+ Nikolai Kudasov. _Functional Pearl: Dependent type inference via free higher-order unification_. 2022.
+
+
+[^4]:
+ Nikolai Kudasov. _E-Unification for Second-Order Abstract Syntax_. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 10:1-10:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
+
+
+[^5]:
+ Nikolai Kudasov. Experimental prover for Tope logic. SCAN 2023, pages 37–39. 2023.
+
+
+[^6]:
+ The Univalent Foundations Program. _Homotopy Type Theory: Univalent Foundations of Mathematics_.
+ Institute for Advanced Study. 2013.
+
+[^7]:
+ Международный коллектив авторов. _Гомотопическая теория типов: унивалентные основания математики_.
+ ИНСТИТУТ ПЕРСПЕКТИВНЫХ ИССЛЕДОВАНИЙ. Перевод и редактирование: ГЕННАДИЙ ЧЕРНЫШЕВ.
+
diff --git a/docs/docs/ru/playground/index.html b/docs/docs/ru/playground/index.html
new file mode 100644
index 000000000..2edf06ccc
--- /dev/null
+++ b/docs/docs/ru/playground/index.html
@@ -0,0 +1,16 @@
+
+
+
+
+ Redirecting
+
+
+
+ Redirecting...
+
+
diff --git a/docs/docs/ru/reference/builtins/directed-interval.rzk.md b/docs/docs/ru/reference/builtins/directed-interval.rzk.md
new file mode 100644
index 000000000..e69de29bb
diff --git a/docs/docs/ru/reference/builtins/unit.rzk.md b/docs/docs/ru/reference/builtins/unit.rzk.md
new file mode 100644
index 000000000..bb2335b72
--- /dev/null
+++ b/docs/docs/ru/reference/builtins/unit.rzk.md
@@ -0,0 +1,64 @@
+# Unit type
+
+Since [:octicons-tag-24: v0.5.1][Unit support]
+
+```rzk
+#lang rzk-1
+```
+
+In the syntax, only `Unit` (the type) and `unit` (the only inhabitant) are provided. Everything else should be available from computation rules.
+More specifically, `rzk` takes the uniqueness property of the `Unit` type (see Section 1.5 of the HoTT book[^1]) as the computation rule, meaning that any (well-typed) term of type `Unit` reduces to `unit`.
+This means in particular, that induction and uniqueness can be defined very easily:
+
+```rzk
+#define ind-Unit
+ (C : Unit -> U)
+ (C-unit : C unit)
+ (x : Unit)
+ : C x
+ := C-unit
+
+#define uniq-Unit
+ (x : Unit)
+ : x = unit
+ := refl
+
+#define isProp-Unit
+ (x y : Unit)
+ : x = y
+ := refl
+```
+
+As a non-trivial example, here is a proof that `Unit` is a Segal type:
+
+```rzk
+#section isSegal-Unit
+
+#variable extext : ExtExt
+
+#define iscontr-Unit : isContr Unit
+ := (unit, \_ -> refl)
+
+#define isContr-Δ²→Unit uses (extext)
+ : isContr (Δ² -> Unit)
+ := (\_ -> unit, \k -> eq-ext-htpy extext
+ (2 * 2) Δ² (\_ -> BOT)
+ (\_ -> Unit) (\_ -> recBOT)
+ (\_ -> unit) k
+ (\_ -> refl)
+ )
+
+#define isSegal-Unit uses (extext)
+ : isSegal Unit
+ := \x y z f g -> isRetract-ofContr-isContr
+ (∑ (h : hom Unit x z), hom2 Unit x y z f g h)
+ (Δ² -> Unit)
+ (\(_, k) -> k, (\k -> (\t -> k (t, t), k), \_ -> refl))
+ isContr-Δ²→Unit
+
+#end isSegal-Unit
+```
+
+[Unit support]: https://github.com/rzk-lang/rzk/releases/tag/v0.5.1
+
+[^1]: The Univalent Foundations Program (2013). _Homotopy Type Theory: Univalent Foundations of Mathematics._
diff --git a/docs/docs/ru/reference/commands/check.rzk.md b/docs/docs/ru/reference/commands/check.rzk.md
new file mode 100644
index 000000000..e69de29bb
diff --git a/docs/docs/ru/reference/commands/compute.rzk.md b/docs/docs/ru/reference/commands/compute.rzk.md
new file mode 100644
index 000000000..e69de29bb
diff --git a/docs/docs/ru/reference/commands/define-postulate.rzk.md b/docs/docs/ru/reference/commands/define-postulate.rzk.md
new file mode 100644
index 000000000..e69de29bb
diff --git a/docs/docs/ru/reference/commands/options.rzk.md b/docs/docs/ru/reference/commands/options.rzk.md
new file mode 100644
index 000000000..e69de29bb
diff --git a/docs/docs/ru/reference/cube-layer.rzk.md b/docs/docs/ru/reference/cube-layer.rzk.md
new file mode 100644
index 000000000..fe5f54e79
--- /dev/null
+++ b/docs/docs/ru/reference/cube-layer.rzk.md
@@ -0,0 +1,28 @@
+# Cube layer
+
+```rzk
+#lang rzk-1
+```
+
+All cubes live in `#!rzk CUBE` universe.
+
+There are two built-in cubes:
+
+1. `#!rzk 1` cube is a unit cube with a single point `#!rzk *_1`
+2. `#!rzk 2` cube is a [directed interval](builtins/directed-interval.rzk.md) cube with points `#!rzk 0_2` and `#!rzk 1_2`
+
+It is also possible to have `#!rzk CUBE` variables and make products of cubes:
+
+1. `#!rzk I * J` is a product of cubes `#!rzk I` and `#!rzk J`
+2. `#!rzk (t, s)` is a point in `#!rzk I * J` if `#!rzk t : I` and `#!rzk s : J`
+3. if `#!rzk ts : I * J`, then `#!rzk first ts : I` and `#!rzk second ts : J`
+
+You can usually use `#!rzk (t, s)` both as a pattern, and a construction of a pair of points:
+
+```rzk
+-- Swap point components of a point in a cube I × I
+#define swap
+ ( I : CUBE)
+ : ( I × I) → I × I
+ := \ ( t , s) → (s , t)
+```
diff --git a/docs/docs/ru/reference/extension-types.rzk.md b/docs/docs/ru/reference/extension-types.rzk.md
new file mode 100644
index 000000000..f2b3f5d44
--- /dev/null
+++ b/docs/docs/ru/reference/extension-types.rzk.md
@@ -0,0 +1,17 @@
+# Extension types
+
+
+4. Extension types \(\left\langle \prod_{t : I \mid \psi} A \vert ^{\phi} _{a} \right\rangle\) are written as `#!rzk {t : I | psi t} -> A [ phi |-> a ]`
+ - specifying `#!rzk [ phi |-> a ]` is optional, semantically defaults to `#!rzk [ BOT |-> recBOT ]` (like in RSTT);
+ - specifying `#!rzk psi` in `#!rzk {t : I | psi}` is mandatory;
+ - values of function types are \(\lambda\)-abstractions written in one of the following ways:
+ - `#!rzk \t -> ` — this is usually fine;
+ - `#!rzk \{t : I | psi} -> ` — this sometimes helps the typechecker;
+
+5. Types of functions from a shape \(\prod_{t : I \mid \psi} A\) are a specialised variant of extension types and are written `#!rzk {t : I | psi} -> A`
+ - specifying the name of the argument is mandatory; i.e. `#!rzk {I | psi} -> A` is invalid syntax!
+ - values of function types are \(\lambda\)-abstractions written in one of the following ways:
+ - `#!rzk \t -> ` — this is usually fine;
+ - `#!rzk \{t : I | psi} -> ` — this sometimes helps the typechecker;
+
+[^1]: Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories._ Higher Structures 1(1), 147-224. 2017.
diff --git a/docs/docs/ru/reference/introduction.rzk.md b/docs/docs/ru/reference/introduction.rzk.md
new file mode 100644
index 000000000..a399a27cc
--- /dev/null
+++ b/docs/docs/ru/reference/introduction.rzk.md
@@ -0,0 +1,72 @@
+# Introduction
+
+`rzk` is an experimental proof assistant for synthetic ∞-categories.
+`rzk-1` is an early version of the language supported by `rzk`.
+The language is based on Riehl and Shulman's «Type Theory for Synthetic ∞-categories»[^1]. In this section, we introduce syntax, discuss features and some of the current limitations of the proof assistant.
+
+Overall, a program in `rzk-1` consists of a language pragma (specifying that we use `rzk-1` and not one of the other languages[^2]) followed by a sequence of commands. For now, we will only use `#define` command.
+
+Here is a small formalisation in an MLTT subset of `rzk-1`:
+
+```rzk
+#lang rzk-1
+
+-- Flipping the arguments of a function.
+#define flip
+ (A B : U) -- For any types A and B
+ (C : (x : A) -> (y : B) -> U) -- and a type family C
+ (f : (x : A) -> (y : B) -> C x y) -- given a function f : A -> B -> C
+ : (y : B) -> (x : A) -> C x y -- we construct a function of type B -> A -> C
+ := \y x -> f x y -- by swapping the arguments
+
+-- Flipping a function twice is the same as not doing anything
+#define flip-flip-is-id
+ (A B : U) -- For any types A and B
+ (C : (x : A) -> (y : B) -> U) -- and a type family C
+ (f : (x : A) -> (y : B) -> C x y) -- given a function f : A -> B -> C
+ : f = flip B A (\y x -> C x y)
+ (flip A B C f) -- flipping f twice is the same as f
+ := refl -- proof by reflexivity
+```
+
+Let us explain parts of this code:
+
+1. `#!rzk #lang rzk-1` specifies that we are in using `#!rzk rzk-1` language;
+2. `#!rzk --` starts a comment line (until the end of the line);
+3. `#!rzk #define «name» : «type» := «term»` defines a name `«name»` to be equal to `«term»`; the proof assistant will typecheck `«term»` against type `«type»`;
+4. We define two terms here — `flip` and `flip-flip-is-id`;
+5. `flip` is a function that takes 4 arguments and returns a function of two arguments.
+6. `flip-flip-is-id` is a function that takes two types, a type family, and a function `f` and returns a value of an identity type `flip ... (flip ... f) = f`, indicating that flipping a function `f` twice gets us back to `f`.
+
+Similarly to the three layers in Riehl and Shulman's type theory, `rzk-1` has 3 universes:
+
+- `CUBE` is the universe of cubes, corresponding to the cube layer;
+- `TOPE` is the universe of topes, corresponding to the tope layer;
+- `U` is the universe of types, corresponding to the types and terms layer.
+
+These are explained in the following sections.
+
+## Soundness
+
+`rzk-1` assumes "type-in-type", that is `U` has type `U`.
+This is known to make the type system unsound (due to Russell and Curry-style paradoxes), however,
+it is sometimes considered acceptable in proof assistants.
+And, since it simplifies implementation, `rzk-1` embraces this assumption, at least for now.
+
+Moreover, `rzk-1` does not prevent cubes or topes to depend on types and terms. For example, the following definition typechecks:
+
+```rzk
+#define weird
+ (A : U)
+ (I : A -> CUBE)
+ (x y : A)
+ : CUBE
+ := I x * I y
+```
+
+This likely leads to another inconsistency, but it will probably not lead to bugs in actual proofs of interest,
+so current version embraces this lax treatment of universes.
+
+[^1]: Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories._ Higher Structures 1(1), 147-224. 2017.
+
+[^2]: In version [:octicons-tag-24: v0.1.0](https://github.com/rzk-lang/rzk/releases/tag/v0.1.0), `rzk` has supported simply typed lambda calculus, PCF, and MLTT. However, those languages have been removed.
diff --git a/docs/docs/ru/reference/render.rzk.md b/docs/docs/ru/reference/render.rzk.md
new file mode 100644
index 000000000..cb74ab3fa
--- /dev/null
+++ b/docs/docs/ru/reference/render.rzk.md
@@ -0,0 +1,183 @@
+# Rendering Diagrams
+
+Starting from version `0.3.0`, `rzk` supports rendering of topes, types, and terms as diagrams.
+
+This is a literate `rzk` file:
+
+```rzk
+#lang rzk-1
+```
+
+To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):
+
+```rzk
+#set-option "render" = "svg" -- enable rendering in SVG
+```
+
+Rendering is completely automatic, and works in the following situations:
+
+1. Mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes;
+2. Type of mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes.
+3. Mappings from a shape that is a section of an existing shape.
+
+The rendering assigns the following colors:
+
+- purple is assigned for parameters (context) variables;
+- blue is used for fillings for types (e.g. for `hom` and `hom2`);
+- red is used for terms (e.g. `Segal-comp-witness`);
+- orange is used for shapes in the tope layer;
+- grey is used for discarded parts of a (larger) mapping (e.g. when extracting a diagonal/face from a larger shape).
+
+The SVG pictures can be inserted directly into `.md` files before a corresponding `rzk` code block. At the bottom of a markdown file, you might want to add stylization, e.g.:
+
+```html
+
+
+
+
+
+
+
+
+
+
+
+
+```
+
+## Examples
+
+### Visualising Simplicial Topes
+
+Topes are visualised with **orange** color:
+
+```rzk
+-- 2-simplex
+#define Δ² : (2 * 2) -> TOPE
+ := \(t, s) -> s <= t
+```
+
+Boundary of a tope:
+
+```rzk
+-- boundary of a 2-simplex
+#define ∂Δ² : Δ² -> TOPE
+ := \(t, s) -> s === 0_2 \/ t === 1_2 \/ s === t
+```
+
+The busiest tope diagram involves the entire 3D cube:
+
+
+```rzk
+-- 3-dim cube
+#define 2³ : (2 * 2 * 2) -> TOPE
+ := \_ -> TOP
+```
+
+
+```rzk
+-- 3-simplex
+#define Δ³ : (2 * 2 * 2) -> TOPE
+ := \((t1, t2), t3) -> t3 <= t2 /\ t2 <= t1
+```
+
+
+### Visualising Simplicial Types
+
+Types are visualised with **blue** color. Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a type is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color.
+
+```rzk
+-- [RS17, Definition 5.1]
+-- The type of arrows in A from x to y.
+#define hom
+ (A : U) -- A type.
+ (x y : A) -- Two points in A.
+ : U -- (hom A x y) is a 1-simplex (an arrow)
+ := (t : 2) -> A [ -- in A where
+ t === 0_2 |-> x, -- * the left endpoint is exactly x
+ t === 1_2 |-> y -- * the right endpoint is exactly y
+ ]
+```
+
+```rzk
+-- [RS17, Definition 5.2]
+-- the type of commutative triangles in A
+#define hom2
+ (A : U) -- A type.
+ (x y z : A) -- Three points in A.
+ (f : hom A x y) -- An arrow in A from x to y.
+ (g : hom A y z) -- An arrow in A from y to z.
+ (h : hom A x z) -- An arrow in A from x to z.
+ : U -- (hom2 A x y z f g h) is a 2-simplex (triangle)
+ := { (t1, t2) : Δ² } -> A [ -- in A where
+ t2 === 0_2 |-> f t1, -- * the top edge is exactly f,
+ t1 === 1_2 |-> g t2, -- * the right edge is exactly g, and
+ t2 === t1 |-> h t2 -- * the diagonal is exactly h
+ ]
+```
+
+### Visualising Terms of Simplicial Types
+
+Terms (with non-trivial labels) are visualised with **red** color (you can see a detailed label on hover). Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a term is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color.
+
+We can visualise terms that fill a shape:
+
+```rzk
+#define square
+ (A : U)
+ (x y z : A)
+ (f : hom A x y)
+ (g : hom A y z)
+ (h : hom A x z)
+ (a : Sigma (h' : hom A x z), hom2 A x y z f g h')
+ : (2 * 2) -> A
+ := \(t, s) -> recOR( s <= t |-> second a (t, s) , t <= s |-> second a (s, t))
+```
+
+If a term is extracted as a part of a larger shape, generally, the whole shape will be shown (in gray):
+
+```rzk
+#define face
+ (A : U)
+ (x y z : A)
+ (f : hom A x y)
+ (a : Sigma (g : hom A y z), {((t1, t2), t3) : 2 * 2 * 2 | t3 <= t1 \/ t2 <= t1} -> A [ t1 === 0_2 |-> f t2, t1 === 1_2 |-> g t3 ])
+ : Δ² -> A
+ := \(t, s) -> second a ((t, t), s)
+```
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/docs/docs/ru/reference/sections.rzk.md b/docs/docs/ru/reference/sections.rzk.md
new file mode 100644
index 000000000..ddffe2b0f
--- /dev/null
+++ b/docs/docs/ru/reference/sections.rzk.md
@@ -0,0 +1,126 @@
+# Sections and Variables
+
+Sections and variables allow to simplify definitions by factoring out common assumptions.
+
+!!! info "Coq-style variables"
+ `rzk` implements variables similarly to
+ `Variable` command in Coq .
+ An important difference is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental.
+ This is, perhaps, somewhat related to this error message in Coq .
+
+This is a literate `rzk` file:
+
+```rzk
+#lang rzk-1
+```
+
+## Variables
+
+Consider the following definitions:
+
+```rzk
+#define compose₁
+ (A B C : U)
+ (g : B -> C)
+ (f : A -> B)
+ : A -> C
+ := \x -> g (f x)
+
+#define twice₁
+ (A : U)
+ (h : A -> A)
+ : A -> A
+ := \x -> h (h x)
+```
+
+Since it might be common to introduce types `A`, `B`, and `C`, we can declare these are variables:
+
+```rzk
+#variables A B C : U
+
+#define compose₂
+ (g : B -> C)
+ (f : A -> B)
+ : A -> C
+ := \x -> g (f x)
+
+#define twice₂
+ (h : A -> A)
+ : A -> A
+ := \x -> h (h x)
+```
+
+The `#variables` command here introduces assumptions, which can be used in the following definitions. Importantly, after checking a file (module), all definitions will have the assumptions used (explicitly or implicitly) attached as bound variables.
+
+### Implicitly used variables (and `uses`)
+
+We can try going even further and declare variables `f`, `g`, `h`, and `x`:
+
+```rzk
+#variable g : B -> C
+#variable f : A -> B
+#variable h : A -> A
+#variable x : A
+
+-- #define bad-compose₃ : C := g (f x) -- ERROR: implicit assumptions A and B
+#define twice₃ : A := h (h x)
+```
+
+Note how this definition of `bad-compose₃` is implicitly dependent on the types `A` and `B`, which is promptly noted by `rzk`, which issues an error (if we uncomment the corresponding line):
+
+```text
+implicit assumption
+ B : U
+used in definition of
+ bad-compose₃
+```
+
+To let `rzk` know that this is not accidental, we can add `uses (...)` annotation to specify a list of variables implicitly used in the definition:
+
+```rzk
+#define compose₃ uses (A B) : C := g (f x)
+```
+
+## Sections
+
+To introduce assumption variables temporarily inside of one file, you can use sections:
+
+```rzk
+#section example-1
+
+#variables X Y Z : U
+#variable k : X -> X
+#variable x' : X
+
+#define compose₄
+ (g : Y -> Z)
+ (f : X -> Y)
+ : X -> Z
+ := \x -> g (f x)
+
+#define twice₄ : X := k (k x')
+
+#end example-1
+```
+
+Now, once outside of the section, `compose₄` and `twice₄` obtain corresponding parameters
+(only those used, explicitly or implicitly):
+
+```rzk
+-- compose₄ : (X : U) -> (Y : U) -> (Z : U) -> (g : Y -> Z) -> (f : X -> Y) -> (X -> Z)
+-- twice₄ : (X : U) -> (k : X -> X) -> (x' : X) -> X
+
+#define twice₅
+ (T : U)
+ (e : T -> T)
+ : T -> T
+ := compose₄ T T T e e
+
+#define identity
+ (T : U)
+ : T -> T
+ := twice₄ T (\t -> t)
+```
+
+!!! warning "Lack of indentation"
+ `rzk` currently does not support indentation, so all definitions and commands inside a section (including nested sections) have to start at the beginning of a line.
diff --git a/docs/docs/ru/reference/tope-disjunction-elimination.rzk.md b/docs/docs/ru/reference/tope-disjunction-elimination.rzk.md
new file mode 100644
index 000000000..0b8f25e65
--- /dev/null
+++ b/docs/docs/ru/reference/tope-disjunction-elimination.rzk.md
@@ -0,0 +1,13 @@
+# Tope disjuction elimination
+
+Following Riehl and Shulman's type theory[^1], `#!rzk rzk-1` introduces two primitive terms for disjunction elimination:
+
+1. `#!rzk recBOT` corresponds to \(\mathsf{rec}_\bot\), has any type, and is valid whenever tope context is included in `#!rzk BOT`;
+
+2. `#!rzk recOR(«tope_1» |-> «term_1», ..., «tope_n» |-> «term_n»)` defines a term for a disjunction of topes `#!rzk «tope_1» \/ ... \/ «tope_n»`. This is well-typed when for an intersection of any two topes `#!rzk «tope_i» /\ «tope_j»` the corresponding terms `#!rzk «term_i»` and `#!rzk «term_j»` are judgementally equal. In particular, `#!rzk recOR(psi |-> a_psi, phi |-> a_phi)` corresponds to \(\mathsf{rec}_\lor^{\psi, \phi}(a_\psi, a_\phi)\).
+
+!!! warning "Deprecated syntax"
+ `#!rzk recOR(psi, phi, a_psi, a_phi)` corresponds to \(\mathsf{rec}_\lor^{\psi, \phi}(a_\psi, a_\phi)\), is well-typed when `#!rzk a_psi` is definitionally equal to `#!rzk a_phi` under `#!rzk psi /\ phi`. However, this syntax is deprecated since it is easy to confuse which tope relates to which term.
+
+[^1]: Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories._ Higher Structures 1(1), 147-224. 2017.
+
diff --git a/docs/docs/ru/reference/tope-layer.rzk.md b/docs/docs/ru/reference/tope-layer.rzk.md
new file mode 100644
index 000000000..a3c5a83b6
--- /dev/null
+++ b/docs/docs/ru/reference/tope-layer.rzk.md
@@ -0,0 +1,21 @@
+# Tope layer
+
+All topes live in `#!rzk TOPE` universe.
+
+Here are all the ways to build a tope:
+
+1. Introduce a variable, e.g. `#!rzk (psi : TOPE) -> ...`;
+
+ - Usually, topes depend on point variables from some cube(s). To indicate that, we usually introduce topes as "functions" from some cube to `#!rzk TOPE`. For example, `#!rzk (psi : I -> TOPE) -> ...`.
+
+2. Use a constant:
+
+ - top tope \(\top\) is written `#!rzk TOP`
+ - bottom tope \(\bot\) is written `#!rzk BOT`
+
+3. Usa a tope connective:
+ - tope conjunction \(\psi \land \phi\) is written `#!rzk psi /\ phi`
+ - tope disjunction \(\psi \lor \phi\) is written `#!rzk psi \/ phi`
+ - equality tope \(t \equiv s\) is written `#!rzk t === s`, whenever `#!rzk t` and `#!rzk s` are points of the same cube
+ - inequality tope \(t \leq s\) is written `#!rzk t <= s` whenever `#!rzk t : 2` and `#!rzk s : 2`
+
diff --git a/docs/docs/ru/reference/type-layer.rzk.md b/docs/docs/ru/reference/type-layer.rzk.md
new file mode 100644
index 000000000..8a1619e65
--- /dev/null
+++ b/docs/docs/ru/reference/type-layer.rzk.md
@@ -0,0 +1,48 @@
+# Types and terms
+
+```rzk
+#lang rzk-1
+```
+
+## Functions (dependent products)
+
+Function (dependent product) types \(\prod_{x : A} B\) are written `#!rzk (x : A) -> B x`. Values of function types are \(\lambda\)-abstractions written in one of the following ways:
+
+ - `#!rzk \x -> ` — this is usually fine;
+ - `#!rzk \(x : A) -> ` — this sometimes helps the typechecker.
+
+## Dependent sums
+
+Dependent sum type \(\sum_{x : A} B\) is written `#!rzk ∑ (x : A), B` or `#!rzk Sigma (x : A), B`. Values of dependent sum types are pairs written as `#!rzk (x, y)`.
+
+To access components of a dependent pair `#!rzk p`, use `#!rzk first p` and `#!rzk second p`.
+
+!!! warning
+ `#!rzk first` and `#!rzk second` are not valid syntax without an argument!
+
+## Identity types
+
+Identity (path) type \(x =_A y\) is written `#!rzk x =_{A} y`.
+
+!!! tip
+ Specifying the type `#!rzk A` is optional: `#!rzk x = y` is valid syntax!
+
+Any identity type has value `#!rzk refl_{x : A}` whose type is `#!rzk x =_{A} x` whenever `#!rzk x : A`
+
+!!! tip
+ Specifying term and type of `#!rzk refl_{x : A}` is optional: `#!rzk refl_{x}` and `#!rzk refl` are both valid syntax.
+
+Path induction is done using \(\mathcal{J}\) path eliminator:
+
+- for
+ - any type \(A\) and \(a : A\),
+ - type family \(C : \prod_{x : A} ((a =_A x) \to \mathcal{U})\) and
+ - \(d : C(a,\mathsf{refl}_a)\) and
+ - \(x : A\) and \(p : a =_A x\)
+- we have \(\mathcal{J}(A, a, C, d, x, p) : C(x, p)\)
+
+In `#!rzk rzk-1` we write `#!rzk idJ(A, a, C, d, x, p)`
+
+!!! warning
+ `#!rzk idJ` is not valid syntax without exactly 6-tuple provided as an argument!
+
diff --git a/docs/docs/ru/rzk.yaml b/docs/docs/ru/rzk.yaml
new file mode 100644
index 000000000..3469d50f8
--- /dev/null
+++ b/docs/docs/ru/rzk.yaml
@@ -0,0 +1,3 @@
+include:
+ - getting-started/dependent-types.rzk.md
+ - examples/recId.rzk.md
diff --git a/docs/docs/ru/tools.md b/docs/docs/ru/tools.md
new file mode 100644
index 000000000..eee1ed4d3
--- /dev/null
+++ b/docs/docs/ru/tools.md
@@ -0,0 +1,30 @@
+# Инструменты
+
+Решатель теорем Rzk включает в себя языковой сервер и возможность автоматичекого форматирования.
+
+Другие инструменты улучшают пользовательский опыт и/или автоматизируют частные задачи.
+
+### Расширение для VS Code
+
+См. [rzk-lang/vscode-rzk](https://github.com/rzk-lang/vscode-rzk).
+Расширение предлагает много удобств и использование VS Code с ним рекомендуется, особенно новичкам,
+поскольку это наиболее распространённый способ работы с Rzk и ему уделяется больше внимания со стороны разработчиков.
+
+### Плагин для MkDocs
+
+См. [rzk-lang/mkdocs-plugin-rzk](https://github.com/rzk-lang/mkdocs-plugin-rzk).
+Плагин улучшает документацию, получаемую из литературных файлов с формализациями (`.rzk.md`):
+- добавляет SVG-диаграммы по определениям/доказательствам, если возможно (экспериментальная поддержка)
+- добавляет якоря для определний (полезно для создания ссылок на конкретные определения)
+
+### Скрипт для GitHub Action
+
+См. [rzk-lang/rzk-action](https://github.com/rzk-lang/rzk-action).
+Этот скрипт позволяет проверять формализации на Rzk для проектов на GitHub автоматически.
+Скрипт также экспериментально поддерживает проверку форматирования.
+
+### Подсветка синтаксиса (Pygments)
+
+См. [rzk-lang/pygments-rzk](https://github.com/rzk-lang/pygments-rzk).
+Это простая реализация подсветки синтаксиса (используется при генерации документации с MkDocs и пакетом `minted` package в LaTeX).
+Учтите, что подсветка может отличатся от подсветки в VS Code, т.к. последний использует языковой сервер Rzk для более точной "семантической подсветки".
diff --git a/docs/docs/tools/continuous.md b/docs/docs/tools/continuous.md
deleted file mode 100644
index 7bb5b35bc..000000000
--- a/docs/docs/tools/continuous.md
+++ /dev/null
@@ -1,5 +0,0 @@
-# Continuous Verification with `rzk`
-
-## GitHub Action
-
-See . See also for an example usage of the action.
diff --git a/docs/docs/tools/highlight.md b/docs/docs/tools/highlight.md
deleted file mode 100644
index efd0505da..000000000
--- a/docs/docs/tools/highlight.md
+++ /dev/null
@@ -1,8 +0,0 @@
-# Syntax Highlighting
-
-Currently basic syntax highlighting is supported for several environments:
-
-1. `vscode-rzk` VS Code extension provides syntax highlighting for both `*.rzk` files and `rzk` code blocks in Markdown files.
-2. HighlightJS syntax highlighting (used by MkDocs) is available at https://github.com/rzk-lang/rzk/blob/develop/docs/custom_theme/js/rzk.js
-3. Pygments syntax highlighting is available a Python package at https://github.com/rzk-lang/rzk/tree/develop/rzk/RzkLexer . This syntax highlighter is suitable for using with LaTeX (e.g. with `minted` package).
-4. There is also an obsolete syntax highlighting mode for CodeMirror 5 .
diff --git a/docs/docs/tools/ide.md b/docs/docs/tools/ide.md
deleted file mode 100644
index 5ed2b48c0..000000000
--- a/docs/docs/tools/ide.md
+++ /dev/null
@@ -1,7 +0,0 @@
-# IDE support for `rzk`
-
-## VS Code
-
-There exists a VS Code extension for `rzk` ([on VS Marketplace](https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting), [on GitHub](https://github.com/rzk-lang/vscode-rzk)).
-
-Please, refer to the documentation of the extension for more details.
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
deleted file mode 100644
index 2792c41d2..000000000
--- a/docs/mkdocs.yml
+++ /dev/null
@@ -1,121 +0,0 @@
-site_name: "rzk: an experimental proof assistant for synthetic ∞-categories"
-repo_url: https://github.com/rzk-lang/rzk
-repo_name: rzk-lang/rzk
-edit_uri: edit/develop/docs/docs/
-
-nav:
- - General:
- - About: index.md
- - Contributors: CONTRIBUTORS.md
- - Changelog: CHANGELOG.md
- - Getting Started:
- - Install: getting-started/install.md
- - Quickstart: getting-started/quickstart.rzk.md
- - Publishing with MkDocs: getting-started/publishing-with-mkdocs.md
- - Reference:
- - Introduction: reference/introduction.rzk.md
- - Cube layer: reference/cube-layer.rzk.md
- - Tope layer: reference/tope-layer.rzk.md
- - Dependent types: reference/type-layer.rzk.md
- - Tope disjunction elimination: reference/tope-disjunction-elimination.rzk.md
- - Extension types: reference/extension-types.rzk.md
- - Organizational features:
- - Sections and Variables: reference/sections.rzk.md
- - Builtins:
- - Directed interval: reference/builtins/directed-interval.rzk.md
- - Unit type: reference/builtins/unit.rzk.md
- - Commands:
- - Define and Postulate: reference/commands/define-postulate.rzk.md
- - Compute: reference/commands/compute.rzk.md
- - Check: reference/commands/check.rzk.md
- - Options: reference/commands/options.rzk.md
- - Other:
- - Rendering Diagrams: reference/render.rzk.md
- - Examples:
- - Weak tope disjunction elimination: examples/recId.rzk.md
- - Community: community.md
- - Tools:
- - Syntax Highlighting: tools/highlight.md
- - IDE support: tools/ide.md
- - Continuous Verification: tools/continuous.md
- - Related Projects:
- - Yoneda lemma for ∞-categories: related/yoneda.md
- - sHoTT: related/sHoTT.md
- - simple-topes: related/simple-topes.md
- - Playground: playground/
-
-markdown_extensions:
- - admonition
- - footnotes
- - pymdownx.details
- - mdx_math
- - pymdownx.highlight:
- anchor_linenums: true
- line_spans: __span
- pygments_lang_class: true
- - pymdownx.inlinehilite
- - pymdownx.snippets
- - pymdownx.superfences
- - toc:
- permalink: true
- - pymdownx.arithmatex:
- generic: true
- - attr_list
- - pymdownx.emoji:
- emoji_index: !!python/name:materialx.emoji.twemoji
- emoji_generator: !!python/name:materialx.emoji.to_svg
-
-
-theme:
- name: material
- custom_dir: overrides
- favicon: assets/images/favicon.png
- logo: assets/images/logo-1000x1000.png
- icon:
- repo: fontawesome/brands/github
- edit: material/pencil
- view: material/eye
- features:
- - content.code.copy
- - content.action.edit
- - navigation.footer
- - navigation.tabs
- - navigation.tabs.sticky
- - navigation.sections
- - navigation.path
- palette:
- # Palette toggle for light mode
- - media: "(prefers-color-scheme: light)"
- primary: white
- scheme: default
- toggle:
- icon: material/brightness-7
- name: Switch to dark mode
- # Palette toggle for dark mode
- - media: "(prefers-color-scheme: dark)"
- primary: black
- scheme: slate
- toggle:
- icon: material/brightness-4
- name: Switch to light mode
-
-extra_javascript:
- - javascript/mathjax.js
- - https://polyfill.io/v3/polyfill.min.js?features=es6
- - https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js
-
-extra_css:
- - https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.16.7/katex.min.css
- - https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.7.0/styles/default.min.css
- - assets/css/rzk-render.css
-
-extra:
- version:
- provider: mike
-
-plugins:
- - mike
- - rzk:
- render_svg: true
- anchor_definitions: true
- - search
diff --git a/docs/requirements.txt b/docs/requirements.txt
index c32519893..631c6eff7 100644
--- a/docs/requirements.txt
+++ b/docs/requirements.txt
@@ -1,5 +1,5 @@
-mkdocs-material
-mike
+mkdocs-material[imaging]
+mike==2.0.0
python-markdown-math
-mkdocs-plugin-rzk==0.1.2
+mkdocs-plugin-rzk
pygments-rzk
diff --git a/docs/root/android-chrome-192x192.png b/docs/root/android-chrome-192x192.png
deleted file mode 100644
index f788e2a29..000000000
Binary files a/docs/root/android-chrome-192x192.png and /dev/null differ
diff --git a/docs/root/android-chrome-512x512.png b/docs/root/android-chrome-512x512.png
deleted file mode 100644
index a5d60488b..000000000
Binary files a/docs/root/android-chrome-512x512.png and /dev/null differ
diff --git a/docs/root/apple-touch-icon.png b/docs/root/apple-touch-icon.png
deleted file mode 100644
index db6b8958f..000000000
Binary files a/docs/root/apple-touch-icon.png and /dev/null differ
diff --git a/docs/root/favicon-16x16.png b/docs/root/favicon-16x16.png
deleted file mode 100644
index a96453dcd..000000000
Binary files a/docs/root/favicon-16x16.png and /dev/null differ
diff --git a/docs/root/favicon-32x32.png b/docs/root/favicon-32x32.png
deleted file mode 100644
index 4e67e099c..000000000
Binary files a/docs/root/favicon-32x32.png and /dev/null differ
diff --git a/docs/root/favicon.ico b/docs/root/favicon.ico
deleted file mode 100644
index ed8b0d72c..000000000
Binary files a/docs/root/favicon.ico and /dev/null differ
diff --git a/docs/root/index.html b/docs/root/index.html
deleted file mode 100644
index 996a8ba1c..000000000
--- a/docs/root/index.html
+++ /dev/null
@@ -1,102 +0,0 @@
-
-
-
- rzk: an experimental proof assistant
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/docs/root/site.webmanifest b/docs/root/site.webmanifest
deleted file mode 100644
index 1799a7ee5..000000000
--- a/docs/root/site.webmanifest
+++ /dev/null
@@ -1 +0,0 @@
-{"name":"","short_name":"","icons":[{"src":"/rzk/android-chrome-192x192.png","sizes":"192x192","type":"image/png"},{"src":"/rzk/android-chrome-512x512.png","sizes":"512x512","type":"image/png"}],"theme_color":"#ffffff","background_color":"#ffffff","display":"standalone"}
diff --git a/rzk.yaml b/rzk.yaml
index 3bc078d8c..3469d50f8 100644
--- a/rzk.yaml
+++ b/rzk.yaml
@@ -1,2 +1,3 @@
include:
- - docs/docs/examples/recId.rzk.md
\ No newline at end of file
+ - getting-started/dependent-types.rzk.md
+ - examples/recId.rzk.md