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.

Announcement: important changes in response to COVID-19.

References

Tentative Schedule

Please review important changes in response to COVID-19.

Topic References Homework/Survey Notes/Code/Slides
Jan 21 Introduction
HoTT 1
PMLTT 1
Preclass Survey Lecture Notes
23 [Agda] Double-Negation Translation Install Agda Agda Code
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
Agda
CatLog
Homework 1
Homework 1 Solution
Re: Homework 1
Notes by Mahrud
Agda Code
Feb 4 Types with Dependency HoTT 1
PMLTT 4-13
Lecture Notes
6 [Agda] Basics Agda Agda Code
11 Identification I HoTT 1.12,2 Lecture Notes
13 [Agda] Groupoid Laws and Homotopy and Truncation Levels Agda
HoTT 2
Homework 1 due
Homework 2
Homework 2 Solution
3-2-1
Agda Code
18 Identification II
Equivalence
HoTT 2.4,2.9,4 Notes by Mahrud
20 [Agda] Paths in Various Types Agda Agda Code
25 Universe & Univalence Lecture Notes
27 [Agda] Paths in Various Types Self Practice Agda
HoTT 7.1 (for Homework 3)
Homework 2 due
Homework 3
Homework 3 Solution
Self-practice (Solution)
Mar 3 Inductive Types HoTT 5 Notes by Calvin & Devon
5 [Agda] Equational Reasoning HoTT 5 3-2-1 Agda Code
Extra Practice for J
10 No Class (Spring break)
12 No Class (Spring break) URGENT: Technology Check-In
17 No Class (Spring break)
Zoom Test Session
19 Inductive Types HoTT 5,6 Homework 3 due
Homework 4
Homework 4 Solution
3-2-1
Temporary Slides and Temporary Code
Notes by Calvin & Devon
24 Introduction to Cubical Type Theory (Part I) Slides
Notes by Daniel
26 [Agda] Cubes and Paths in Sigma Types Agda: Library Management
GitHub: agda/cubical
3-2-1 Agda Code
29 Mini-Lecture: Truncation Levels Slides
Apr 1 Composition Structure of Types Slides
2 [Agda] Connections and Partial Elements Homework 4 due
Homework 5
Homework 5 Solution
3-2-1
Agda Code
Slides
7 Composition Structure of Various Types Slides
Notes by Nathan & Nori
9 [Agda] Groupoid Laws 3-2-1 Agda Code
Slides
14 Universe & Univalence, reprised Slides
Notes by Dawn & Jack
16 [Agda] Transport and Heterogeneous Composition Homework 5 due
Homework 6
Homework 6 Solution
3-2-1
Agda Code
22 Normalization Slides
Notes by Bowen & Zhuyang
23 [Agda] Univalence 3-2-1 Agda Code
30 [Agda] Homework 6 due
Homework 7
Homework 7 Solution
Agda Code
May 2 More on Higher Inductive Types Slides
4 Categorical Aspects of Type Theory Slides
12 No Class (Final exam week) Homework 7 due (12 days)

Goals

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.

Requirements

(Updated on 3/13 in response to coronavirus.)

Grading

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