A general syntax for nonrecursive higher inductive types