Ну, да, такое случается с многими каждый раз, когда они решают поизучать гомотопическую теорию типов. Причём, когда вы хотите узнать побольше о HoTT, то ожидаете 690 страниц теории категорий, но на самом деле получаете 890 страниц Agda :)

И в целом, теоркат на пути к HoTT совсем не первый, не второй и не третий шаг.

Иначе вы не въедете в теоркат на уровне универсальных пропертей вроде UMP.