Mathematical logic seminar - October 14, 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 III


Last week, I defined strict n-categories, and explained why we'd like to "weaken" the notion, with motivating "hoped-for examples" from topology and type theory. As a warmup to our definition of weak n-categories, 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 n-categories; this done, I will start to show how they arise from intensional type theory.

Here are handwritten notes from last week's talk.