Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminars LFCS seminar: Stuart Presnell: What is Homotopy Type Theory?

LFCS seminar: Stuart Presnell: What is Homotopy Type Theory?

— filed under: ,

  • LFCS Seminar
  • Upcoming events
When Nov 07, 2017
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal

In this talk I'll give an introduction to Homotopy Type Theory (HoTT) in its various aspects. HoTT is many things: it's an intensional dependent type theory based on Martin-Lof Type Theory; a 'synthetic' reconstruction of homotopy theory (the theory of topological spaces up to continuous distortion); a proposed new foundation for mathematics; and the basis for a (purportedly) more practical formalisation of mathematics that promises to bring automated proof verification within reach of real-world mathematical practice.

After sketching some of the reasons why people are excited about HoTT, I'll present the components of the theory, with focus on the more exotic elements such as the identity and higher-identity types, the Univalence axiom (which allows isomorphic structures to be identified), and Higher Inductive Types which introduce ideas from homotopy theory directly into the type theory.

Finally, I'll address the question "What (exactly) is Homotopy Type Theory?” Of the various components described above, is there any principled way to say that some of them belong to the essential core of the theory while others are optional extras? To answer this I'll try to explain the slogan that "HoTT is (or should be) the internal language of an infinity-topos".

(joint work with James Ladyman)


Document Actions