Гомотопічна теорія типів

Навчальна програма для студентів третього курсу

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

Вступ

Цей курс є сучасним вступом в теорію типів, яка використовується для побудови не тільки мов програмування, але і мов для математичної верифікації. Оскільки модальна гомотопічна теорія типів підходить для формалізації усієї математики її ще називають "мовою простору".

Серія лекцій присвячена базовій бібліотеці Групоїд Інфініті та здобуттю навичок програмування математичних визначень та теорем на одній з реалізацій цієї теорії типів — мові Anders.

Мотивація

Головні завдання курсу: 1) безпосередня побудова термів-доведень в кубічній теорії типів за допомогою комп'ютерної верифікації; 2) вирішення домашній завдань або вправ з підручника HoTT на мові Anders; 3) запис нонаток у TeX як основна культура документування; 5) курсова робота по формалізації певної математичної теорії або порт існуючої формалізації з Agda або Lean; 6) гуртування людей які намагаються поєднати професійну математику та програмування; 7) отримання інтелектуального задоволення.

Підручник HoTT

Що стосується теорії та дидактичних матеріалів, то курс побудований таким чином аби можна було використовувати як текстуальне джерело-компаньон класичний Підручник HoTT Структура курсу теж ділиться на дві великі частини: 1) програмування (або базові синтетичні конструкції теорії типів); та 2) математика (математичні теорії написані на цій мові програмування). На додаток до класчних тем підручника HoTT, цей курс містить початковий вступ у формальну алгебраїчну топологію та диференціальну геометрію.

Кубічні мови

На практиці професійні математики зосереджені навколо двох мов математичного програмування: Agda та Lean. У той час як Agda підтримує кубічні примітиви в ядрі прувера, для Lean існує бібліотека яка інтерналізує кубічні примітиви в примитіви ядра Lean які називаються фактортипами (така система є консистентною проте не завжди має нормальні форми). Усього існує небагато кубічних мов програмування: 1) cubical/cubicaltt (CCHM); 2) RedPRL/redtt/cooltt (ABCFHL). 3) yacctt (ABCFHL); 4) Arend (I-HoTT); 5) Agda (CCHM); 6) Anders (CCHM). Ми покажемо відмінності між ними проте курс зосереджений навколо синтаксису CCHM. Посилання на адаптації нашої бібліотеки Групоїд Інфініті для усіх цих кубічних пруверів, а також посилання на самі прувери та їх математичні моделі наведені на сайті Кубічні Системи

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

Лекція I: Теорія типів

The first section is an introduction to type theory, its subject matter, and the method of computer science. We will show basic principles of lambda calculus, its most powerful version — System $P_\omega$, Calculus of Constructions, and Pure Type Systems. Then we will encode the theorems of MLTT type system in cubical type checkers. This section will cover Pi, Sigma, Equ, W types.

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

Issue I: Internalizing Martin-Löf Type Theory

Issue II: Inductive Types

The second section is an introduction to basic inductive types and induction principle. Inductive types form a basis of so-called Calculus of Inductive Constructions, the theory behind Coq. We will show how proving theorems with induction principle will differ from cubical constructions. Also, we introduce a general Impredicative Encoding of Inductive Types (Awodey). This section will cover: Empty, Unit, Either, Prod, Bool, Maybe, Nat, List, Fix, Mu, Nu, Free, Cofree types.

HoTT 1.7, 1.8, 1.9, 5.1, 5.6

Issue II: Inductive Types and Encodings

Issue III: Homotopy Type Theory

This topic gives a fundamental view of Pi types as Fibrations used in constructive Equivalence. Also here we give an infinite hierarchy of types, containing higher globular equalities used as a base for IPL, Set Theory, and Simplicial Geometry. This section will cover Fiber, n-Groupoid, $\infty$-Groupoid types.

