Monoidal weak ω-categories as models of a type theory

DOI10.1017/S0960129522000172arXiv2111.14208MaRDI QIDQ6149952

Unnamed Author

Publication date: 5 March 2024

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Abstract: Weak $omega$-categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored, based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of weak $omega$-groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this definition of globular weak $omega$ obreakdash-groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type theory called CaTT, whose models are weak $omega$-categories. Here, we generalize this approach to monoidal weak $omega$-categories. Based on the principle that they should be equivalent to weak $omega$-categories with only one $0$-cell, we are able to derive a type theory MCaTT whose models are monoidal categories. This requires changing the rules of the theory in order to encode the information carried by the unique $0$-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory MCaTT and the type theory CaTT. Our main contribution is to show that these translations relate the models of our type theory to the models of the type theory CaTT consisting of $omega$-categories with only one $0$-cell, by analyzing in details how the notion of models interact with the structural rules of both type theories.

Full work available at URL: https://arxiv.org/abs/2111.14208

zbMATH Keywords

dependent type theoryhigher categoriesdeloopingmonoidal \(\omega\)-categories

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Higher-dimensional word problems with applications to equational logic
• Limits indexed by category-valued 2-functors
• Monoidal globular categories as a natural environment for the theory of weak \(n\)-categories
• Types are weak ω -groupoids
• Weak ω-Categories from Intensional Type Theory
• Internal type theory
• Higher-dimensional algebra and topological quantum field theory
• A Type-Theoretical Definition of Weak {\omega}-Categories
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: Monoidal weak ω-categories as models of a type theory