Skip to the content.

← Changelog index


v1.4.18 — Add Recall subsections across the whole book (23 entries)

Every section with a References block (23 in total) now opens with a Recall subsection: the formal, citation-backed definition(s) that section uses, given as a verbatim quote followed by a short plain-English gloss, so a reader skimming back to check a term gets the precise definition immediately rather than a re-explanation. Inline citation markers were removed from body prose and “Mathematical reading” boxes throughout those files, since the formal citation now lives in Recall; References sections were trimmed to concise pointers.

Two mischaracterizations were caught and fixed while pulling verbatim quotes from source for this pass:

Also fixed two explicitness gaps: Mac Lane’s “initial in C” and Jacobs’s “T : B → B” quotes now state explicitly that C/B are categories, rather than leaving that implicit.

Try Lean
Lean playground · v1.4.18