В двух словах, гомотопическая теория типов отличается от обычного (дискретного) взгляда на математику в том, что в ней "структура равенства" не обязана быть бинарным отношением "да/нет", а может представлять собой ∞-группоид. В частности, это может быть тот же 0-группоид / отношение эквивалентности (обычное равенство для элементов множеств), но может быть и более общий 1-группоид (релевантное понятие равенства для объектов многих 1-категорий), и ещё более общий 2-группоид (соотв. для объектов 2-категорий) и т.д.

К слову, часто в популярных пересказах (в том числе кажется на вики) фразу "в гомотопической теории типов отождествляются изоморфные объекты" понимают неправильно думая, что богатое понятие изоморфизма в ней редуцируется до бедного понятия 0-равенства, когда, на самом деле, это понятие равенства расширяется так, что потенциально может совпадать с изоморфизмом (и быстро становится видно, что это принципиально естественнее, что так и было с самого начала)

По умолчанию типы и простые алгебраические структуры образованные из них — высшие (в семантике теории гомотопий / sSet: типы — ∞-множества т.е. ∞-группоиды, кольца — ∞-кольца и т.д.). Но можно определить n-усеченные типы и n-усечения (в семантике sSet соответствуют усечениям в смысле теории гомотопий — то есть этажам башни Постникова) следующим образом:

X (-1)-усеченный := для любых x, y : X верно, что x = y. В теории типов кванторы и логика устроены так, что эта фраза означает "задана функция, которая по x, y строит элемент типа x = y" (элементы этого типа называют свидетелями равенства — скажем, в некоторых 1-ситуациях это может быть изоморфизм x -> y, ). Ясно, что гомотопически, в предположении исключенного третьего, это условие означает " стягиваемый или пустой": если есть хотя бы одна точка, то функториальное семейство путей реализует стягивание к ней. Эти типы играют роль простых предложений / логических значений (в предположении исключенного третьего соответственно true и false)

X (n+1)-усеченный := для любых x, y : X верно, что тип x = y n-усеченный.

Множества определяются как 0-типы и в гомотопической семантике они в точности совпадают с классическими множествами (для каждых двух элементов их равенство — это просто утверждение/факт). Но тип множеств автоматически является 1-типом, равенство в нем и есть изоморфизм множеств. Тоже самое касается типа групп (определенных через эти множества, а не произвольные типы, я имею в виду, т.е. 1-групп).

1-категория задается следующими данными:
* тип объектов Ob
* для каждых a, b: Ob задано множество Hom(a, b)
* композиция, id
* обычные аксиомы
* естественное отображение =(a, b) -> iso(a, b) является эквивалентностью этих типов [аксиома унивалентности, гарантирующая согласованность изначального равенства на типе Ob и того, что приходит из структуры категории — вообще говоря первое может быть более строгим, что собственно и имеет место для всех категорий в дискретных основаниях, кроме очень узкого класса gaunt категорий]

Итак, легко показать, что тип 1-категорий является 2-типом, а равенством 1-категорий является эквивалентность.

Подробнее объясню скоро на планируемом мини-курсе по HoTT для гомотопистов (анонс будет позже)