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

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

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

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

Ну и список литературы, отсортированый по годам. Может форум какой для этого есть специальный?

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

Только не такой "продвинутый" — 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, интерпретация Брауэра — Гейтинга — Колмогорова
Соответствие Карри — Ховарда

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

Ну и список литературы, отсортированый по годам. Может форум какой для этого есть специальный?