The lightbulb moment for Voevodsky was apparently realizing that CoC (used in Coq) is almost entirely equivalent to HoTT. So in a sense, Coq actually is kind of based on HoTT, just using different words. (One could maybe say there is a homotopy between CoC and HoTT?? IANAM.) The library they are developing is basically a restatement of HoTT in Coq using more familiar terms/concepts.