¹In particular, in the language of §1.1, this means that our higher inductive types are a mix of rules (specifying how we can introduce such types and their elements, their induction principle, and their computation rules for point constructors) and axioms (the computation rules for path constructors, which assert that certain identity types are inhabited by otherwise unspecified terms). We may hope that eventually, there will be a better type theory in which higher inductive types, like univalence, will be presented using only rules and no axioms.