Cubical Course

Introduction to Modern Type Theories



This seminar supposed to be a contemporary introduction to modern type theory that is suitable for mathematicians needs, in the sense that this theory forms a foundation of mathematics and the language for theorems formulation and their proofs.


The seminar will focus on 1) direct proof-term construction in cubical type theory with computer-based type checker; 2) solving home assignments in cubical type checker; 3) make people writing cubical code; 4) writing lecture notes by students in LaTeX; 5) making small course project as the final task (could be porting some library or theory from Agda or even formalizing a new part of mathematics); 6) gather smart people together; 7) have fun.

The HoTT Book

While this seminar will try to follow HoTT book as a main source, I will try to give some parts, not present in HoTT, such as algebraic topology or higher category theory. On the other hand I will miss some parts from HoTT. Please treat this course as author's one, but heavily inspired by HoTT book and cubical type checkers.

Cubical Languages

What is cubical type theory and why it is important? The cubical type theory is a theory in which univalence axiom by Voevodsky has computational interpretation. There are several type checkers which use different flavors of cubical type theory while sharing the same concept. Most notable stable implementations are: 1) agda --cubical; 2) cubicaltt; 3) cubicaltt/hcomptrans; 4) yacctt; 5) RedPRL. We will show differences between them and students are free to choose type checker of their favor (for home assignments), but at learning classes (joint hackathon) I will use cubicaltt flavor I most experienced with.



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

2. 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 an 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

3. Fibrations and n-Groupoids

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.

HoTT 2.1, 2.3, 2.4, 2.6, 2.7

4. Prop and Set

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

5. Equiv, Iso and Univ

In Type Theory exists on three equalities: 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.10, 4.6, 4.7

6. 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 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

7. Modalities

This section will cover: Infinitesimal type.

HoTT 7.7


8. Category Theory

More than 10 Field's 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 a building of 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.

9. Topos Theory

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

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

10. Basic Algebra

Types in this section: Monoid, Commutative Monoid, Group, Ring, Abelian Group, Abelian Ring.

11. Ordinals

Types in this section: Ordinal, Mahlo.

12. Differential Topology

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

13. Hopf Fibrations

Types in this section: Hopf.

14. Introduction to K-Theory

Types in this section: Category of Commutative Monoids, Category of Abelian Groups, Grothendieck Group.


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. The history part could be extended by request from the students.

Towards EGA/SGA

Cohesive Type Theory is satisfying the needs of modeling 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 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.