The HoTT Game
latest
Getting Started
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
The HoTT Game
Trinitarianism
Edit on GitHub
Trinitarianism
Overview
Terms and Types
Non-dependent Types
Dependent Types
What is ‘the Same’?
Quest 0 - Terms and Types
Part 0 - True / Unit / Terminal object
Part 1 - False / Empty / Initial object
Part 2 - The natural numbers
Part 3 - Universes
Quest 1 - Dependent Types
Part 0 - Predicates / Dependent Constructions / Bundles
Part 1 - Interpretations of Bundles
Part 2 - Using the Trinitarianism
Quest 2 - Sigma Types
Part 0 - Existence / Dependent Pair / Total Space of Bundles
Part 1 - Making terms in Sigma Types
Part 2 - Using Terms in Sigma Types
Quest 2 - Side Quests
A Tautology / Currying / Cartesian Closed
Quest 3 - Pi Types
Part 0 - Defining Addition
Part 1 - The Statement
Part 2 - Remarks
Quest 3 - Side Quests
Decidability of
isEven
Quest 4 - Paths and Equality
Part 0 - The Identity Type
Part 1 - The Path Space
Part 2 - Properties of the Path Space
Part 3 - Univalence
Quest 4 - Side Quests
Functional Extensionality
Justifying
J
Quest 5 - Dependent Paths
Part 0 - A motivating example
Part 1 - Dependent Paths
Part 2 - How
pathToFun
Interacts with Other Types
Read the Docs
v: latest
Versions
latest
Downloads
pdf
html
epub
On Read the Docs
Project Home
Builds