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

Abstract: 
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 omegacategory (as an algebra for a particular globular operad) (definition from Leinster 2004), and construct the ``fundamental weak omegacategory'' of a type in Martin Löf intensional type theory. Here are handwritten notes from last week's talk. 