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.
Announcement: important changes in response to COVID19.
Please review important changes in response to COVID19.
Topic  References  Homework/Survey  Notes/Code/Slides  

Jan  21  Introduction 
HoTT 1 PMLTT 1 
Preclass Survey  Lecture Notes 
23  [Agda] DoubleNegation Translation  Install Agda  Agda Code  
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 Homework 1 Solution Re: Homework 1 
Notes by Mahrud Agda Code 

Feb  4  Types with Dependency  HoTT 1 PMLTT 413 
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 321 
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 
Selfpractice (Solution)  
Mar  3  Inductive Types  HoTT 5  Notes by Calvin & Devon  
5  [Agda] Equational Reasoning  HoTT 5  321  Agda Code Extra Practice for J 

10  No Class (Spring break)  
12  No Class (Spring break)  URGENT: Technology CheckIn  
17  No Class (Spring break) Zoom Test Session 

19  Inductive Types  HoTT 5,6  Homework 3 due Homework 4 Homework 4 Solution 321 
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 
321  Agda Code  
29  MiniLecture: Truncation Levels  Slides  
Apr  1  Composition Structure of Types  Slides  
2  [Agda] Connections and Partial Elements  Homework 4 due Homework 5 Homework 5 Solution 321 
Agda Code Slides 

7  Composition Structure of Various Types  Slides Notes by Nathan & Nori 

9  [Agda] Groupoid Laws  321  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 321 
Agda Code  
22  Normalization  Slides Notes by Bowen & Zhuyang 

23  [Agda] Univalence  321  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) 
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.
(Updated on 3/13 in response to coronavirus.)
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.
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).