This organisation collects some repositories related to rzk, an experimental proof assistant for synthetic ∞-categories:
- rzk-lang/rzk — the Rzk proof assistant
Below we list other repositories in this organisation with brief descriptions.
- rzk-lang/vscode-rzk — VS Code extension for
rzk(recommended) - rzk-lang/mkdocs-plugin-rzk — MkDocs plugin for
rzk(diagram rendering, definition anchors, etc.) - rzk-lang/rzk-action — GitHub Action for running
rzkto check formalisations - rzk-lang/pygments-rzk — syntax highlighter for Pygments (used by MkDocs and
mintedpackage in LaTeX) - 🚧 rzk-lang/rzk.sty — LaTeX package for
rzk(will appear soon)
- rzk-lang/sHoTT — an active formalisation project for simplicial HoTT
- rzk-lang/hottbook — the HoTT Book formalisations in
rzk(early stages) - Known external formalizations:
- emilyriehl/yoneda — the ∞-categorical Yoneda lemma (and its variations), and comparison with 1-categorical versions in other provers
- Templates:
- rzk-lang/rzk-project-template — template repository for
rzkformalisations
- rzk-lang/rzk-project-template — template repository for
- https://fizruk.github.io/itp-school-2023-demo/ — demo/tutorial for the «Interactions of Proof Assistants and Mathematics» school in Regensburg, September 18–29, 2023, containing introduction to the syntax of Rzk and basics of theorem proving in Rzk, as well as a few exercises.
- https://fizruk.github.io/bmstu-rzk-demo-2023/ — demo/tutorial for the HoTT seminar at Bauman Moscow State Technical University, Nov 20–21, 2023; contains a partial introduction to homotopy type theory (following the HoTT Book) and simplicial type theory in Rzk. Perhaps, the most approachable tutorial for newcomers unfamiliar with both dependent types and homotopy type theory.
