Favonia: This repository still requires lots of work but I do not have time to maintain it now. In particular, many lecture notes are in unmerged pull requests but they never received enough attention after the course ended. It is possible that I would have to take over those pull requests and finish the revisions when I have time. Until then, this repository is archived.
These are some lecture notes of Higher-Dimensional Type Theory (CSCI 8980) in 2020 Spring, collectively done by the students and Favonia.
notes-0121-introduction: Introduction to Type Theory (2020/01/21, 2020/01/28) by Favonianotes-0204-dependency: Dependent Types (2020/02/04) by Bowen Wang and Zhuyang Wangnotes-0211-identification: Identification Types (2020/02/11) by Nathan Ringo and Norihiro Yamada
Contributors outside the course:
- Jon Sterling (@jonsterling)
The work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License. Some content were adapted from the source of the book Homotopy Type Theory: Univalent Foundations of Mathematics.
It is recommended to install the most recent TeX distributions, such as TeXLive and MiKTeX.
In case you see the following error message, please install the TeX package newtx via your OS or TeX package manager:
kpathsea: Running mktexmf txex-bar
! I can't find file `txex-bar'.