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. Benchmark history is published at the benchmark page.
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.
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.