Abstract
This paper develops a general categorical semantics for higher inductive types. The work interprets these types within suitably structured model categories, providing a framework to rigorously validate their formation, introduction, elimination, and computation rules.
Categorical Framework
The framework requires model categories that are locally presentable and combinatorial category. To interpret the underlying dependent type theory, the model category must support dependent products, dependent sums, and identity types, which are typically modeled using right proper fibrations and path objects.
Semantics of Constructors
This work models higher inductive types as initial algebras of polynomial endofunctors or signatures. The existence of these initial algebras is established using transfinite construction techniques within locally presentable categories.
Point Constructors
The paper interprets point constructors as standard algebraic operations that generate the discrete elements or 0-cells of the underlying space.
Path Constructors
The work interprets path constructors using cell attachments or homotopy colimits. The model category uses cylinder objects to interpret these constructors as homotopies between paths. The elimination principle of the higher inductive type corresponds directly to the universal property of the initial algebra in the model category.
Syntax-Semantics Correspondence
The authors delineate a formal syntax for a broad class of higher inductive types and prove that any model category satisfying the specified combinatorial and accessibility conditions supports this syntax. This enables interpretation of pushouts, suspensions, truncations, and spheres in standard foundational models such as the Quillen model category of simplicial sets.