Direct imports between the 75 literate chapters. Horizontal axis is dependency depth (no dependencies at the left, the root theorem at the right); lanes are the sidebar's namespace tree. A → B means B imports A. Hover for a chapter's dependency cones; click to pin.
Reading order (corner numbers) and dependency order differ on purpose: this page is the third derived view of the two-catalog doctrine (PLAN §5). Regenerated from the import lines of src/**.lagda.md on every site build.