Mathematical logic seminar - October 21, 2008

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 IV


Last week, we defined and played around with globular operads, which formalise the structure "a set of operation symbols for composing pasting diagrams in a globular set; and laws specifying how these operations compose".

This week, we'll finally define a weak omega-category (as an algebra for a particular globular operad) (definition from Leinster 2004), and construct the ``fundamental weak omega-category'' of a type in Martin- Löf intensional type theory.

Here are handwritten notes from last week's talk.