CSCI 8980 Higher-Dimensional Type Theory

This is a graduate seminar course on the recent development of higher-dimensional type theory. Type theory serves as an alternative foundation to set theory, with attention to construction. The study of higher-dimensional types was motivated by homotopy theory, a branch of mathematics on topological spaces up to continuous deformation, but has become a thing on its own. In this semester, we will start with Martin-Löf (dependent) type theory, introduce extensions such as univalence and higher inductive types, and eventually cubical type theory, a radical rethink about these extensions. We will also use Agda to assist the learning.


Tentative Schedule

Topic References Homework/Survey Notes/Code
Jan 21 Introduction
HoTT 1
Preclass Survey Lecture Notes
23 [Agda] Double-Negation Translation Install Agda Code: Double Negation
28 Principle of Harmony I HoTT 1
PMLTT 2-7,9-12
Preclass Survey due Lecture Notes
30 Principle of Harmony II
[Agda] Agda Pre-basics
Homework 1 handout
Homework 1 sources
Notes by Mahrud
Code: Agda Pre-basics
Feb 4 Types with Dependency HoTT 1
PMLTT 4-13
Lecture Notes
6 [Agda] Natural Numbers and Lists Agda Code: Agda Basics
11 Identification I HoTT 1.12,2 Notes by Nathan & Nori
13 [Agda] Groupoid Laws and Homotopy Levels Agda
HoTT 2
Homework 1 due
Homework 2 handout
Homework 2 sources
3-2-1 Feedback
18 Identification II
HoTT 4 Notes by Mahrud
20 [Agda] Universes and Paths in Various Types Agda
25 Universe & Univalence Notes by Dawn & Jack
27 No Class Homework 2 due
Homework 3 out
Mar 3 Inductive Types Notes by Calvin & Devon
5 [Agda]
10 No Class (Spring break)
12 No Class (Spring break)
17 Inductive Types Notes by Calvin & Devon
19 [Agda] Homework 3 due
Homework 4 out
24 Introduction to Cubical Type Theory Notes by Daniel
26 [Agda] Cubical Features
31 Composition Structure of Types Notes by Favonia
Apr 2 [Agda] Homework 4 due
Homework 5 out
7 Path Structure of Types, reprised Notes by Nathan & Nori
9 [Agda]
14 Univalence, reprised Notes by Dawn & Jack
16 [Agda] Homework 4 due
Homework 5 out
21 Inductive Types Notes by Bowen & Zhuyang
23 [Agda] Inductive Types
28 Normalization
30 [Agda] TBD Homework 5 due
Homework 6 out
May 5 No Class (Study days)
7 No Class (Final exam week)
12 No Class (Final exam week) Homework 6 due (12 days)


At the end of the semester, you will have working knowledge in interactive proof assistants and cubical type theory, and you can start using tools like Agda or conduct research in formal verification and type theory.

Install Agda

You need the development version of Agda.



Here is how Favonia interprets the letter grades:

Each homework assignment and lecture note will be graded accordingly. Your final grade will take into account all of your activities in class, but it will be based on the (unweighted) average of all your available letter grades, provided that you do not cheat or miss any class meeting. The average is determined by the closest letter grade of the GPA of individual letter grades.

To work around the limitations of Canvas, A is converted to 95%, B is converted to 80%, and C is converted to 65%. The conversion table (and the special grading scheme used on Canvas) is to implement the formula described in the previous paragraph. The percentages have no special meaning other than displaying the correct letter grades to you.

Academic Integrity

You are encouraged to discuss homework problems with your fellow students following the whiteboard policy: you may not take notes of what is written during a discussion, and need to erase the whiteboard at the end of the discussion. You need to be able to recreate the results solely from your memory afterwards.

You may also use on-line resources that do not directly contain solutions.

You always need to cite the sources for any ideas you learned from others, including the people you have worked with.

Late Submissions

You should negotiate with Favonia beforehand, unless the make-up work policy permits late negotiation.

Other Important Information

Please check out Recommended Policy Statements for Syllabi for the information about Sexual Harassment, EOAA (Equal Opportunity, and Affirmative Action), Disability, Mental Health and Stress Management. Favonia takes these very seriously. It is highly recommend to read through it and know your rights.

This page was made with GitHub-like CSS (licensed under MIT and modified by favonia).