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