Time:  12:00  13:20 
Room: 
Doherty Hall 4303

Speaker: 
Peter Lumsdaine Department of Mathematical Sciences Carnegie Mellon University 
Title: 
Intensional type theory and higher category theory I

Abstract: 
MartinLöf Type Theory is a powerful and popular logical framework, intensional at its core but with natural extensionality principles that can be added. Unfortunately, for a long time, all the wellunderstood semantics for MLTT were extensional  unfortunately, since the weaker intenstional theory has > not only philosophical interest but also various prooftheoretic advantages (eg decidable typechecking). Higherdimensional Category Theory deals with structures comprising not only objects ("0cells") and arrows between them ("1cells"), but also 2cells between 1cells, 3cells between 2cells, and so on. (Think of points in a topological space, paths between points, homotopies between paths, higher homotopies between homotopies...) The pictures one draws are very pretty, but the combinatorics of formalising this can be daunting. Starting with the work of Hofmann and Streicher, it has recently been realised that higher categories give natural nonextensional models of MLTT. Intuitively, if types are modelled by objects and terms of a type by arrows into that object (as in the usual extensional semantics), then proofs of equality between terms are 2cells between their arrows, proofs of equality between _these_ are 3cells, and so on ad infinitum. In these talks I aim to make precise the above background, leading up to my current work, and the eventual goal of showing that terms of any type in MLTT naturally have the structure of a weak \omegagroupoid. Light reading: http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory "The tale of ncategories", starting in http://math.ucr.edu/home/baez/week73.html about 1/3 of the way down. Heavy reading: NordstromPetersonSmith, "Programming in MartinLöf's Type Theory" http://www.cs.chalmers.se/Cs/Research/Logic/book/ Leinster, "Higher operads, higher categories", http://www.maths.gla.ac.uk/~tl/book.html 