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.

To get started with the HoTT Game, go to Getting Started.

This game was created by Joseph Hua, Ken Lee, and Bendit Chan.