The HoTT Game

The Homotopy Type Theory (HoTT) Game is a project aimed at introducing mathematicians with no experience in proof verification interested in HoTT and able to use Agda for HoTT. This guide will help you get the Game working for you.

Installing Agda and the Cubical Agda library

Our Game is in Agda, which can be installed following instructions on their site. It is recommended that you use Agda in the text editor emacs, in particular Doom Emacs is a bit nicer if you can't be bothered to do a bunch of configuration.

Once you have Emacs and Agda, get the Cubical Library (version 0.3) and make sure Agda knows where your cubical library is by following instructions on the library management page. In short: locate (or create) your libraries file and add a line

the-directory/cubical.agda-lib

to it, where the-directory is the location of cubical.agda-lib on your computer.

Get the HoTT Game by cloning this repository into a folder and then making sure that Agda knows where the HoTT Game is by adding a line

the-directory/HoTTGameLib.agda

to your libraries file as above.

Try opening up Trinitarianism/AsProps/Quest0.agda in Emacs and do Ctrl-c Ctrl-l. Some text should be highlighted, and any ? should turn into { }.

How the game works

Our Game is under development. Please contact the devs. Currently you can try Trinitarianism/AsProps/Quest0.agda, making use of the accompanying solutions Agda file.

Emacs and Agda usage

We have a file with a list of basic Emacs commands and you should be able to learn how to use Agda as you go along.

Feedback

If you have any feedback please contact the devs.