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


When 
Nov 07, 2017 from 04:00 PM to 05:00 PM 
Where  IF 4.31/4.33 
Add event to calendar 
vCal iCal 
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 MartinLof 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 realworld 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 higheridentity 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 infinitytopos".
(joint work with James Ladyman)