Tags:enriched categories, extensive categories, generalised operads and higher dimensional categories
Abstract:
Bicategories have been used for many years to model computational phenomena such as concurrency and binders. The collectivity, Bicat, of bicategories has the structure of a tricategory, which have occasionally appeared explicitly and more often implicitly in the programming semantics literature. But what is a weak n-category in general? Strict n-categories for arbitrary n have been used to model concurrency and in connection with rewriting. So it seems only a matter of time until weak n-categories for arbitrary n prove to be of value for programming semantics too. Here, we explore, enrich, and otherwise mildly generalise a prominent definition by Batanin, as refined by Leinster, together with the surrounding theory: they assumed knowledge of sophisticated mathematics, glossed over the inherent recursion, and did not consider the concerns of programming semantics.
Higher-dimensional categories: induction on extensivity