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.

For instructions on how to get started with the HoTT Game, visit this page.

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