A general syntax for nonrecursive higher inductive types

Higher Inductive Types are one of the most interesting features of HoTT, as they let us define geometrical objects into the theory. However, unlike inductive types, there is not yet a general schema telling us what exacly an HIT is, or what its corresponding rules in the calculus are. In fact, HITs are often given via “ad hoc” definitions, as in [7, 8]. In this paper we propose a general syntax schema that encapsulates a broad family of nonrecursive HITs. We generalize the concepts of transport and dependent application to higher paths, which we use to give a procedure to extract the elimination rule and the related computation rules.