This is a graduate seminar course on the recent development of higherdimensional type theory. Type theory serves as an alternative foundation to set theory, with attention to construction. The study of higherdimensional 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 MartinLö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.
Topic  References  Homework/Survey  Notes/Code  

Jan  21  Introduction 
HoTT 1 PMLTT 1 
Preclass Survey  Lecture Notes 
23  [Agda] DoubleNegation Translation  Install Agda  Code: Double Negation  
28  Principle of Harmony I  HoTT 1 PMLTT 27,912 
Preclass Survey due  Lecture Notes  
30  Principle of Harmony II [Agda] Agda Prebasics 
Agda CatLog 
Homework 1 handout Homework 1 sources 
Notes by Mahrud Code: Agda Prebasics 

Feb  4  Types with Dependency  HoTT 1 PMLTT 413 
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 321 Feedback 
Code  
18  Identification II Equivalence 
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.
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.
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 online 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.
You should negotiate with Favonia beforehand, unless the makeup work policy permits late negotiation.
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 GitHublike CSS (licensed under MIT and modified by favonia).