![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[ ]](/icons/layout.gif){kind=icon}
| Name | Last modified | Size | Description |
|---|---|---|---|---|
| Parent Directory | - | ||
| L01 - Overview and Syntax of ULC.pdf | 2022-06-30 03:19 | 7.9M | |
| L02 (Additional exercises).pdf | 2022-02-23 15:14 | 142K | |
| L02 - Syntax and Environmental models of ULC.pdf | 2022-06-30 03:20 | 7.7M | |
| L03 - Syntax-free models of ULC.pdf | 2022-06-30 03:21 | 6.7M | |
| L04 - Categorical semantics of ULC I.pdf | 2022-06-30 03:21 | 7.7M | |
| L05 - Algebraic type theory (by Nathanel Arkor).pdf | 2022-03-18 01:25 | 3.9M | |
| L06 - Categorical semantics of ULC II.pdf | 2022-06-30 03:22 | 8.5M | |
| L07 - Categorical semantics of ULC III and STLC.pdf | 2022-06-30 03:22 | 7.2M | |
| L08 - STLC II.pdf | 2022-06-30 03:23 | 6.2M | |
| L09 - STLC III and Syntax of MLTT I.pdf | 2022-06-30 03:23 | 7.5M | |
| L10 - Syntax of MLTT II.pdf | 2022-06-30 03:24 | 6.7M | |
| L11 - Syntax of MLTT III.pdf | 2022-06-30 03:24 | 6.5M | |
| L12 - Categorical Semantics of MLTT.pdf | 2022-06-30 03:24 | 8.5M | |
| L13 - Categories with Universes.pdf | 2022-06-30 03:25 | 6.5M | |
| L14 - Examples of Categories with Universes and the UIP.pdf | 2022-06-30 03:25 | 8.2M | |