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

TL;DR

This paper defines higher inductive types within $( abla,1)$-categories, demonstrating their existence, presentability, and a form of canonicity, advancing the understanding of type theory in higher category contexts.

Contribution

It introduces a definition of higher inductive types in $( abla,1)$-categories and proves their existence and properties, including initiality and canonicity.

Findings

The $( abla,1)$-category of such categories is finitarily presentable.

The initial $( abla,1)$-category with higher inductive types exists.

The global section functor preserves higher inductive types.

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.