Раньше у меня было какое-то подобие личности, а потом я изучил теорию типов...

Первый (из семи) уровней рационального просветления ментата -- это освоить теоркат пониманием локальных декартово замкнутых категорий (ибо это категориальная модель лямбда-исчисления с зависимыми типами), симметричных моноидальных категорий (как обобщение лямбда-исчисления с гом- джаббаром функтором) и категории коммутативных диаграмм. Ну и, соответственно, изучить мои гайды по HoTT/CoC/CTT.