An agda development focussed on the development of ∞-category theory using simplicial type theory. Visit the forest to browse the resource and find out more about the project.
Have questions or just want to chat? Join our Discord server!
The easiest way to build or work on this project is using nix, and we provide a range
of targets for building, watching, and serving the site via the Makefile. To build
the project and set up a server you can run make server from the nix shell, with an
optional PORT= parameter (default: 1313). To see all make targets run
make help.
To get working on the library without nix you will at minimum need a working installation of Agda nightly version f369741 or newer. You can find the latest release binaries here. See also the Agda documentation: installing from source.
We use pre-commit to run a series of quality checks on
contributions. It can be installed as a stand alone program or via
Python using python -m pip install pre-commit. After it
is installed you can run them manually with pre-commit run --all-files, or
alternatively enable the automatic git hooks with pre-commit install (to disable
them later run pre-commit uninstall).
In order to build the forest, you will need:
- agda-forester
- treelist
- Forester version 5
- We use Kento Okura's forest-server by default to serve the Forest locally, but you may choose other options. A python server target is provided in the makefile.
I have been using the emacs mode by the Topos Institute at github:ToposInstitute/forester.el, which works well when editing trees, but there is currently no solution for working with literate agda in forests.
Benchmarking history is published at the benchmarks page.