Here is the current state of Coq for HoTT.
Matthieu Sozeau and Hugo Herbelin implemented two command-line options for the trunk version of Coq that replace some of the patches:
Matthieu is working on better universe polymoprhism which will eliminate the need for the first option (which is a hack).
Andrej Bauer wrote configuration scripts for the HoTT library that use autoconf. This makes the library a bit easier to install. The library however requires the latest version of Coq with the new command line options.
There is an ongoing effort to put the ssreflect tactics (just the tactics, no math components) into HoTT, but we’re meeting some technical difficulties.
The Coq working group meets on Wednesday 1:30 — 3 and is occasionally used for some talks.
A page on type classes
Wednesday December 19: HITs in Coq (Bruno Barras)
Wednesday December 5: Universe Polymorphism (Matthieu Sozeau)
Wednesday November 28: The Agda proof assistant (Guillaume Brunerie) slides