Higher Dimensional Categories: Induction on Extensivity

In this paper, we explore, enrich, and otherwise mildly generalise a prominent definition of weak n -category by Batanin, as refined by Leinster, to give a definition of weak n -dimensional V -category, with a view to applications in programming semantics. We require V to be locally presentable and to be (infinitarily) extensive, a condition which ensures that coproducts are suitably well-behaved. Our leading example of such a V is the category ω - Cpo , ω - Cpo -enriched bicategories already having been used in denotational semantics. We illuminate the implicit use of recursion in Leinsteru0027s definition, generating the higher dimensions by a process of repeated enrichment. The key fact is that if V is a locally presentable and extensive category, then so are the categories of small V -graphs and small V -categories. Iterating, this produces categories of n -dimensional V -graphs and strict n -dimensional V -categories that are also locally presentable and extensive. We show that the free strict n -dimensional V -category monad on the category of n -dimensional V -graphs is cartesian. This, along with results due to Garner, allows us to follow Batanin and Leinsteru0027s approach for defining weak n -categories. In the case that V = Set , the resulting definition of weak n -dimensional V -category agrees with Leinsteru0027s definition.