Martin-Löf Type Theory

• Lecturer: 柯向上 Hsiang-Shang Ko

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

Course Materials

TBA