Собственно вопрос на самом деле весьма общий. Мне кажется, что какие-то вещи в изучении математики можно пропустить и изучить только более абстрактную конструкцию. Тупой пример: нет особого смысла изучать классическую алгебраическую геометрию (Шафаревич), можно сразу учить в духе Хартсхорна. Гипотетический пример: нет смысла учить комбинаторные штучки в inf-категориях, если HoTT всё-таки окажется естественным "inner language" для них. Поправь, если ошибаюсь.

О не_фриках, Urs Schreiber вроде бы ратует за HoTT в физике (https://golem.ph.utexas.edu/category/2012/05/what_is_homotopy_type_theory_g.html). Но мне недостаточно компетенции, чтобы понять, насколько это реально важно и глубоко ли оно лежит.