Homotopy Type Theory

Idea

“HoTT = ITT + HIT + UA”

Homotopy Type Theory (HoTT) is an interpretation of intensional Type Theory into homotopy theory. It treats types as spaces, terms as points, and identity types as paths. This framework provides a synthetic approach to homotopy theory and a new foundation for mathematics based on the Univalence Axiom.

Definition

Homotopy Type Theory is a branch of mathematics that combines Type Theory with Homotopy Theory by viewing types as infinity groupoids or spaces. Formally, a type $A$ is a space, and for any $a,b:A$, the identity type $a{=}_{A}b$ is the space of paths from $a$ to $b$.

Fundamentals

Type Theory as Logic

Propositions are represented as types; a proof of a proposition $P$ is a term $p:P$. Constructive logic is recovered through the Curry-Howard Correspondence.

Type Theory as Geometry

Types are viewed as $\infty$-groupoids or spaces. Functions $f:A\to B$ are continuous maps. The identity type $a{=}_{A}b$ is the space of paths from $a$ to $b$ in $A$.

The Identity Type

Path Induction

The eliminator for identity types, $J$, allows for the construction of functions on paths by defining them on reflexivity $ref{l}_a:a=a$. This corresponds to the contractibility of the space of paths with one fixed endpoint.

Higher Inductive Types

Types defined not only by point constructors but also by path constructors. Examples include:

• The Circle $S^1$: One point $base$ and one path $loop:base=base$.
• Suspensions: Generalizing the construction of spheres.
• Truncations: Squashing a type to a specific homotopy level, such as propositional truncation.

Univalence Axiom

The Univalence Principle states that for any two types $A$ and $B$, the map $(A\simeq B)\to (A=B)$ is an equivalence. This identifies equivalent types as being equal, allowing for the substitution of equivalent structures in any context.

Hierarchy of Types

Types are classified by their homotopy level ($n$-types):

• $-2$-types: Contractible types (single point up to homotopy).
• $-1$-types: Propositions (at most one point up to homotopy).
• $0$-types: Sets (discrete spaces where paths are trivial).
• $1$-types: Groupoids (paths exist, but paths between paths are trivial).

Cubical Type Theory

Cubical Type Theory is an extension of HoTT that provides computational content to the univalence axiom and higher inductive types by using cubical structures instead of simplicial ones. It enables functional programming with higher-dimensional data.

Definitions

Homotopy Homotopy Equivalence Weak Infinity Groupoid Whiskering Composition

Results

Eckmann-Hilton Theorem

References

hott2013-book awodey2012-type-theory-homotopy cohen2016-cubical-type-theory