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.