v1.4.22 — Book-wide content-quality pass: clarity fixes, citations, and new diagrams
A large batch of reader-feedback fixes, gathered and shipped as several separate PRs:
Quick surgical fixes (7 issues): the propositional-logic BNF grammar
now uses two distinct metavariables (φ/ψ) instead of reusing φ on
both sides of a connective, with a gloss explaining the convention; Prop
now gets a forward-safe “Sort 0” gloss at its first mention, instead of
being used silently before its formal definition two files later; the
eight “Correction:“-labeled citations across the References sections
are now plain, integrated remarks; extending-structures.md gained a
second single-parent example plus a genuine multi-parent (extends A, B)
example with a field-collision explanation; the motive explanation was
redone with a second worked example (beyond Nat.rec) and a genuine
ill-typed counterexample; more Π-type and Σ-type worked
examples/counterexamples were added; and more worked λ-calculus reduction
examples were added, including one requiring genuine α-conversion.
Prose-style pass (5 files): rewrote dense, jargon-stacked sentences and multi-line parenthetical asides into plain declarative prose in Chapters 1, 2, 6, 8, and 10 — a book-wide sweep confirmed the remaining chapters didn’t have the same density problem, so this pass is complete.
Full section-number citations: replaced every remaining §N shorthand
with the full “Chapter M, Section N” form, including twelve same-chapter
cross-references that had been left as a bare “Section N” — two of which
turned out to cite the wrong section number outright (04-implication.md
is Section 4 of Chapter 3, not Section 3).
New categorical diagrams: added tikz-cd diagrams for Chapter 1’s
F-algebra/initiality box, Chapter 2’s categorical-product universal
property, the multi-parent extends case’s two independent forgetful
projections, and Chapter 10’s M ⊕ N biproduct — each verified to compile
standalone before being wired into the book.
Also fixed: a false claim that “$e$” reappears later in a categorical box, and the bare “→”/”×” naming inconsistency in Chapter 1 §5.
All Lean snippets added or modified were checked directly against the
toolchain pinned in this repository’s lean_project/lean-toolchain
(v4.31.0) rather than only described.