Benno van den Berg (Darmstadt)

Types as weak omega-categories

Abstract: Fix a type X in a context \Gamma. Define a globular set as
follows: A_0 consists of the terms of type X in context \Gamma, modulo
definitional equality; A_1 consists of terms of the types Id(X,p,q) (in
context \Gamma) for elements p, q in A_0, modulo definitional equality;
A_2 consists of terms of well-formed types Id(Id(X,p,q),r,s) (in context
\Gamma) for elements p, q in A_0, r, s in A_1, modulo definitional
equality; etcetera...

What is the structure of this globular set? That of a weak omega-groupoid,
certainly. But unless I missed something there is no definition of a weak
omega-groupoid for globular sets. However, there is a definition of a weak
omega-category, especially the one explained in detail in Tom Leinster's
book "Higher operads, higher categories". I will show that the globular
set defined above is a weak omega-category in precisely this sense.