|Time:|| 12:00 - 13:20
Doherty Hall 4303
Department of Mathematical Sciences
Carnegie Mellon University
Intensional type theory and higher category theory IV
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.