Subcategories
Subcategories generated by collections of morphisms.
Chapters 1 and 2 use the rebuild2 formalization. Agda links for Chapter 3 remain temporarily unavailable.
Chapter 3
Constructions of categories
In this chapter, we introduce various fundamental categorical constructions in the setting of synthetic category theory: subcategories and full subcategories, localizations, geometric realizations, exponentiable functors, joins, and slices.
Sections
Full subcategories
Full subcategories spanned by collections of objects.
Localizations
Inverting morphisms and the localization universal property.
Geometric realizations
Realization, groupoid recognition, and objectwise isomorphisms.
Exponentiable functors
Dependent products, base change, and relative functor categories.
Joins
The two universal properties of joins, their cores, and cones.
Slice categories
Relative slices and functors into absolute slices.
Exercises
Exercises on subcategories, localizations, and dependent products.