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.

• Getting Started
  • The HoTT Game
  • Installation
  • Emacs and Unicode Commands
  • Getting Git on MacOS
• Trinitarianism
  • Overview
  • Quest 0 - Terms and Types
  • Quest 1 - Dependent Types
  • Quest 2 - Sigma Types
  • Quest 2 - Side Quests
  • Quest 3 - Pi Types
  • Quest 3 - Side Quests
  • Quest 4 - Paths and Equality
  • Quest 4 - Side Quests
  • Quest 5 - Dependent Paths
• Fundamental Group of the Circle
  • Overview
  • Quest 0 - Working with the Circle
  • Quest 0 - Side Quests
  • Quest 1 - Loop Space of the Circle
  • Quest 2 - ℤ is a Set
  • Quest 3 - The Loop Space is ℤ