Abstract
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 Leinster's 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 Leinster's approach for defining weak n-categories. In the case that V = Set, the resulting definition of weak n-dimensional V-category agrees with Leinster's definition.
| Original language | English |
|---|---|
| Pages (from-to) | 73-90 |
| Number of pages | 18 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 341 |
| DOIs | |
| Publication status | Published - 1 Dec 2018 |
Keywords
- cartesian monad
- enriched category
- extensive category
- higher dimensional category
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Cite this
Higher Dimensional Categories : Induction on Extensivity. / Cottrell, Thomas; Fujii, Soichiro; Power, John.
In: Electronic Notes in Theoretical Computer Science, Vol. 341, 01.12.2018, p. 73-90.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Higher Dimensional Categories
T2 - Induction on Extensivity
AU - Cottrell, Thomas
AU - Fujii, Soichiro
AU - Power, John
PY - 2018/12/1
Y1 - 2018/12/1
N2 - 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 Leinster's 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 Leinster's approach for defining weak n-categories. In the case that V = Set, the resulting definition of weak n-dimensional V-category agrees with Leinster's definition.
AB - 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 Leinster's 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 Leinster's approach for defining weak n-categories. In the case that V = Set, the resulting definition of weak n-dimensional V-category agrees with Leinster's definition.
KW - cartesian monad
KW - enriched category
KW - extensive category
KW - higher dimensional category
UR - http://www.scopus.com/inward/record.url?scp=85058042751&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2018.11.005
DO - 10.1016/j.entcs.2018.11.005
M3 - Article
VL - 341
SP - 73
EP - 90
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
ER -