Reading the Agda formalization | Synthetic category theory

The main experimental feature of this site is the interface it provides for inspecting and learning about the AI-generated formalization of the book.

Reading code beside the book

The site offers the option to read the AI-generated Agda code side to side with the (human-written) book.

Clicking a dotted-underlined phrase open an Agda reader on the right-hand side, and highlights the corresponding line in the code. For example, “There are categories” highlights CAT : Set c.
Sometimes, a phrase in the book corresponds to several lines of code, which are then all highlighted. For example, clicking on animae highlights both isAn and the fields of AN. The reader moves to the first highlighted line.
The book and the code can be explored independently. The Module menu can be used to open any available module, grouped per chapter and section.
Clicking a line number or unlinked part of the code highlights that line and moves the book to its corresponding passage. Since the Agda code is a lot more detailed than the natural language proofs in the book, not all Agda code directly corresponds to text in the book; in such cases, one jumps to a related line, where more specific proof steps take precedence over enclosing declarations. When there are alternatives, a Book passage menu appears. Some lines are not assigned a passage in the text.
Click on a word in the code to jump to its definition; the button Back in code can be used to jump back. Click Copy selection to copy the highlighed line. Click Full module, or Ctrl/Command-click a word, to open the corresponding module in a new window. Close the Agda reader with × or Escape.

The highlighting and linking in the source is done by Agda itself. The typechecking is carried out during the build of the webpage. The code snippets displayed on the webpage are extracted from that output via a python script.

Statuses

A selected line in the code displays one of the following statuses:

Assumption, type checked. This is a field of an input record, i.e. something that serves as an assumption. Agda checks that its type is well formed, but it does not derive that field.
Definition, checked. This is a verified definition or construction with the displayed type, built from the parameters and imports the module provides.
Derivation, checked. This is a verified proof of a statement. In agda, statements are implemented as types, so this is actually the same thing as a checked definition.

While Agda has checked all code compiles, this does not construct a model or prove consistency; these are tasked that need to be proved separately. Similarly, the Agda formalization does not say anything about the validity of the underlined environments in arbitrary categorical contexts.

Quick notation guide

Agda	Reading
`CAT`, `MAP C D`	Categories and functors.
`Obj-abs C`	An absolute object, a functor from the terminal anima.
`f ＝ g`	The anima of identifications between functors. The equals sign is Unicode U+FF1D, since Agda reserves plain `=` for definitions.
`f =₁ g`	A natural isomorphism.
`α =₂ β`	An identification between natural isomorphisms.
`p =₃ q`	An identification between such identifications.
`＝-isAn`	The equality category is an anima.
`＝-inv`	The inversion functor on equality animae.
`α ⁻¹`	The inverse of an equality.
`_∙_`, `_◁_`, `_▷_`, `_⋆_`	Vertical composition, postwhiskering, prewhiskering, horizontal composition.
`{A : CAT}`	An implicit parameter category. Its occurrence in a signature remains visible.

All the code

The all-code index contains every source module in the web edition, with a searchable index for modules. Moreover, each full module pages offers a list of all corresponding book passages.

Reading preferences

Selecting Hide links to Agda code displays the plain book text without the underlines and links to Agda code. This preference is remembered across pages. Click Browse Agda modules to open the Agda reader without clicking a prose link.