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)

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