.. _theHoTTGame:

*************
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 <https://agda.readthedocs.io/en/v2.6.0/language/cubical.html>`_
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 <https://thehottgameguide.readthedocs.io/en/latest/index.html>`_.

The creators of this game are 
`Joseph Hua <https://jlh18.github.io/>`_, 
`Ken Lee <http://kl-i.github.io/>`_,
and `Bendit Chan <https://benditchan.wordpress.com/>`_.