Version: March 2026

  • p.2: "Given that determining the result of a program is in general undecidable" - insert "the problem of" before "determining"
  • p.4: "vector has length at least one" - insert "of" before "at least one"
  • p.7: "we can now define not only variadic functions but even higher-order functions taking variadic functions as input, such as apply which applies" - maybe add commas: "functions, but"; "apply, which"
  • p.13: "closed vector" - what is it?
  • p.17: "ignoring the rules marked with (ITT), which are present only in intensional type theory" - change "ignoring" to "ignore"
  • p.17: "These questions lead to..." - change "questions" to "topics"
  • /p.21: some rules are referenced not by content ("rules for") but by name ("lambda rule", "variable rule"), but displayed rules are not named/
  • p.22: "their thoughts" - should be "the thoughts"?
  • p.23: "are η-equivalences" - insert "called" after "are"
  • p.23: function "FreeVariables" is referenced but not defined
  • p.24: "“junk” judgments that should not correspond to elements of some Tm(Γ, A)" - change "some" to "any" or rephrase
  • p.25: "η-rule of functions" - change "of" to "for"?
  • p.25: "we will notice ... in the right-hand side of the η-rule of functions, f is in context Γ, x : A, whereas in the premise and left-hand side it is in Γ" - I fail to notice this in the rule as it is given in the text ;)
  • p.27: "arbitrary terms of arbitrary type to occur within types" - change "type" to "types"
  • p.27: "rules of all ... to all depend on one another" - is double-"all" intentional?
  • p.35: "construct a substitution that we will name γ .A, satisfying" - change "that" to "which" and insert a comma before it
  • p.36: "There continue to be a few notational shifts" - this sounds wrong ;)
  • p.67: "These rules quickly become tedious, so we write only their introduction" - change "These" to "The" or "their" to "the"
  • p.78: "is “propositions as some types” too restrictive, or it is genuinely incorrect" - change "it is" to "is it"
  • p.84: "proposition that maps out into only other propositions" - change "into only" to "only into"
  • p.84: "Where are the β and η principles?" - change "principles" to "rules"