What is 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. You can find it here. Much of the content of the game is based on the HoTT book and lectures by Robert Harper on YouTube.
How does the game work?
The game is a guided sequence of exercises that the user can complete in cubical agda. There are currently two main parts to it:
- Fundamental Group of the Circle: This part has one goal in mind: to show that π₁(S¹) = ℤ from scratch. We use this as an excuse to introduce higher inductive types, univalence, transport, loop spaces, and homotopy levels.
- Trinitarianism: This introduces the basics of dependent type theory and later the extension to HoTT. We try to outline each new concept with logical, type theoretic, and categorical perspectives. Whilst this can be the starting point for learning HoTT, we recommend users to start with Fundamental Group of the Circle.
The format: The website contains all the information the user needs to play the game, but to follow along with the exercises, one must do so in agda installed on their computer. Unfortunately installing agda is often the most challenging part, and we are yet to find a good solutions to this. If you have any difficulties installing agda, please try to reach us with ‘issues’ on the github repository. If you have any suggestions or solutions (such as making a browser format of the game) please let us know as well.
Who are we and why did we make it?
The current development team consists of Joseph Hua (me), Ken Lee, and Bendit Chan. We are masters students in pure mathematics at Imperial College London. We were inspired by the Natural Numbers Game made by our professor Kevin Buzzard introducing undergraduates to lean, and thought making a similar game would be a nice way to review the HoTT we learnt. Moreover, we thought this would be a nice resource for people to try out HoTT in a modern, hands-on way.
If you try out the game we would also love to hear your feedback.
Homotopy Type Theory 
This is very cool! Thanks for the post, Joseph, and for making the HoTT game!
Thank you for letting us advertise it here!
Oh that’s a great idea. Would love to try.
Tried installing Agda, failed at literally the first step of the guide found here (I’m on Windows which probably is my first mistake but still) https://thehottgameguide.readthedocs.io/en/latest/getting-started/installation.html#installation-on-windows
choco installs ghc and cabal just fine but then cabal claims it cannot find ghc and, thus, none of the packages. Usually that is a path variable issue, I think, but ghc is already in path, so I have no idea what’s going wrong.
Turns out all I had to do was close and open the shell. Wow, thanks windows. (On the install guide for cabal, it mentioned running refreshenv as extra step. That didn’t do the trick but it allowed me to guess at the solution)
If you have any more problems you can raise an issue on the github page https://github.com/thehottgame/TheHoTTGame/issues Yes windows is particularly difficult for this sort of thing, but we have got it working on a couple of windows computers so don’t give up! (or move to linux of course)
I added an issue but it looks like I somehow managed to post it twice. Sorry about that. – I got it running now and have played up to and including Quest 2
I managed to install doom emacs as per the instructions there. Next step:
“cabal install make”
outcome:
“cabal.exe unknown package “make”.”
One site suggested
“cabal update”
so I did that, but it didn’t fix the issue.
Googling around, I found no other reference to this.
I went through stack instead:
(install stack using the installer)
(using git Bash, starting in ~/ )
cabal get Agda
cd Agda-2.6.2
stack –stack-yaml stack-9.0.1.yaml install
This gave me what looks to be a working version of Agda 2.6.2 as promised.
However, for some reason the agda2-mode that emacs sees says it’s agda2-mode 2.6.3 which mismatches Agda version 2.6.2.
Very neat! Is there any prospect of a “cubical agdapad” so that people wouldn’t have to install Agda locally?
This is likely to happen at some point yes – it should just be a case of having a copy of the game in the home directory of agdapad
There is now! Check out (agdapad)[https://agdapad.quasicoherent.io/] where Ingo Blechschmidt has kindly incorporated our game 🙂
Since recently the vscode plugin for Agda has an option to automatically install a precompiled version of Agda, this is probably the easiest way to get a local installation of Agda at the moment: https://github.com/banacorn/agda-mode-vscode#agda-language-server
Great – I’ll add this to our list of ways to get agda!