Higher Dimensional Categories

Induction on Extensivity

Thomas Cottrell, Soichiro Fujii, John Power

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)73-90
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume341
DOIs
Publication statusPublished - 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 journalArticle

@article{e6ca732e00614c33bf945c3f7ccf20a1,
title = "Higher Dimensional Categories: Induction on Extensivity",
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.",
keywords = "cartesian monad, enriched category, extensive category, higher dimensional category",
author = "Thomas Cottrell and Soichiro Fujii and John Power",
year = "2018",
month = "12",
day = "1",
doi = "10.1016/j.entcs.2018.11.005",
language = "English",
volume = "341",
pages = "73--90",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

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 -