v1.4.10 — Formally cite and define the remaining type-theory notions
Follow-up to the “judgment” fix: audited the whole book for other
type-theory notions introduced or used without a formal definition and a
citation to a source. Fixed five: definitional/propositional equality and
the universe hierarchy (both already had good definitions/examples, just
no References section — added citations to Pierce, Martin-Löf, Girard,
and TPIL4); the Curry–Howard correspondence (added a citation to Howard’s
1980 paper, newly added to the Bibliography, plus TPIL4); “eliminator”/
“recursor,” used twice with a formal treatment explicitly promised in
Chapter 1 §4 but never delivered (added the promised definition and a
Nat.rec worked example to Chapter 1 §5, cross-linked from Chapter 3 §5’s
Or.elim); and decidability (added a Pierce/TAPL citation).
v1.4.10 — Formally define “judgment” at its first use, with an example
Chapter 1 §1 used the type-theoretic term “judgment” (#check e is the
judgment $e : \tau$) without ever formally defining it — the term-first,
citation-never treatment that had crept in. Added a short formal
definition, cited to Martin-Löf’s Intuitionistic Type Theory, right
before the term’s first use, followed immediately by a worked example
($3 : \mathtt{Nat}$) illustrating what the definition means, plus a
matching Bibliography entry/reference link.