Section 1.1
The basic vocabulary
Categories, functors, identifications, and products.
This is an experiment in mathematical exposition. The webpage displays the opening of the book Synthetic category theory by Denis-Charles Cisinski, Bastiaan Cnossen, and Tashi Walde. The webpage also contains an Agda formalization of this part of the book. The reader has the option to display the book and the Agda code side-to-side. Clicking an underlined passage in the text reveals the corresponding Agda code. Clicking a line in the Agda code causes the book to jump to the closest match in the text.
About this experiment
This experimental site is maintained by Bastiaan Cnossen. It has been built using substantial AI assistance, model Codex 6 Astra. My coauthors are aware of the experiment and endorse it, but have not yet been directly involved. I take the sole responsibility for the usage of AI for creating this site, and no inference about my coauthors' opinion on AI should be inferred from this.
All mathematics on this webpage not in the form of Agda code is taken directly from the tex source of our joint book, extracted via a python script. Any error introduced by the conversion is mine. Edits to the book do not automatically result to changes to this webpage unless the python script is rerun, and so this webpage may not always display the up-to-date version of the book.
All Agda code on this webpage is AI generated. Some of the high-level naming conventions were chosen by me, but apart from that all implementation decisions were made by Codex.
Given the experimental nature of this webpage, I wish to mostly keep this webpage under the radar for now. The reason this is a public repository is only because GitHub Pages requires a public repository on a free plan.
Introduction · Overview of the axioms
Chapter 1: The language of synthetic category theory
Section 1.2
Coherences
Composition of identifications, whiskering, unitors, and associativity.
Section 1.3
Equivalences of categories
Equivalence calculus and finite compatibility of products.
Section 1.4
Mapping animae
Evaluation, currying, composition, and their coherence.
Section 1.5
Initial categories and coproducts
Initiality, copairing, and the universal property of coproducts.
Section 1.6
Pullbacks of categories
Pullback cones, fibers, coproduct descent, and embeddings.
Section 1.7
Functor categories
Currying, evaluation, and the relation to mapping animae.
Section 1.8
Pushout squares
The mapping-out criterion and pasting of pushout squares.
Chapter 2: The internal structure of categories
Section 2.1
Morphisms and diagrams
Morphisms, natural transformations, and commutative triangles and squares.
Section 2.2
The Segal axiom
Composition, unit laws, associativity, and interchange.
Section 2.3
The Rezk axiom
Invertible morphisms, identifications, and natural isomorphisms.
Section 2.4
Groupoids
Characterizations of groupoids and their closure properties.
Section 2.5
Recognizing animae
Groupoid recognition, core embeddings, and closure of animae.
Section 2.6
Exercises
Composition in products and the elementary Yoneda criterion.
Chapter 3: Constructions of categories
Section 3.1
Subcategories
Subcategories generated by collections of morphisms.
Section 3.2
Full subcategories
Full subcategories spanned by collections of objects.
Section 3.3
Localizations
Inverting morphisms and the localization universal property.
Section 3.4
Geometric realizations
Realization, groupoid recognition, and objectwise isomorphisms.
Section 3.5
Exponentiable functors
Dependent products, base change, and relative functor categories.
Section 3.6
Joins
The two universal properties of joins, their cores, and cones.
Section 3.7
Slice categories
Relative slices and functors into absolute slices.
Section 3.8
Exercises
Exercises on subcategories, localizations, and dependent products.