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)?