Skip to the content.

← Changelog index


v1.4.21 — Add a Π vs Σ comparison table

Chapter 1 §5 discussed Π-types and Σ-types at length in separate sections but never gathered their notation, readings, and special cases into one side-by-side comparison. Added a recap table right after both constructs are introduced (notation, what each generalizes, categorical reading, Lean surface syntax, the / logic special case, the witness-extraction asymmetry between Sigma and Exists, and each construct’s first worked example earlier in the section).

Caught and fixed a table-rendering bug while writing it: an empty first header cell broke Pandoc’s Markdown-to-LaTeX table conversion (the header row lost its \toprule/content structure entirely). Giving the column a real header (“Aspect”) fixed it — verified with a full PDF rebuild.

Try Lean
Lean playground · v1.4.18