HoTT 3: Вселенные и индуктивные типы

В этой лекции мы добавим в систему вселенные, которые, по сути, являются типами типов. После этого мы обсудим понятие индуктивных типов, как для них в общем случае описываются конструкторы и элиминаторы. В конце мы немного поговорим о интуиционистской логике и законе исключенного третьего.