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.

• Time: Tue/Thu 4-5:15pm Tuesday 4-5:15pm for Office Hours, and Thursday 4-5:15pm for practicing Agda
• Room: Amundson Hall 104 (Zoom)
• Instructor: Favonia
• Office Hour: Wednesday 4-5pm at Keller Hall 6-209 Tuesday 4-5:15pm
• Piazza: https://piazza.com/class/k5ljh7amlse5bg
• Lecture Recordings: YouTube Lecture Channel (Since 3/19)
• Lecture Notes: github:favonia/hdtt2020-notes

References

• [Book] Homotopy Type Theory: Univalent Foundations of Mathematics (HoTT)
• [Book] Programming in Martin-Löf’s Type Theory (PMLTT)
• [Book] Categorical Logic (CatLog)
• [Thesis] Computational Semantics of Cartesian Cubical Type Theory by Carlo Angiuli (Angiuli)
• [Paper] Axioms for Modelling Cubical Type Theory in a Topos (OP)
• [Paper] Syntax and Models of Cartesian Cubical Type Theory (ABCFHL)
• Papers specific to the variant implemented by Cubical Agda
  • [Paper] Cubical Type Theory: a constructive interpretation of the univalence axiom (CCHM)
  • [Paper] On Higher Inductive Types in Cubical Type Theory (CHM)
  • [Notes] A Cubical Type Theory for Higher Inductive Types by Simon Huber (Pre-CHM)
  • [Paper] Cubical Agda: A Dependently Typed ProgrammingLanguage with Univalence and Higher Inductive Types [VMA]
• [Webpage] Agda language reference (Agda)
• [Webpage] A collection of Agda tutorials
• (More to add.)

Tentative Schedule

Please review important changes in response to COVID-19.

Goals

At the end of the semester, you will have learned cubical type theory (updated).

Install Agda

You need the development version of Agda.

Requirements

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

• You should attend all class meetings (or watch the recordings).
• You should register yourself in the Piazza forum.
• You should participate in the note-taking in pairs.
• You should finish the homework assignments and email them to Favonia in two weeks (except Homework 7).
• You should finish the note-taking in one week (before the lectures in the next week).

Grading

Here is how Favonia interprets the letter grades:

• A: You have understood the concepts, possibly making occasional minor mistakes.
• B: You have understood the basics, possibly still struggling with some advanced materials.
• C: You have participated in class but still struggling with the basic concepts.
• F: You have cheated, or you have not shown the minimum efforts.

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