The HoTT Game

The Homotopy Type Theory (HoTT) Game is a project written by mathematicians for mathematicians interested in HoTT and no experience in proof verification, with the aim of introducing cubical agda as a tool for trying out mathematics in HoTT. This page will help you get the Game working for you.

Agdapad

The HoTT Game can be played entirely in your browser using Agdapad. If you want a quick start to the game without installing anything, you can go straight to the site, create your own agda session, and start playing.

Specifically, once you open an agda session, you should see a welcome page (which contains useful information). Around the top left of the screen there is a folder icon. Click on the folder icon, and open the directory TheHoTTGame. This contains everything you need for the game.

Many thanks to Ingo Blechschmidt for incorporating the game into Agdapad.

Installing Agda and the Cubical Agda library

A more long-term setup for using agda would be to install it locally. If you would like detailed instructions on how to install agda and a supportive text editor then we recommend you follow instructions on Installation. More general instructions follow:

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, specifically we recommend doom emacs, but it can also work in atom and vs-code.

Once you have emacs and agda, clone the cubical library repository (version 0.3) and make sure agda knows where your copy of the 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 our repository into a folder and then making sure that agda knows where the HoTT Game is by adding a line

the-directory/TheHoTTGame.agda-lib

to your libraries file as above.

Try opening 1FundamentalGroup/Quest0.agda in Emacs and do Ctrl-c Ctrl-l. Some text should be highlighted, and any {!!} should turn into { }.

Where to start?

You can start with trinitarianism if you are interested in how logic, type theory and category theory come together as different ways to view the same thing. If you are more interested in homotopy theory, try Fundamental Group of the Circle where we show that the fundamental group of S¹ is ℤ. We recommend starting with Fundamental Group of the Circle for intuition, then going to trinitarianism.

How to start?

To start with Fundamental Group of the Circle (for example), go to Quest 0 - Working with the Circle and follow the instructions there. Any agda should happen in Agdapad or your local copy of the repository.

Emacs issues

If you can’t figure out emacs or forget some command, then try consulting the Emacs and Unicode Commands page.

Special thanks

We would like to thank Kevin Buzzard for introducing us to formalization, making the Natural Numbers Game for learning lean (which inspired this project), and helping the game gain publicity. We would also like to thank all those involved in the HoTT community and writing the HoTT book, especially Steve Awodey, who helped us post about the Game on homotopytypetheory.org. Lastly we thank all those who are trying out the game and giving us feedback. If you would like to get involved, simply open and issue and let us know what you would like to do.