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 omega-category (as an algebra for a particular globular operad) (definition from Leinster 2004), and construct the ``fundamental weak omega-category'' of a type in Martin- Löf intensional type theory.

Here are handwritten notes from last week's talk.