I have been trying to make my way through the homotopy type theory book, slowly but surely, and I just finished reading this introductory series of 3 articles on hott on ScienceForAll.

http://www.science4all.org/le-nguyen-hoang/homotopy-type-theory/

At some point, he describes identity proofs and higher inductive types, he shows how you could construct the integers starting with a base element 0 and two constructors, up (u) and down (d), such that

udA=A,

for any "integer" A. Now he says that one way of reducing the complexity of the type and flattening it is to use higher order inductive types and have two identity constructors:

id_ud (n) : n = u(d(n)),

id_du (n) : n = d(u(n))

Now, my question is simply: Why can't we just make up this type by playing around with computation rules? Couldn't we just posit an induction principle that would say something like:

ind_Z (C,0) := C(0),

ind_Z (C, u(d(n))) := ind_Z (C, n),

ind_Z (C, d(u(n))) := ind_Z (C, n)

I'm aware that we'd get stuck at something like uudd(0), but then I'm sure we could have more rules to swap the ups and downs around or something.

Then, having those equalities at the definitional level, u(d(n))=n : Z (3-bar equality symbol), we would get the equality type from above u(d(n))=n (as a type). Is the problem that it's too strong?

Thank you very much