Homotopy Type Theory

Homotopy Type Theory (HoTT) offers the promise of a new foundation for mathematics. The goal is to establish a single language capable of describing, and even building, fields as vast as algebra, topology, and logic. In this framework, the

• rules,
• structures, and
• proofs
  of these mathematical fields all reside within the same unified universe. The key idea is that identity is not a mere proposition but a structured object.

Types

In HoTT, a type can be visualized as a space. This space is populated by items referred to as terms.

• Terms can represent things like numbers, functions, or even types themselves.
• Notation: The colon (:) is used to denote that a term inhabits a particular type (e.g., $x:A$ means term $x$ is in type $A$).
• Distinction from Sets: While types might initially seem like sets, they are fundamentally different, with the main distinction lying in the way types handle equality.

Equality in HoTT: Paths and Structure

In HoTT, equality is not merely a yes-or-no statement; it is understood as a path with shape and structure. There are several ways of "being equal".

• Two terms (e.g., $x$ and $y$ with $x,y:A$) are considered equal if a path exists from one to the other.
• A key feature of HoTT is that multiple paths can exist that demonstrate $x$ is equal to $y$ (e.g., paths $p$ and $q$).
• Equality Type: These proofs of equality (the paths $p$ and $q$) are defined as inhabitants of a special kind of type called an equality type ($x=y$). This type contains all the proofs that one term is equal to another. And we write $p,q:x=y$

Higher Structures (Homotopies)

The concept of equality can be applied recursively: one can inquire whether the path $p$ is equal to the path $q$.

• This relationship is not simply a path, but a path of paths.
• Topologists refer to these paths of paths as homotopy, which is the origin of the theory's name, Homotopy Type Theory.
• It is possible to continue defining these structures to higher levels, speaking of paths of paths of paths, and potentially continuing this structure up to infinity.