v1.4.17 — Cite the terminology glossary; fix F-algebra citation; fix leaked blockquote markers
01-basics/04-terminology.md — the book’s core glossary, cross-referenced
from many later chapters — had zero citations anywhere. Added
notebook-verified exact section/page citations and a References section
for every lambda-calculus term defined there (bound/free variables,
alpha-conversion, beta-reduction, currying, weak head normal form, the
Church-Rosser theorem — Pierce2002 §5.1–5.3, Thompson1991 §2.3) and every
category-theory term (universal property, initial object, forgetful
functor, subobject, full subcategory — MacLane1998, Pareigis1970).
Lean-specific operational sections (elaboration, unification) intentionally
left uncited, matching this book’s treatment of Python “Programmer’s
corner” boxes elsewhere: they describe Lean’s own behavior, not a claim
from external literature.
Also added the missing [Jacobs1999] citation to the F-algebra
definition itself in the Chapter 1 §1 optional math box, and fixed an
unrelated pre-existing bug found along the way: leaked \textgreater{}
blockquote-continuation artifacts rendering as literal > characters in
one PDF box (isolated to this file, confirmed via book-wide search).