HoTT 5: Тип интервала

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