Constructing Higher Inductive Types as Groupoid Quotients
Constructing Higher Inductive Types as Groupoid Quotients
In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in …