Thanks to you (and Chinjut) for the replies. I don't know how to correlate your reply to Chinjut's, though (or vice versa). Could either of you take a stab at it? Are you saying the same thing in different ways? Or are you actually disagreeing?
So when you said, "at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions", That was what Chinjut meant by "Homotopy Type Theory axiomatizes weak omega groupoids; it gives you formal rules you can manipulate to reason about weak omega groupoids"? That is, those lowest-level rules don't assume weak omega groupoids; they turn out to define weak omega groupoids?