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.

This repository is a library of incomplete agda code, for the user to complete as part of the HoTT Game. For instructions on how to get started, visit this page.

The creators of this game are Joseph Hua, Ken Lee, and Bendit Chan.