Можете поиграться:
Интерактивный Конструктор Типов MLTT
(ссылочка пока временная)

MLTT (теория типов Мартина-Лёфа) предлагает нам три ключевые концепции:

1. Зависимые типы. Типы могут зависеть от значений/предикатов/..., например, тип "матрица размером 2x3" или "чётное число" (внутри такого типа могут существовать только чётные значения). Соответственно, мы можем много дополнительных проверок рантайма перенести на фазу компиляции (был такой прекрасный язык Паскаль/Дельфи, а потом Оберон, а до них Алгол 68).

2. Индуктивные типы: позволяют создавать сложные структуры данных из других типов, от натуральных чисел до деревьев и т.д.

3. Универсумы типов: иерархическая система "типов типов", которая помогает избежать парадоксов и обеспечить стабильность сложной типовой системы.

Потому что в MLTT сами типы -- объекты, которые имеют свои собственные типы... И рассуждая в такой парадигме логически, мы неизбежно придём к парадоксу существования "типа всех типов" (Type : Type).
Вот есть тип R, который определяется как "тип всех типов, которые не содержат самих себя". Будет ли R элементом самого себя? Ведь он по определению "не содержит себя", значит, он должен быть элементом типа R...

===

Ну и вот что тут непонятного? Любой сообразительный старшеклассник, хорошо изучивший информатику, это поймёт.
Ну разве что про универсумы не очень, но вы сразу их осознаете вот на таком простейшем примере:
- Универсум Type0 (или Set): содержит "простые" типы, такие как Nat (натуральные числа), Bool (логические значения) и т.д.
- Универсум Type1: содержит типы, которые могут включать в себя типы из Type0, например, типы функций или типы, зависящие от значений.
- Универсум Type2: содержит типы, которые могут включать в себя типы из Type1, и так далее.

И отсюда до гомотопической теории типов HoTT собственно остался всего один шаг: унивалентность. И это на самом деле тоже совершенно простая вещь на нашем программистском уровне, которую ввёл Воеводский:

Эквивалентность типов эквивалентна их равенству.
(Если два типа A и B эквивалентны (то есть существует биекция/отображение между ними, сохраняющая структуру), то они равны как типы: A = B)

И такое дополнение, напоминающее утиную типизацию, однако внезапно позволило формализовать идеи из алгебраической топологии и теории категорий в рамках теории типов!

=

Этот мой тренажёр быстро вас обучит синтаксису всех этих трёх ключевых концепций MLTT (я нагенерил 256 шаблонов задачек, на трёх уровнях сложности). Там даже никакой справки не требуется, по подсказкам и школьник разберётся, просто такой странный квест из простых синтаксических паззлов. А кто проходил мой курс по F#, конечно будет вообще легко и понятно.
А кто не проходил, просто вот на это взгляньте:

A → B означает тип функции (функциональный тип), которая принимает аргумент типа A и возвращает результат типа B.
Например, если A -- это тип натуральных чисел (Nat), а B -- тип булевых значений (Bool), то Nat → Bool — это тип функции, которая принимает натуральное число и возвращает булево значение (например, функция проверки натурального числа на чётность)
В тренажёре вместо "→" указываете "=>"

Дальше, соответственно, можно будет двигаться в семантику MLTT и далее.
Но мне ежедневно сливать на AI по 10-20 долларов, чтобы делать такие вещи в public domain, слишком накладно выходит, совсем не по карману.
Поэтому, следующие версии буду делать только через ваши донаты :)

/don только не надо пожалуйста звёздочки донатить, что я с ними буду делать? в крипту переводить? )

Единственная схема донатов, которая у меня будет -- это вин-вин. С 9 января начну выкладывать новые курсы и секретные материалы для всех, вот покупайте их лучше всего.