A Type-Theoretical Definition of Weak {\omega}-Categories
From MaRDI portal
Publication:5144671
zbMath1452.18024arXiv1706.02866MaRDI QIDQ5144671
Publication date: 19 January 2021
Full work available at URL: https://arxiv.org/abs/1706.02866
03G30: Categorical logic, topoi
03B38: Type theory
18N20: Tricategories, weak (n)-categories, coherence, semi-strictification
Related Items
Unnamed Item, Unnamed Item, Hom weak ω-categories of a weak ω-category, Syntactic approaches to opetopes, A Quillen's Theorem A for strict \(\infty\)-categories. I: The simplicial proof, The construction of set-truncated higher inductive types