dependent sum

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

$f^* \colon \mathcal{C}_{/I} \to \mathcal{C}_{/A}$

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

$(\sum_f \dashv f^* )
\colon
\mathcal{C}_{/A}
\stackrel{\overset{\sum_f}{\to}}{\underset{f^*}{\leftarrow}}
\mathcal{C}_{/I}
\,.$

This is directly seen to be equivalent to the following.

The **dependent sum** along $f \colon A \to I$ is the functor

$\sum_f \coloneqq f\circ (-) \colon \mathcal{C}_{/A} \to \mathcal{C}_{/I}$

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 *$:

$\sum_{X} X^* A \simeq X \times A \in \mathcal{C}
\,.$

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 .

Notice 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}$ | $\left( \array{ A \\ \downarrow^{\mathrlap{p_1}} \\ X} \; \in \mathcal{C}\right) \Rightarrow \left( A \in \mathcal{C}\right)$ |

term introduction | $\frac{x \colon X \;\vdash\; a \colon A(x)}{\vdash (x,a) \colon \sum_{x' \colon X} A\left(x'\right) }$ | $\array{ Q &\stackrel{a}{\to}& A \\ & {}_{\mathllap{x}}\searrow & \\ && X }$ |

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))}$ | $\array{ Q &\stackrel{(x,a)}{\to}& A \\ & & \downarrow^{\mathrlap{p_1}} \\ && X }$ |

computation rule | $p_1(x,a) = x\;\;\;\; p_2(x,a) = a$ | $\array{ Q &\stackrel{(x,a)}{\to}& A \\ & {}_{\mathllap{x}}\searrow & \downarrow^{\mathrlap{p_1}} \\ && X }$ |

For $\mathcal{C}$ a category with finite limits and $X \in \mathcal{C}$ an object, then dependent sum

$\underset{X}{\sum}: \mathcal{C}_{/X} \longrightarrow \mathcal{C}$

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}$

$\array{
A &\longrightarrow& X^\ast \underset{X}{\sum} A
\\
\downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{X^\ast \underset{X}{\sum} f}}
\\
B &\longrightarrow& X^\ast \underset{X}{\sum} B
}$

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

$\array{
\underset{X}{\sum} A &\stackrel{(A,id)}{\longrightarrow}& X \times \underset{X}{\sum} A
\\
\downarrow^{\mathrlap{\underset{X}{\sum}f}} && \downarrow^{\mathrlap{(id, \underset{X}{\sum} f)}}
\\
\underset{X}{\sum} B &\stackrel{(B,id)}{\longrightarrow}& X \times \underset{X}{\sum} B
}
\,.$

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}$

$\array{
\underset{X}{\sum} X^\ast A &\longrightarrow& A
\\
\downarrow^{\mathrlap{\underset{X}{\sum}X^\ast f}} && \downarrow^{\mathrlap{f}}
\\
\underset{X}{\sum} X^\ast B &\longrightarrow& B
}$

is a pullback.

By Frobenius reciprocity the diagram is equivalent to

$\array{
X\times A & \longrightarrow& A
\\
\downarrow^{\mathrlap{(id,f)}} && \downarrow^{\mathrlap{f}}
\\
X \times B &\longrightarrow& B
}
\,.$

Standard textbook accounts include section A1.5.3 of

and section IV of

Revised on May 9, 2015 01:40:58
by Rob Rix?
(192.0.144.185)