Synthetic category theory

Volume I · Experimental web edition

Build and coverage

This page provides some details about the build process for this web edition.

Tex-to-html conversion

  1. The mathematical content on this page is taken directly from the corresponding tex-files from the Synthetic category theory book project.
  2. A Python script produces an auxiliary file with marked theorems and inserted HTML anchors to keep track of the Agda links.
  3. The tex is then converted into html via TeX4ht. This uses TeX to expand the macros from the preamble, process environments and counters, and handle the various auxiliar files. TeX4ht then uses this to generate html files.
  4. Another script compiles all TikZ diagrams to SVG images.
  5. A final python script splits the converted material into section pages, adds the sidebar and reading controls, applies the website styling, and connects the passages to Agda's compiler-generated code and definition links.

Agda verification

  1. Agda checks all the Agda code published in this web edition, including all its dependencies, with compiler options --safe (disallow any mechanisms for bypassing verification) and --without-K (no uniqueness of identity proofs).
  2. A script checks that the code displayed on the website is identical to the compiler output.
  3. Several Python scripts run checks; e.g. whether the selected code excerpts and highlighted lines belong to the intended Agda declarations; or whether links from book passages to code, and from code back to book passages, point to existing targets.

Agda can only verify the formal definitions and proofs relative to their stated assumptions. It needs to be checked separately whether the formal statements accurately express the corresponding mathematics in the book. A major purpose of this experimental web edition is to aid in this reviewing process.

Build record

The build summary records the Agda version, the module used to initiate verification, and the number of published modules, declaration mappings, and diagrams. The validation results record the outcome of the automated website checks. These records are updated whenever the site is rebuilt.