|Time:|| 12:00 - 13:20
Doherty Hall 4303
Department of Mathematical Sciences
Carnegie Mellon University
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.