Martin-Löf 型別理論 (Martin-Löf Type Theory)
Outline
- The propositions-as-types principle (Curry–Howard correspondence) (1/3 unit)
- Propositional types revisited
- Type families (2/3 unit)
- Predicates as type families
- Dependent product
- Dependent sum
- Computational aspects of MLTT (1/3 unit)
- Judgemental equality and computation rules
- Canonicity
- Equational reasoning (2/3 unit)
- Natural numbers
- Equality types
- Peano axioms
