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.

Homotopy type theory: Univalent foundations of mathematics

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?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s