Search

• < Previous
• 1
• Next >

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&nbsp;[&hellip;]