Рогозин Д.Д., Родин А.В. Теория типов в логике и основаниях математики

М.: Институт Философии РАН, 2016. — 66 с.Введение
Типы в исчислении предикатов и в лямбда-исчислении
Теория типов Б. Рассела и А. Уайтхеда
Лямбда-исчисление: чистое и типовое. Комбинаторная логика. Соответствие Карри-Говарда
Теория категорий и типы
Базовые определения теории категорий
Декартово замкнутые категории
Пример декартово замкнутой категории
Категории над объектами и локально декартово замкнутые категории
n-категории
Декартово замкнутые категории и типовое лямбда-исчисление
Теория типов П. Мартина-Лефа
Основные определения
Теоретико-категорная модель теории зависимых типов (экстенсиональный вариант)
Гомотопическая интерпретация теории конструктивных типов
Базовые определения теории гомотопий
Фундаментальные и высшие группоиды
Типы как высшие группоиды
Семейства типов как расслоения, суммы и произведения
Высшие индуктивные типы
Гомотопические n-типы
Заключение
Список литературы