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.

doubleCover