When we look at the book, Homotopy Type Theory - we see the following topics:Homotopy type theory 2.1 Types are higher groupoids2.2 Functions are functors2.3 Type families are brations2.4 Homotopies and equivalences2.5 The higher groupoid structure of type formers2.6 Cartesian product types2.7 S-types2.8 The unit type2.9 P-types and the function extensionality axiom2.10 Universes and the univalence axiom2.11 Identity type2.12 Coproducts2.13 Natural numbers2.14 Example: equality of structures2.15 Universal propertiesNow 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?
What parts of homotopy type theory are not possible in Agda or Coq?
type systems
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.