Back to Search Start Over

Higher inductive types in $(\infty,1)$-categories

Authors :
Uemura, Taichi
Publication Year :
2024

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.

Details

Database :
arXiv
Publication Type :
Report
Accession number :
edsarx.2410.17615
Document Type :
Working Paper