Higher dimensional categories: recursion on extensivity

Research output: Contribution to conferencePaper

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.
LanguageEnglish
StatusAccepted/In press - 2018

Fingerprint

Recursion
High-dimensional
Semantics
Computer programming
n-dimensional
Graph in graph theory
Bicategory
Denotational Semantics
Coproducts
Monads
Cartesian
Higher Dimensions
Programming
Generalise

Keywords

  • higher dimensional category
  • enriched category
  • extensive category
  • cartesian monad

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

Cite this

Higher dimensional categories: recursion on extensivity. / Power, Anthony; Cottrell, Thomas; Fujii, Soichiro.

2018.

Research output: Contribution to conferencePaper

@conference{a13dcdd441dd4d16bbd6ba1f5adac375,
title = "Higher dimensional categories: recursion 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 suitablywell-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 thatare 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 withLeinster’s definition.",
keywords = "higher dimensional category, enriched category, extensive category, cartesian monad",
author = "Anthony Power and Thomas Cottrell and Soichiro Fujii",
year = "2018",
language = "English",

}

TY - CONF

T1 - Higher dimensional categories: recursion on extensivity

AU - Power,Anthony

AU - Cottrell,Thomas

AU - Fujii,Soichiro

PY - 2018

Y1 - 2018

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 suitablywell-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 thatare 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 withLeinster’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 suitablywell-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 thatare 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 withLeinster’s definition.

KW - higher dimensional category

KW - enriched category

KW - extensive category

KW - cartesian monad

M3 - Paper

ER -