Зависимости между термами и типами. Система с операторами над типами \( \lambda\underline{\omega} \). Конструкторы типов. Виды (kinds). Система с зависимыми типами \( \lambda P \). Семейства типов. Виды для семейств типов. Тип зависимого произведения (\( Pi \)-тип). Проблема равенства типов. Системы лямбда-куба. Общие и специальные правила присваивания типов.