Higher-dimensional categories with finite derivation type

Abstract

We study convergent (terminating and confluent) presentations of n-categories. Using the notion of polygraph (or computad), we introduce the homotopical property of finite derivation type for n-categories, generalizing the one introduced by Squier for word rewriting systems. We characterize this property by using the notion of critical branching. In particular, we define sufficient conditions for an n-category to have finite derivation type. Through examples, we present several techniques based on derivations of 2-categories to study convergent presentations by 3-polygraphs.

References in corpus (4)

• Termination orders for 3-dimensional rewriting
• The three dimensions of proofs
• Two polygraphic presentations of Petri nets
• Intensional properties of polygraphs

Cited by in corpus (8)

• Higher-dimensional normalisation strategies for acyclicity
• Polygraphs of finite derivation type
• Towards 3-Dimensional Rewriting Theory
• Convergent presentations and polygraphic resolutions of associative algebras
• Innocent strategies as presheaves and interactive equivalences for CCS (expanded version)
• A coherence theorem for pseudonatural transformations
• Innocent strategies as presheaves and interactive equivalences for CCS
• Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics