## Homotopy Type Theory and Univalent Foundations

This site serves to collect and disseminate research, resources, and tools for the investigation of homotopy type theory, and hosts a blog for those involved in its study.

Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning.  As the natural logic of homotopy, constructive type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos.

Univalent Foundations of Mathematics is Vladimir Voevodsky’s new program for a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory. The type theoretic univalence axiom relates propositional equality on the universe with homotopy equivalence of small types. The program is currently being implemented with the help of the automated proof assistant Coq.  The Univalent Foundations program is closely tied to homotopy type theory and is being pursued in parallel by many of the same researchers.

NEWS: The HoTT Book is now available!  Get it here.

### 4 Responses to Homotopy Type Theory and Univalent Foundations

1. HoTT says:

Here is a page that explains how to use LaTeX in a WordPress posting. Basically, instead of writing \$formula\$ you write “latex formula” enclosed in \$-signs. It even works in comments: $\Sigma x:A\, \Pi y:A.\, \mathsf{Id}_A(x,y)$.

2. Philipp Schuster says:

Is there an official forum / mailing list / subreddit / irc channel where one can ask questions and discuss the book and especially the exercises?

• Cris Perdue says:

You might want to try the recently-created “HOTT Amateurs” Google Group (https://groups.google.com/forum/#!forum/hott-amateurs). There may be other options as well.

• Hi,

There is in fact a recently created Homotopy Type Theory channel on the freenode IRC network. The channel is ##hott (note the double hash!).

You can connect to it through the chat.freenode.net server. More information, including a web-based chat client, at https://freenode.net

Cheers,
Darin