The HoTT Game
latest
  • Getting Started
  • Trinitarianism
  • Fundamental Group of the Circle
The HoTT Game
  • The HoTT Game
  • Edit on GitHub

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
  • 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 ℤ
Next

© Copyright . Revision 65180065.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
Downloads
pdf
html
epub
On Read the Docs
Project Home
Builds