...Но главное, что весь предыдущий недельный спринт я вложил в курс "Гомотопическая теория типов для программистов". Продвигается очень тяжело, но зато я буду первым в мире, кто низведёт HoTT до уровня рядовых миддлов мэйнстрима. Ну или возвысит их до уровня HoTT :)

Столько времени к сожалению вкладывать в него долгосрочно нереально, ну хотя бы по нескольку помидорок в день буду стараться.

Пока я сделал БАЗУ: введение в HoTT и MLTT, интуиционистская версия, теория групп, открытое множество, непрерывное отображение, топологическое пространство...

И начал "Базовые понятия": фундаментальная группа, петля, путь, окружность, тор... При этом добавляю мою реализацию HoTT на питоне, с максимумом комментариев.

=

Отвечая на ваш вопрос. Нет никакой практической ценности в изучении HoTT, иначе вся мировая айтишка была бы там. Однако HoTT от этого застрахован, потому что туда очень трудно попасть.
..И все же всегда имеется слабая возможность и для обычного человека войти в эту тему, если он получит правильную карту. Но, предупреждаю заранее, если ему это и удаётся, то результатом становится замешательство, иногда необратимое -- вплоть до полного unemployable.