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 III

Abstract: 
Last week, I defined strict ncategories, and explained why we'd like to "weaken" the notion, with motivating "hopedfor examples" from topology and type theory. As a warmup to our definition of weak ncategories, I showed how to use operads to weaken the notion of a monoid. This week, I'll restate the definition of an operad in a form which lets us generalise it, and then, using generalised operads, define weak ncategories; this done, I will start to show how they arise from intensional type theory. Here are handwritten notes from last week's talk. 