Section A.4 of the HoTT book states that the metatheoretic properties of Martin-Löf type theory (such as normalization and canonicity properties) can be proved using “standard techniques from type theory.”

What is the best book to learn about these standard techniques?

  • 1
    $\begingroup$ What have you tried? :P $\endgroup$ Aug 16, 2022 at 0:49
  • 1
    $\begingroup$ You'll probably have more luck here or here. $\endgroup$
    – ShyPerson
    Aug 19, 2022 at 3:09


You must log in to answer this question.