What parts of homotopy type theory are not possible in Agda or Coq? When we look at the book, Homotopy Type Theory - we see the following topics:

Homotopy type theory 
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are ﬁbrations
2.4 Homotopies and equivalences
2.5 The higher groupoid structure of type formers
2.6 Cartesian product types
2.7 S-types
2.8 The unit type
2.9 P-types and the function extensionality axiom
2.10 Universes and the univalence axiom
2.11 Identity type
2.12 Coproducts
2.13 Natural numbers
2.14 Example: equality of structures
2.15 Universal properties


Now we know that not all of homotopy type theory is possible is Agda and Coq. 

My question is: What parts of homotopy type theory are not possible in Agda or Coq?
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.