Higher inductive types in $(\infty,1)$-categories
Category Theory
2024-10-24 v1 Logic in Computer Science
Logic
Abstract
We propose a definition of higher inductive types in -categories with finite limits. We show that the -category of -categories with higher inductive types is finitarily presentable. In particular, the initial -category with higher inductive types exists. We prove a form of canonicity: the global section functor for the initial -category with higher inductive types preserves higher inductive types.
Keywords
Cite
@article{arxiv.2410.17615,
title = {Higher inductive types in $(\infty,1)$-categories},
author = {Taichi Uemura},
journal= {arXiv preprint arXiv:2410.17615},
year = {2024}
}