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

Course Materials