arXiv · 2410.17615
Higher inductive types in $(\infty,1)$-categories
Abstract
We propose a definition of higher inductive types in $(\infty,1)$-categories with finite limits. We show that the $(\infty,1)$-category of $(\infty,1)$-categories with higher inductive types is finitarily presentable. In particular, the initial $(\infty,1)$-category with higher inductive types exists. We prove a form of canonicity: the global section functor for the initial $(\infty,1)$-category with higher inductive types preserves higher inductive types.
Explore related subjects
Keep this discovery
Taichi Uemura. 2024-10-23. Higher inductive types in $(\infty,1)$-categories. https://arxiv.org/abs/2410.17615
Cite the original work for its findings. Save a collection to share your selection of sources.