Module 5: Universal Constructions I: Limits
Universal constructions are the way category theory specifies objects by what they must do rather than how they are built. This module covers limits — the categorical generalization of intersection, conjunction, and constraint satisfaction. You will find that SQL joins, type unification in a type inference engine, and version control merges are all instances of the same universal construction: the pullback. The key insight is that the universal property guarantees uniqueness up to unique isomorphism — there is no choice, no ambiguity, no hyperparameter.
Learning Objectives
- Define a diagram, a cone over a diagram, and a limit as a terminal cone.
- Compute products, pullbacks, equalizers, and terminal objects as special cases of limits.
- Identify SQL natural joins as pullbacks in the category of sets and functions.
- Identify type unification in a type inference algorithm as a pullback.
- Prove that any two limits of the same diagram are uniquely isomorphic, using the universal property.
- Construct limits explicitly in the categories Set, Graph, and Pos.
Materials
Key Concepts
- Diagram: A functor D: J → C from a small index category J into C; describes the shape of a construction (e.g., a span, a cospan, a parallel pair).
- Cone: A natural transformation from a constant functor Δ_c to a diagram D; a compatible collection of morphisms from a single apex c into all parts of the diagram.
- Limit: A terminal cone — the most general object satisfying all the constraints of the diagram; unique up to unique isomorphism by the universal property.
- Product: The limit of a two-object discrete diagram; generalizes Cartesian product, AND, and product types.
- Pullback: The limit of a cospan A → C ← B; generalizes SQL join, fiber product, type unification, and version control merge.
- Equalizer: The limit of a parallel pair f, g: A ⇉ B; the subobject of A on which f and g agree.
- Terminal Object: The limit of the empty diagram; the unit type, the singleton set, the trivial database.
Central Concepts from Prerequisites
- Modules 2–4: categories, functors, natural transformations, Yoneda
- Databases: SQL joins, relational algebra
- Type theory: unification, the occurs check (helpful)
- Abstract algebra: fiber products, direct products