If I understand the question correctly, one answer is that the rules of type theory are not (supposed to be) arbitrarily chosen independently of each other like the axioms of set theory are. They come in "packages", one for each "type-forming operation", and each package has the same general shape: it consists of a Formation rule, some Introduction rules, some Elimination rules, and some Computation rules.

A Formation rule tells you how to introduce a type, e.g. "if $A$ and $B$ are types, so is $A\times B$". An Introduction rule tells you how to introduce terms in that type, e.g. "if $a:A$ and $b:B$, then $(a,b):A\times B$". An Elimination rule tells you how to *use* terms in that type to construct terms in other types, e.g. "if $f:A\to B\to C$, then $rec(f):A\times B\to C$". And a Computation rule tells you what happens when you apply an Elimination rule to an Introduction rule, e.g. "$rec(f)((a,b)) \equiv f(a)(b)$".

These four groups of rules that pertain to any type former can't be chosen arbitrarily either; they have to be "harmonious". There's no formal definition of what this means, but the idea is that the Introduction and Elimination rules should determine each other, and the Computation rules should tell you exactly how to apply any Elimination rule to any Introduction rule and no more.

A bit more specifically, there are two kinds of type formers: positive ones and negative ones. For a positive type, you choose the Introduction rules, and then the Elimination rules are essentially determined by saying "in order to define a function out of our new type, it suffices to specify its value on all the inputs coming from some Introduction rule". For a negative type, you choose the Elimination rules, and then the Introduction rules are essentially determined by saying "in order to construct an element of our new type, it suffices to specify how all the Elimination rules would behave on that element". In both cases, the Computation rules then say that these "specifications" do in fact hold (as definitional equalities).

So, you can't just arbitrarily postulate Computation rules. I mean, you *can*, but you won't end up with a well-behaved theory. Thus, we have to regard the equalities postulated by higher inductive types as Introduction rules, with correspondingly determined Elimination and Computation rules. (We could try to make them Elimination rules instead, yielding a notion of "Higher Coinductive Type", but there's no consensus yet on what such a thing should look like.)

Why do we require this sort of harmony between the rules? From a computational point of view, it's so that we can actually compute with the Computation rules. If you didn't have that sort of harmony, then you might end up with "stuck" terms with an Elimination form applied to an Introduction form but no applicable Computation rule, or conversely if there were too many Computation rules then you might have some terms that try to "compute" to many different things.

From a category-theoretic point of view, it's because we're specifying objects by universal properties: a positive type former has a "left" universal property like a colimit, while a negative type former has a "right" universal property like a limit. I wrote a blog post about this here.

1more comments