Chapter 1 Agda code

The current experimental webpage contains the version of the Chapter 1 agda code from rebuild2/src, last checked on 14 October 2026.

Mathematical scope

One deviation from the book is that we do not assume that isAn is closed under equivalences of categories. This is not needed for anything in Chapter 1 and will become provable after having available the groupoid recognition principle from Chapter 2.

Publication selection

All mathematical Chapter 1 modules are included.

Modules