dependent sum


Category theory

Limits and colimits



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:AIf \colon A \to I a morphism in 𝒞\mathcal{C} such that pullbacks along ff exist in 𝒞\mathcal{C}. These then constitute a base change functor

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

between the corresponding slice categories.


The dependent sum or dependent coproduct along the morphism ff is the left adjoint f:𝒞 /A𝒞 /I\sum_f \colon \mathcal{C}_{/A} \to \mathcal{C}_{/I} of the base change functor

( ff *):𝒞 /Af * f𝒞 /I. (\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:AIf \colon A \to I is the functor

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

given by composition with ff.


Relation to the product

Assume that the category 𝒞\mathcal{C} has a terminal object *𝒞* \in \mathcal{C}. Let X𝒞X \in \mathcal{C} be any object and assume that the terminal morphism f:X*f \colon X \to * admits all pullbacks along it.

Notice that a pullback of some A*A \to * along X*X \to * is simply the product X×AX \times A, equipped with its projection morphism X×AXX \times A \to X. But if we regard this as the image of the base change functor f *:𝒞 /*𝒞 /Xf^* \colon \mathcal{C}_{/*} \to \mathcal{C}_{/X} then it is not quite just the product in 𝒞\mathcal{C}. Instead we have:


The product X×A𝒞X \times A \in \mathcal{C} is, if it exists, equivalently the dependent sum of the base change of A*A \to * along X*X \to *:

XX *AX×A𝒞. \sum_{X} X^* A \simeq X \times A \in \mathcal{C} \,.

Here we write “XX” also for the morphism X*X \to *.

Relation to type theory

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 x:X,Px\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 theorycategory theory
natural deductionuniversal construction
dependent sum typedependent sum
type formationX:Typex:XA(x):Type( x:XA(x)):Type\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 introductionx:Xa:A(x)(x,a): x:XA(x)\frac{x \colon X \;\vdash\; a \colon A(x)}{\vdash (x,a) \colon \sum_{x' \colon X} A\left(x'\right) }
term eliminationt:( x:XA(x))p 1(t):Xp 2(t):A(p 1(t))\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 rulep 1(x,a)=xp 2(x,a)=ap_1(x,a) = x\;\;\;\; p_2(x,a) = a


Standard textbook accounts include section A1.5.3 of

and section IV of

Revised on July 12, 2014 08:35:11 by yuning? (