Martin-Lö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 well-understood semantics for MLTT were extensional --- unfortunately, since the weaker intenstional theory has --> --not only philosophical interest but also various proof-theoretic advantages (eg decidable type-checking).

Higher-dimensional Category Theory deals with structures comprising not only objects ("0-cells") and arrows between them ("1-cells"), but also 2-cells between 1-cells, 3-cells between 2-cells, 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 non-extensional 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 2-cells between their arrows, proofs of equality between _these_ are 3-cells, 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 \omega-groupoid.

Light reading:

http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory "The tale of n-categories", starting in http://math.ucr.edu/home/baez/week73.html about 1/3 of the way down.

Heavy reading:

Nordstrom-Peterson-Smith, "Programming in Martin-Lö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