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

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

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

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

This section will cover: Infinitesimal type.

HoTT 7.7

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

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

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

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

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

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.