The dependent sum is a universal construction in category theory. It generalizes the Cartesian product to the situation where one factor may depend on the other. It is the left adjoint to the base change functor between slice categories.
The dual notion is that of dependent product.
Let $\mathcal{C}$ be a category and $f \colon A \to I$ a morphism in $\mathcal{C}$ such that pullbacks along $f$ exist in $\mathcal{C}$. These then constitute a base change functor
between the corresponding slice categories.
The dependent sum or dependent coproduct along the morphism $f$ is the left adjoint $\sum_f \colon \mathcal{C}_{/A} \to \mathcal{C}_{/I}$ of the base change functor
This is directly seen to be equivalent to the following.
The dependent sum along $f \colon A \to I$ is the functor
given by composition with $f$.
Assume that the category $\mathcal{C}$ has a terminal object $* \in \mathcal{C}$. Let $X \in \mathcal{C}$ be any object and assume that the terminal morphism $f \colon X \to *$ admits all pullbacks along it.
Notice that a pullback of some $A \to *$ along $X \to *$ is simply the product $X \times A$, equipped with its projection morphism $X \times A \to X$. We may regard $X \times A \to X$ as the image of the base change functor $f^* \colon \mathcal{C}_{/*} \to \mathcal{C}_{/X}$, but this is not quite just the product in $\mathcal{C}$, which instead corresponds to the terminal morphisms $X \times A \to *$. But we have:
The product $X \times A \in \mathcal{C}$ is, if it exists, equivalently the dependent sum of the base change of $A \to *$ along $X \to *$:
Here we write “$X$” also for the morphism $X \to *$.
Under the relation between category theory and type theory the dependent is the categorical semantics of dependent sum types .
Notce that under the identification of propositions as types, dependent sum types (or rather their bracket types) correspond to existential quantification $\exists x\colon X, P x$.
The following table shows how the natural deduction rules for dependent sum types correspond to their categorical semantics given by the dependent sum universal construction.
type theory | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
dependent sum type | dependent sum | |
type formation | $\frac{\vdash\: X \colon Type \;\;\;\;\; x \colon X \;\vdash\; A(x)\colon Type}{\vdash \; \left(\sum_{x \colon X} A\left(x\right)\right) \colon Type}$ | |
term introduction | $\frac{x \colon X \;\vdash\; a \colon A(x)}{\vdash (x,a) \colon \sum_{x' \colon X} A\left(x'\right) }$ | |
term elimination | $\frac{\vdash\; t \colon \left(\sum_{x \colon X} A\left(x\right)\right)}{\vdash\; p_1(t) \colon X\;\;\;\;\; \vdash\; p_2(t) \colon A(p_1(t))}$ | |
computation rule | $p_1(x,a) = x\;\;\;\; p_2(x,a) = a$ |
For $\mathcal{C}$ a category with finite limits and $X \in \mathcal{C}$ an object, then dependent sum
By this proposition limits over a cospan diagram in the slice category are computed as limits over the cocone diagram under the cospan in the base category. By this proposition this inclusion is a final functor, hence preserves limits. Since the dependent sum of the diagram is the restriction along this final functor, the result follows.
For $\mathcal{C}$ a category with finite limits and $X\in \mathcal{C}$ any object, the naturality square of the unit of the $(\underset{X}{\sum} \dashv X^\ast)$-adjunction on any morphism $(f \colon A \to B)$ in $\mathcal{C}_{/X}$
is a pullback.
By prop. 2 it suffices to see that the diagram is a pullback in $\mathcal{C}$ under $\underset{X}{\sum}$, where, by Frobenius reciprocity, it becomes
For $\mathcal{C}$ a category with finite limits and $X\in \mathcal{C}$ any object, the naturality square of the counit of the $(\underset{X}{\sum} \dashv X^\ast)$-adjunction on any morphism $(f \colon A \to B)$ in $\mathcal{C}$
is a pullback.
By Frobenius reciprocity the diagram is equivalent to
dependent sum, dependent product
Standard textbook accounts include section A1.5.3 of
and section IV of