Курс "Мова простору"

Програмування

Випуск I: Теорія типів

Перший розділ є введенням у теорію типів, її предметну область та методи комп'ютерних наук. Ми розглянемо основні принципи лямбда-числення, його найпотужнішу версію — System , Calculus of Constructions та Pure Type Systems. Потім ми закодуємо теореми системи типів MLTT в кубічних верифікаторах. Цей розділ охопить типи Pi, Sigma, Path.

HoTT 1.3, 1.4, 1.5, 1.6, 1.12, 2.7, 2.9, 2.11, 6.2

  Випуск I: Інтерналізція теорії типів Мартіна-Льофа

Випуск II: Індуктивні типи

Другий розділ є введенням у базові індуктивні типи та принцип індукції. Індуктивні типи формують основу так званого Calculus of Inductive Constructions, теорії, що лежить в основі Coq. Ми покажемо, як доведення теорем за принципом індукції відрізняється від кубічних конструкцій. Також ми представимо загальне імпредикативне кодування індуктивних типів (Awodey). Цей розділ охопить типи: W, Empty, Unit, Either, Prod, Bool, Maybe, Nat, List. Для неконсистетних систем факультативно розглядаються Fix, Mu, Nu, Free, Cofree.

HoTT 1.7, 1.8, 1.9, 5.1, 5.6

  Випуск II: Індуктивні типи та кодування

Випуск III: Гомотопічна теорія типів

Ця тема дає фундаментальне уявлення про типи Pi як фібрування, що використовуються в конструктивній еквівалентності. Також тут ми розглянемо нескінченну ієрархію типів, що містить вищі глобулярні рівності, які використовуються як основа для IPL, теорії множин та симпліціальної геометрії. Цей розділ охопить типи Fiber, n-Groupoid.

У теорії типів існують три рівності: 1) вбудована в перевірник типів, що представляє тип Id, Equ або Path з J-елімінатором; 2) еквівалентність на основі фібрування; 3) ізоморфізм, що містить ретракт і секцію. Цей факт призводить до аксіоми унівалентності, яка стверджує, що всі еквівалентність дорівнює простору шляхів, і це може бути доведено в кубічних перевірниках типів. Цей розділ охопить типи: Equiv, Iso, Homotopy, Univalence, Injective, Surjective.

HoTT 2.1, 2.3, 2.4, 2.6, 2.7

  Випуск III: Гомотопічна теорія типів

Випуск IV: Вищі індуктивні типи

Однією з основних мотивацій HoTT є конструктивна геометрія та клітинні комплекси, простори, побудовані шляхом склеювання n-дисків уздовж їхніх меж. У цьому розділі ми покажемо, як будувати топологічні примітиви та як міркувати про них. Цей розділ охопить типи: Line, Suspension, n-Sphere, Pushout, Pullback, Truncation, Quotient.

HoTT 6.3, 6.4, 6.5, 6.6, 6.9, 6.10

  Випуск IV: Вищі індуктивні типи

Випуск V: Модальності

Цей розділ охопить тип Infinitesimal.

HoTT 7.7

  Випуск V: Модальності

Математика

Випуск XXII: Теорія множин

Цей розділ є введенням у інтуїціоністську логіку висловлювань (IPL), її відмінність від класичної логіки, аксіому вибору, закон виключеного третього, пропозіційну урізку, теорему Хедберга, вирішувані типи, конструктивну теорію множин. Цей розділ охопить типи: Prop, Set, Decidable, Stable, Discrete.

HoTT 3.1, 3.3, 3.11

Випуск XXIII: Теорія категорій

Понад 10 медалей Філдса отримано завдяки теорії категорій (CT) як інструменту. Для занять математикою CT є вирішальною. Як супровід до розділу HoTT про CT, ми пропонуємо курс Стіва Аводі (учня Сондерса Мак Лейна), який також зробив HoTT можливим.

Цей розділ дасть фундаментальне уявлення про такі типи: Precategory, Rezk Completion, Functor, Natural Transformation, Adjoint, Cone, Structure Identity Principle, Limit, Pullback, Kan Extension, Monomorphism, Epimorphism, Universal Mapping Property.

Основне застосування CT у комп'ютерних науках — побудова категоріальної моделі залежно типізованого лямбда-числення як внутрішньої мови локально декартово замкненої категорії. У цьому курсі згадуються дві моделі: Categories with Families (Dybjer) та C-Systems (Voevodsky).

Також як приклади екземплярів категорій використовуються такі типи: Категорія множин, Категорія функцій, Категорія категорій, Категорія функторів, Срізна категорія, Добуткова категорія. Використовуючи їх, ми можемо побудувати базові приклади 2-категорій та дати дуже базове введення в -Категорії. Типи в цьому розділі: Category of Commutative Monoids, Category of Abelian Groups, Grothendieck Group.

  Випуск XXII: Теорія категорій

  Випуск XXX: Контекстуальні категорії для теорії типів Мартіна-Льофа

Випуск XXXIX: Теорія топосів

Теорія топосів дасть більш глибоке розуміння категоріальних моделей і створить міцніший фундамент для побудови мосту між CT та логікою простору.

У цьому розділі я згадаю типи Subobject Classifier та Topos.

  Випуск XXXIX: Формальний топос на категорії множин

Випуск IX: Алгебраїчна топологія

Типи в цьому розділі: Monoid, Commutative Monoid, Group, Ring, Abelian Group, Abelian Ring, Hopf, Loop Space, Homotopy Group.

Випуск X: Диференціальна геометрія

Типи в цьому розділі: Abstract Homogeneous Structure, Shape, Étale Map, Automorphism, Fiber Bundle, Manifold, Covering Space (G-Set).

Історія