Могу быть сильно неправ, но расскажу на пальцах что это такое.
Как обычно, в математике все довольно просто, но математики иногда запутывают ) им и так немного платят )) должна же быть маленькая компенсация ))
===
книга
Homotopy Type Theory:
Univalent Foundations of Mathematics
https://homotopytypetheory.org/book/
Унивалентные основания математики
В. А. Воеводский
ролик на русском от автора
http://www.mathnet.ru/present4281
===
Типы это точно такие же типы данных как и у программистов
Теория типов это какието теоретизирования по вопросу какихто свойств этих типов данных
теория типов утверждает примерно следующее, вот есть разные типы данных и есть их свойства и какието операции можно вводить над типами, и этого достаточно чтобы ее можно было использовать в основаниях математики
это универсальный язык и на нем можно все записать, теорию множеств, теорию категорий и всю прочую математику
помните я вам в двух словах рассказывал в жж что теория категорий это такие специальные направленные графы
дык вот теория типов это по сути правила переписывания цепочек символов
симовлы могут быть разных сортов(видов, категорий), т.е. разных типов
отсюда и название что теория типов
унивалентная, что это?
валентность=связь
уни= один
т.е. односвязная
далее вводится некое преобразование которое и называется односвязным, это преобразование и есть переписывание цепочки или преобразование цепочки символов разных типов
а односвязная это потому что выполняется свойство
если a=b , то f(a)=f(b)
такое f есть унивалентное или односвязное, можно сказать однозначное
дык вот, наша теория изучает самые общие переписывания цепочек
и говорится
цепочки преобразований эквивалентны/одинаковы если они изоморфны. т.е. если их можно преобразовать друг в друга
в целом это весьма очевидно, и это есть главная аксиома этих правил переписываний цепочек
что это все дает? оказывается можно весьма общие разные схемы теорем и доказательств в математике записывать в виде такихх цепочек и доказывать их эквивалентность
т.е. напримерр мы чтото доказали для целых чисел, это можно перенести и на другие числа и мы можем вычислить условия когда это можно
итого это дает нам универсальный язык формализации и программирования
в целом и все вроде )
======
когда я с вами беседовал по поводу иск.интеллекта, о том что такое смысл и т.п.
по сути нечто такое мы тоже делали, у нас тоже универсальный язык, это язык упорядоченных пар, есть эквивалентность, которую устанавливается, есть аналог унивалентного оператора, это просто связь в упорядоченной паре
все что универсальный сильный искин делает, то он делает переписывание цепочек с помощью упорядоченных пар, на языке ИИ это рассуждение, создание ассоциаций это ввод нового унивалентного оператора и прочее
собственно я сказал все это к тому, что мы идем примерно правильным путем и независимым образом воспроизводим примерно такие же структуры
всё )
ps Могу быть очень сильно неправ.