• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Гомотопическая теория типов

2018/2019
Учебный год
RUS
Обучение ведется на русском языке
4
Кредиты
Статус:
Курс по выбору
Когда читается:
1-й курс, 1, 2 модуль

Преподаватель

Программа дисциплины

Аннотация

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

Цель освоения дисциплины

  • формирование у студентов теоретических знаний и практических навыков использования гомотопической теории типов
Планируемые результаты обучения

Планируемые результаты обучения

  • Демонстрирует знание эквивалентности сигма типов, свойств функций pmap и transport, знает аксиому унивалентности, параметризированные типы и конструкции над ними
  • Демонстрирует знание понятий пропорционального обрезания и закона исключенного третьего, знает понятия конечных множеств и пропозиционального обрезания. Знает понятия эквивалентности, вложений и сюрьекции
  • Умеет сравнивать категории в HoTT и ZFC, знает категории функторов , понятие подкатегории и эквивалентности подкатегорий
Содержание учебной дисциплины

Содержание учебной дисциплины

  • Виды типов и функций
    Стягиваемые типы, эквивалентность сигма типов, свойства функций pmap и transport. Эквивалентности типов, аксиома унивалентности, параметризованные типы и конструкции над ними. Утверждения, множества, вложения, разрешимые множества.
  • Классические принципы
    Пропозициональное обрезание, обрезанные и необрезанные квантор существования и дизъюнкция, закон исключенного третьего, resizing axiom, конечные множества. Конечные множества и пропозициональное обрезание, аксиома выбора, необходимость аксиомы выбора, аксиома выбора для конечных множеств. Фактор множества, AC влечет LEM. Эквивалентности, вложения и сюръекции
  • Унивалентные категории
    Категории, группоиды, примеры. Сравнение категорий в HoTT и ZFC, (ко)пределы. Категория функторов, подкатегории, эквивалентности категорий, пополнение Резка.
Элементы контроля

Элементы контроля

  • неблокирующий Домашнее задание 1
  • неблокирующий Домашнее задание 2
  • неблокирующий Экзамен
Промежуточная аттестация

Промежуточная аттестация

  • Промежуточная аттестация (2 модуль)
    0.25 * Домашнее задание 1 + 0.25 * Домашнее задание 2 + 0.5 * Экзамен
Список литературы

Список литературы

Рекомендуемая основная литература

  • Del Mar González, M., Yang, P. C., Gambino, N., & Kock, J. (2015). Extended Abstracts Fall 2013 : Geometrical Analysis; Type Theory, Homotopy Theory and Univalent Foundations. Cham: Birkhäuser. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=1094638

Рекомендуемая дополнительная литература

  • Heller, J., Krishna, A., & Ostvaer, P. A. (2014). Motivic homotopy theory of group scheme actions. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsarx&AN=edsarx.1408.2348