- Видео 18
- Просмотров 14 622
HoTT-Lectures
Добавлен 3 фев 2015
Семинар по HoTT. Вещественные числа
Семинар по гомотопической теории типов. Определяются вещественные числа по Коши и Дедекинду.
Просмотров: 268
Видео
Семинар по HoTT. Кубические теории типов и высшие индуктивные типы
Просмотров 1313 года назад
Семинар по гомотопической теории типов. Вводится версия кубической теории типов и определяются высшие индуктивные типы данных в ней.
Семинар по HoTT. Фундаментальная группа окружности
Просмотров 663 года назад
Семинар по гомотопической теории типов. Доказывается эквивалентности фундаментальной группы окружности и целых чисел.
Семинар по HoTT. Базовые понятия
Просмотров 1093 года назад
Семинар по гомотопической теории типов. Функции, пути, транспорт, эквивалентности и унивалентность.
Семинар по HoTT. Обрезания и аксиома выбора
Просмотров 473 года назад
Семинар по гомотопической теории типов. Обсуждаются обрезания и аксиома выбора.
Семинар по HoTT. Индуктивные типы
Просмотров 833 года назад
Семинар по гомотопической теории типов. Более подробно обсуждаются различные вариации индуктивных типов.
Семинар по HoTT. Введение
Просмотров 7303 года назад
Семинар по гомотопической теории типов. Вводная лекция.
HoTT 11: Модели теории
Просмотров 6509 лет назад
На этой лекции мы рассмотрим основные вопросы и проблемы, связанные с конструированием моделей (гомотопической) теории типов.
HoTT 10: Метатеоретические свойства системы
Просмотров 3159 лет назад
На этой лекции мы рассмотрим ряд метатеоретических свойств системы, включая каноничность и сильную нормализацию.
HoTT 9: Гомотопические группы
Просмотров 7859 лет назад
На этой лекции мы определим понятие гомотопических групп типа и рассмотрим ряд конструкций, при помощи которых можно их подсчитывать.
HoTT 8: Эквивалентность 1-типов и групп
Просмотров 3829 лет назад
На этой лекции мы закончим доказательство эквивалентности связных 1-типов с отмеченной точкой и групп и начнем изучение произвольных типов.
HoTT 7: Унивалентность
Просмотров 4149 лет назад
На этой лекции мы рассмотрим понятие эквивалентности, введем аксиому унивалентности и начнем конструирование эквивалентности между группами и связными 1-типами с отмеченной точкой.
HoTT 6: 1-типы и группоиды
Просмотров 6939 лет назад
В этой лекции мы определим понятие 1-типа в теории типов и группоида в теории множеств, после чего покажем связь между этими понятиями.
HoTT 5: Тип интервала
Просмотров 6469 лет назад
В начале данной лекции мы рассмотрим небольшой пример использования аксиомы выбора. После чего мы добавим в систему новый тип - тип интервала, и переопределим несколько старых типов, через тип интервала, что решает ряд проблем в прежних формулировках.
HoTT 4: J оператор и множества
Просмотров 5579 лет назад
На этой лекции мы рассмотрим несколько примеров использования J оператора. Также мы введем предикат на типах isSet, и рассмотрим несколько примеров, демонстрирующих, что типы, удовлетворяющие данному предикату, действительно ведут себя как множества.
HoTT 3: Вселенные и индуктивные типы
Просмотров 1 тыс.9 лет назад
HoTT 3: Вселенные и индуктивные типы
HoTT 2: Curry-Howard correspondence
Просмотров 2,1 тыс.9 лет назад
HoTT 2: Curry-Howard correspondence
HoTT 1: Типизированное лямбда исчисление
Просмотров 6 тыс.9 лет назад
HoTT 1: Типизированное лямбда исчисление
Коллеги кто нибудь может дать полное название упоминаемой в лекции "the book"
в обозначении А -> А -> А наверное нужно указывать скобки A -> (A -> A) тк операция неассоциативна
Думаю, предполагается, что операция (->) правоассоциативна
> записано на гитхабе Поделитесь линкой пжлст
не видно текст на правой доске :( хотя, в этом видео это пока не очень важно, наверное
На 59:30 "Вот такая проблемка возникает". -- не уловил, какая проблемка. Всё же вроде хорошо получилось?
Мелковато написано на доске, не всегда различимо
Будет ли выложена четвёртая лекция?
Будет через несколько дней.
Спасибо, очень интересная лекция!
отлично