Викиучебник по теории типов посоветуйте, пожалуйста.

Только не такой "продвинутый" — https://en.wikibooks.org/wiki/Homotopy_Type_Theory_using_the_Agda_HoTT_library
а попроще, более "от печки".

Нужна схема, что в каком порядке изучать.

И список понятий, которые надо знать, например:
2000, Владимир Воеводский, Гомотопическая теория типов (HoTT), https://github.com/HoTT/book/wiki/Nightly-Builds
1991, Хенк Барендрегт, Лямбда-куб
1988, Стефано Берарди, Чистая система типов
1889, Джузеппе Пеано, арифметика Пеано, аксиомы Пеано
Трансфинитная индукция
Математическая индукция
1925, интерпретация Брауэра — Гейтинга — Колмогорова
Соответствие Карри — Ховарда

логика высказываний соответствует простому типизированному λ-исчислению
исчисление предикатов — λ-исчислению с зависимыми типами
логика высказываний второго порядка — полиморфному λ-исчислению

Ну и список литературы, отсортированый по годам.

Может форум какой для этого есть специальный?
Только не такой — https://www.reddit.com/r/ProgrammingLanguages/comments/b7qecp/domain_theory_and_type_theory/
а русскоязычный.

Викиучебник по теории типов посоветуйте, пожалуйста.

Только не такой "продвинутый" — https://en.wikibooks.org/wiki/Homotopy_Type_Theory_using_the_Agda_HoTT_library
а попроще, более "от печки".

Нужна схема, что в каком порядке изучать.

И список понятий, которые надо знать, например:
2000, Владимир Воеводский, Гомотопическая теория типов (HoTT), https://github.com/HoTT/book/wiki/Nightly-Builds
1991, Хенк Барендрегт, Лямбда-куб
1988, Стефано Берарди, Чистая система типов
1889, Джузеппе Пеано, арифметика Пеано, аксиомы Пеано
Трансфинитная индукция
Математическая индукция
1925, интерпретация Брауэра — Гейтинга — Колмогорова
Соответствие Карри — Ховарда

логика высказываний соответствует простому типизированному λ-исчислению
исчисление предикатов — λ-исчислению с зависимыми типами
логика высказываний второго порядка — полиморфному λ-исчислению

Ну и список литературы, отсортированый по годам.

Может форум какой для этого есть специальный?
Только не такой — https://www.reddit.com/r/ProgrammingLanguages/comments/b7qecp/domain_theory_and_type_theory/
а русскоязычный.

Открыл учебник
2022, Кудрявцева И. А. & Швецкий М. В., Программирование теория типов
на странице 24-25, там написано:
Typ — так будем записывать называние множества типов, а конструировать его будем из символов `0` и круглых скобок.
у меня сразу вопросы:
— есть соглашение по скобкам, ок. Но что если склеиваются два типа с уже по-разному расставленными скобками?
например
(0 0) (0 0), это ведь не то же самое, что ( ( (0 0 ) 0 ) 0 ), и не то же самое, что соглашению о правоассоциативности.
это важно, это неважно, зачем вообще конструировать это множество? Почему его конструировать именно так?