There exist three equalities in Type Theory: 1) built-in into type checker, representing Id, Equ or Path type with J eliminator; 2) Fibration based Equivalence; 3) Isomorphism containing retract and section. This fact leads to Univalence Axiom that states that all equalities are equal and this could be proved in cubical type checkers. This section will cover: Equiv, Iso, Homotopy, Univalence, Injective, Surjective types.

HoTT 2.1, 2.3, 2.4, 2.6, 2.7

Issue III: Homotopy Type Theory

Issue IV: Higher Inductive Types

One of the primary motivation of HoTT is constructive geometry and cell complexes, the spaces constructed by gluing n-discs along their boundaries. In this section, we show how to build topological primitives and how to reason about them. This section will cover: Line, Suspension, n-Sphere, Pushout, Pullback, Truncation, Quotient types.

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

Issue VI: Higher Inductive Types

Issue V: Modalities

This section will cover: Infinitesimal type.

HoTT 7.7

Mathematics

Issue VI: Set Theory

This section is an introduction to Intuitionistic Propositional Logic (IPL), its difference from Classical Logic, Axiom of Choice, Law of Excluding Middle, Propositional Truncation, Hedberg Theorem, Decidable Types, Constructive Set Theory. This section will cover: Prop, Set, Decidable, Stable, Discrete types.

HoTT 3.1, 3.3, 3.11

Issue VII: Category Theory

More than 10 Fields awards are taken with Category Theory (CT) as an instrument. For doing Math, CT is crucial. As a companion to HoTT chapter on CT, we suggest the course of Steve Awodey (the disciple of Saunders Mac Lane), who also made HoTT possible.

This section will give the fundamental notion of following types: Precategory, Rezk Completion, Functor, Natural Transformation, Adjoint, Cone, Structure Identity Principle, Limit, Pullback, Kan Extension, Monomorphism, Epimorphism, Universal Mapping Property.

The primary application of CT in Computer Science is building the categorical model of Dependently Typed Lambda Calculus as an internal language of Locally Cartesian Closed Category. The two models mentioned in this course are Categories with Families (Dybjer) and C-Systems (Voevodsky).

Also as examples of Category instances following types are used: Category of Sets, Category of Functions, Category of Categories, Category of Functors, Slice Category, Product Category. Using those we can construct basic examples of 2-categories, and give a very basic intro to $\infty$-Categories. Types in this section: Category of Commutative Monoids, Category of Abelian Groups, Grothendieck Group.

Issue VIII: Contextual Categories for Martin-Löf Type Theory

Issue VIII: Topos Theory

Topos Theory will give a more in-depth look into categorical models and make a stronger foundation to build a bridge between CT and Logic of Space.

In this section, I will mention Subobject Classifier and Topos types.

Issue IX: Formal Topos on Category of Sets

Issue IX: Algebraic Topology

Types in this section: Monoid, Commutative Monoid, Group, Ring, Abelian Group, Abelian Ring, Hopf, Loop Space, Homotopy Group.

Issue X: Differential Geometry

Types in this section: Abstract Homogeneous Structure, Shape, Étale Map, Automorphism, Fiber Bundle, Manifold, Covering Space (G-Set).

History

Historical Notes

As for the tower of type theories that are necessary for CCHM (Cohen-Coquand-Huber-Mortberg) introduction we will use the following setting.

Type Systems

These historical prerequisites (PTS, MLTT, CiC) and will be given along the way of the course.

Towards EGA/SGA

Cohesive Type Theory is satisfying the needs of modalities, such as connectedness, compactness, infinitesimal shapes, etc. Differential Cohesive Type Theory is the internal language of differential cohesive $(\infty,1)$-topoi, with additional structure, just as $(\infty,1)$-categories add a globular path equality structure to locally cartesian closed categories and its internal language — MLTT. Please refer to cohesivett for more information.

Cohesive types are modeled in the base library as undefined axioms. Process Calculus is another example of modality types with special spawn arrows hiding the underlying run-time implementation.