Homotopy type theory and Gödel's incompleteness theorems Kurt Gödel's incompleteness theorems  establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic". 

Homotopy Type Theory provides an alternative foundation for mathematics, a univalent foundation based on higher inductive types and the univalence axiom. 
The HoTT book explains that types are higher groupoids, functions are functors, type families are ﬁbrations, etc. 

The recent article "Formally Verified Mathematics" in CACM 
by Jeremy Avigad and John Harrison 
discusses HoTT with respect to 
formally verified mathematics and automatic theorem proving. 


  Do Gödel's incompleteness theorems apply to HoTT?


And if they do,


  is homotopy type theory impaired by Gödel's incompleteness theorem 
  (within the context of formally verified mathematics)?
HoTT "suffers" from Gödel incompleteness, of course, since it has a computably enumerable language and rules of inference, and we can formalize arithmetic in it. The authors of the HoTT book were perfectly aware of its incompletness. (In fact, this is quite obvious, especially when half of the authors are logicians of some sort).

But does incompleteness "impair" HoTT? No more than it does any other formal system, and I think the whole issue is a bit misguided. Let me try an analogy. Suppose you have a car which can't take you everywhere on the planet. For instance, it can't climb vertically up a wall. Is the car "impaired"? Of course, it can't get you to the top of the Empire State building. Is the car useless? Far from it, it can take you too many other interesting places. Not to mention that the Empire State building has elevators.