https://github.com/rzk-lang/rzk Skip to content Toggle navigation Sign up * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions For + Enterprise + Teams + Startups + Education By Solution + CI/CD & Automation + DevOps + DevSecOps Resources + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} rzk-lang / rzk Public * Notifications * Fork 3 * Star 134 An experimental proof assistant based on a type theory for synthetic [?]-categories. rzk-lang.github.io/rzk/ 134 stars 3 forks Activity Star Notifications * Code * Issues 29 * Pull requests 4 * Actions * Projects 0 * Security * Insights More * Code * Issues * Pull requests * Actions * Projects * Security * Insights rzk-lang/rzk This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. develop Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags Name already in use A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch? Cancel Create 12 branches 19 tags Code * Local * Codespaces * Clone HTTPS GitHub CLI [https://github.com/r] Use Git or checkout with SVN using the web URL. [gh repo clone rzk-la] Work fast with our official CLI. Learn more about the CLI. * Open with GitHub Desktop * Download ZIP Sign In Required Please sign in to use Codespaces. Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Launching Xcode If nothing happens, download Xcode and try again. Launching Visual Studio Code Your codespace will open once ready. There was a problem preparing your codespace, please try again. Latest commit @fizruk fizruk Merge branch 'release-v0.6.4' into develop ... 8e4f3ad Sep 27, 2023 Merge branch 'release-v0.6.4' into develop * release-v0.6.4: Bump version and update changelogs 8e4f3ad Git stats * 550 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time .github/workflows Show log if nix-build fails September 27, 2023 14:25 docs Bump version and update changelogs September 27, 2023 18:25 images Update demo image in README April 28, 2023 17:14 rzk Bump version and update changelogs September 27, 2023 18:25 try-rzk Update all references from fizruk to rzk-lang July 9, 2023 23:07 .envrc add flake with cabal, hls, ghcjs, set up caching May 17, 2023 21:13 .ghci Add .ghci and remove some FIXMEs November 5, 2021 00:46 .gitignore Remove and ignore generated docs for grammar July 12, 2023 00:47 CITATION.cff Update all references from fizruk to rzk-lang July 9, 2023 23:07 README.md Update all references from fizruk to rzk-lang July 9, 2023 23:07 cabal.project add flake with cabal, hls, ghcjs, set up caching May 17, 2023 21:13 flake.lock add flake with cabal, hls, ghcjs, set up caching May 17, 2023 21:13 flake.nix add flake with cabal, hls, ghcjs, set up caching May 17, 2023 21:13 rzk.yaml Add rzk.yaml to specify files to check September 23, 2023 18:24 snapshot.yaml Use custom Stack snapshot to avoid rebuilding extra-deps September 27, 2023 16:40 stack-8.6.5.yaml Update deps and stack.yaml files September 27, 2023 15:54 stack-8.6.5.yaml.lock Fix build for GHC 8.6.5 April 13, 2023 09:53 stack.yaml Use custom Stack snapshot to avoid rebuilding extra-deps September 27, 2023 16:40 stack.yaml.lock Update deps and stack.yaml files September 27, 2023 15:54 View code [ ] rzk About this project How to use rzk VS Code Checking How to contribute to rzk Building the Documentation Locally Development Building with GHC Building with GHCJS Flake References README.md rzk MkDocs Haddock GHCJS build An experimental proof assistant for synthetic [?]-categories. Early prototype demo. 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 is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: https:// github.com/fizruk/sHoTT and https://github.com/emilyriehl/yoneda. 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 https://github.com/fizruk /simple-topes. 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. How to use rzk For relatively small single-file formalisations, you can use the online playground at https://rzk-lang.github.io/rzk/playground.html However, for larger and multi-file formalisations you should install a version of rzk locally: * You can install the latest "stable" version of rzk from Hackage: cabal install rzk * You can install the latest "development" version of rzk from the develop branch of this repository: git clone https://github.com/rzk-lang/rzk.git cd rzk git checkout develop stack build && stack install VS Code There exists a VS Code extension for rzk available on the Marketplace. The extension supports basic syntax highlighting, but more features may come in the future. Checking To check a multi-file project, you need to call rzk typecheck specifying the files in correct order, e.g.: rzk typecheck first.rzk second.rzk third.rzk A proper support for inter-file dependencies will be implemented in the future. Until then, it is recommented to start names of files with a number, ensuring correct order when using a wildcard (*). For example: . +-- 0-common.md +-- 1-paths.md +-- 2-contractible.md +-- 3-homotopies.md +-- 4-equivalences.md +-- 5-sigma.md +-- 6-trivial-fibrations.md 1 directory, 7 files Inside of such directory, you can run rzk typecheck on all files using wildcards: rzk typecheck *-*.md How to contribute to rzk Building the Documentation Locally First, you need to install MkDocs and mdx_math Markdown extension (to enable LaTeX): pip install python-markdown-math Now, you can build and serve the documentation locally by running mkdocs serve --config-file docs/mkdocs.yml The (locally built) documentation should be available at http:// 127.0.0.1:8000 The pages of the documentation are the *.md files in docs/docs directory and its subdirectories. To add a new page, you can create a new *.md file and add it to the navigation by modifying docs/ mkdocs.yml. Development The project is developed with both Stack and Nix (for GHCJS version). Building with GHC For quick local development and testing it is recommended to work with a GHC version, using Stack tool. Clone this project and simply run stack build: git clone git@github.com:rzk-lang/rzk.git cd rzk stack build The build provides an executable rzk which can be used to typecheck files: stack exec -- rzk typecheck FILE Building with GHCJS try-rzk package is designed to be compiled using GHCJS for an in-browser version of the proof assistant. To build this package you need to use Nix. It is recommended that you use Cachix to avoid recompiling lots of dependencies: # Install Nix curl https://nixos.org/nix/install | sh # (optionally) Install Cachix nix-env -iA cachix -f https://cachix.org/api/v1/install # (optionally) Use cached miso from Cachix cachix use miso-haskell Clone the repository, enter try-rzk directory and use nix-build: git clone git@github.com:rzk-lang/rzk.git cd rzk/try-rzk nix-build Now open playground.html to see the result. Note that if local GHCJS build is unavailable, playground.html will use the JS file from GitHub Pages as a fallback. Flake The flake in this repository allows to build try-rzk incrementally and reproducibly. 1. Install Nix via single-user installation: 1. Run script sh <(curl -L https://nixos.org/nix/install) --no-daemon 1. Permanently enable flakes 2. Enter the devShell with GHC (not GHCJS). Answer y to Nix prompts to use binary caches. nix develop 3. The shell provides ghc, haskell-language-server, cabal-install, hpack. 4. (Optionally) Install direnv to start the devShell when you enter the repository directory. 5. Build rzk. cabal build 6. Enter the devShell with GHCJS. nix develop .#ghcjs 7. Build try-rzk. This may require ~10 GB of RAM. cabal build --ghcjs 8. (Optionally) Build rzk via Nix. The resulting executable will be in result/bin/rzk. nix build .#rzk 9. (Optionally) Run rzk via Nix. nix run .#rzk 10. (Optionally) Build try-rzk via Nix. This may require ~10 GB of RAM. The resulting executable will be in try-rzk/result/bin/ try-rzk.jsexe. nix build .#try-rzk --out-link try-rzk/result 11. Open the app in a browser. firefox try-rzk/playground.html References 1. Emily Riehl & Michael Shulman. A type theory for synthetic [?]-categories. Higher Structures 1(1), 147-224. 2017. https:// arxiv.org/abs/1705.07442 2. Nikolai Kudasov. E-unification for Second-Order Abstract Syntax. 2023. https://arxiv.org/abs/2302.05815 About An experimental proof assistant based on a type theory for synthetic [?]-categories. rzk-lang.github.io/rzk/ Topics haskell proof-assistant category-theory homotopy-type-theory Resources Readme Activity Stars 134 stars Watchers 6 watching Forks 3 forks Report repository Releases 19 v0.6.4 Latest Sep 27, 2023 + 18 releases Packages 0 No packages published Contributors 4 * @fizruk fizruk Nikolai Kudasov * @aabounegm aabounegm Abdelrahman Aly Abounegm * @github-actions[bot] github-actions[bot] * @deemp deemp Danila Danko Languages * Haskell 95.3% * HTML 3.3% * Other 1.4% Footer (c) 2023 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time.