Abstract

Higher inductive types are a key feature of Homotopy Type Theory. Higher inductive types generalise ordinary inductive types, by not only having constructors for elements (points), but also constructors for equalities between elements (paths), constructors for equalities between equalities, etc. In spite of their importance for the theory, the syntax and semantics of higher inductive types are not yet fully understood. To this end we look at the special case of “one-dimensional” higher inductive types (1-hits), that is, higher inductive types with only point and path constructors. A general form for an introduction rule for a 1-hit is proposed, as well as an inversion principle for deriving the elimination and equality rules from the introduction rules. We also show that the setoid model supports this schema. Finally, we outline the extension of this schema to 2-hits and their interpretation as groupoids.