Homotopy Type Theory Reading Group
This is the homepage for the Homotopy type Theory Reading Group in the Spring 2018 semester, where we keep track of the topics discussed and host notes from the Homotopy Type Theory Reading Group in the Spring 2018 semester.
Information
| Meeting Time: | Thursdays 3:00 - 4:15 (flexible end time) |
| Meeting Place: | Malott 206 |
Resources
| Homotopy Type Theory (The Book) | [Link] |
| Intuitionistic Type Theory (Martin-Löf) | [Link] |
| Foundations of Constructive Mathematics (Beeson) | [Link] |
| Categorical Logic and Type Theory (Bart) | [Link] |
| An Introduction to Univalent Foundations for Mathematicians (Grayson) | [Link] |
| Homotopy Type Theory Electronic Seminar (Open to all!) | [Link] |
Schedule
| Date | Topic | Speaker | Reference | |
|---|---|---|---|---|
| 25 January | Organization | |||
| 1 February | Type Theory | Andrew | Notes | |
| 8 February | Homotopy Theory | Brandon | Notes | |
| 15 February | Identity Types | Daoji | Book 1.12, 2.1 | |
| 22 February | Path Lifting, Equivalences | Michael | Book 2.2-2.4 | |
| 1 March | Categorical Fibrations | Andrew | Notes | |
| 8 March | Higher Groupoid Structure | Michael | Book 2.7, 2.10, 2.12 |
Potential Future Topics
| Univalence, Function Extensionality |
| Equivalences |
| Higher Inductive Types |
| Models (like simplicial, cubical,...) |
| Logic, Foundations, Philosophy |
| Topos Theory |