HoTT means a lot to me (lol) HoTT brought dependent types and interactive theorem proving to the masses. Before HoTT, the number of researchers working serious

HoTT means a lot to me (lol) HoTT brought dependent types and interactive theorem proving to the masses. Before HoTT, the number of researchers working seriously on dependent type theory was probably < 20. This has now changed, and the field is developing at a much more rapid pace than before.