Cubical Tutorial

Introduction Course



This seminar is 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) helping people write 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) gathering smart people together; 7) having fun.

The HoTT Book

While this seminar will try to follow HoTT book as a main source, I will try to give some theory not present in HoTT, such as algebraic topology or higher category theory. On the other hand, I will skip 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 a cubical type theory and why is it important? The cubical type theory is a theory where 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 the type checker of their flavor (for home assignments), but at learning classes (joint hackathon) I will use cubicaltt flavor I most experienced with.


Issue I: Type Theory

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


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


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.