If you look at Notes on Chapter 8 you will see what has already been formalized, and I think that's a lot. There are the Coq HoTT library and the Agda HoTT-Agda library which formalize large chunks of Homotopy Type Theory.
To get things done in Coq we needed a special version of Coq that was patched just for the purposes of HoTT. However, Coq is moving in the direction of supporting homotopy type theory, so before long we might be able to do it with standard Coq.
In Agda one has to turn on the
--without-K option, otherwise Agda thinks all types are 0-types. There are some lingering doubts as to whether
--without-K really gets rid of the assumption that everything is a 0-set, or perhaps one could reintroduce it into Agda with tricky uses of pattern matches.
The following aspects of Coq and Agda formalizations are not satisfactory:
The Univalence axiom is stated as a hypothesis. It would be better if it were built into the system. In particular we would like Coq and Agda to understand the computation rules about the Univalence axiom.
Likewise, we have to use hacks to get workable higher-inductive types. Again, it would be better to have direct support.
The trouble with the above deficiencies is that nobody knows how to fix them even in theory. This is an active area of research.
Other than that, I think it's fair to say that HoTT can be mostly done in Coq and Agda, just not in the optimal way.