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.
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.