Contents
Context
Category theory
category theory
Concepts
Universal constructions
Theorems
Extensions
Applications
Limits and colimits
limits and colimits
1-Categorical
-
limit and colimit
-
limits and colimits by example
-
commutativity of limits and colimits
-
small limit
-
filtered colimit
-
sifted colimit
-
connected limit, wide pullback
-
preserved limit, reflected limit, created limit
-
product, fiber product, base change, coproduct, pullback, pushout, cobase change, equalizer, coequalizer, join, meet, terminal object, initial object, direct product, direct sum
-
finite limit
-
Kan extension
-
weighted limit
-
end and coend
2-Categorical
(∞,1)-Categorical
Model-categorical
bec
Contents
Idea
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.
Definition
Let be a category and a morphism in such that pullbacks along exist in . These then constitute a base change functor
between the corresponding slice categories.
Definition
The dependent sum or dependent coproduct along the morphism is the left adjoint of the base change functor
This is directly seen to be equivalent to the following.
Definition
The dependent sum along is the functor
given by composition with .
Properties
Relation to the product
Assume that the category has a terminal object . Let be any object and assume that the terminal morphism admits all pullbacks along it.
Notice that a pullback of some along is simply the product , equipped with its projection morphism . We may regard as the image of the base change functor , but this is not quite just the product in , which instead corresponds to the terminal morphisms . But we have:
Proposition
The product is, if it exists, equivalently the dependent sum of the base change of along :
Here we write “” also for the morphism .
Relation to type theory
Under the relation between category theory and type theory the dependent sum 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 .
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 | | |
term introduction | | |
term elimination | | |
computation rule | | |
Relation to some limits
Proposition
For a category with finite limits and an object, then dependent sum
preserves and reflects fiber products.
Proposition
For a category with finite limits and any object, the naturality square of the unit of the -adjunction on any morphism in
is a pullback.
Proof
By prop. it suffices to see that the diagram is a pullback in under , where, by Frobenius reciprocity, it becomes
Proposition
For a category with finite limits and any object, the naturality square of the counit of the -adjunction on any morphism in
is a pullback.
Proof
By Frobenius reciprocity the diagram is equivalent to
In higher category theory
Let be an (∞,1)-category. We still want to define the dependent sum as the functor given by composing with the functor , but the details are more complex.
The codomain fibration is a cocartesian fibration classified by a functor .
Then for any , we can define to be the dependent sum.
Since the morphisms induced by composition are cocartesian morphisms, we see that is indeed given by composition with .
By proposition 6.1.1.1 and the following remarks of Lurie, if has pullbacks, then this is also a cartesian fibration, and is classified by a map . Then is the functor computing pullbacks along , and we have the adjunction .
References
Standard textbook accounts include section A1.5.3 of
and section IV of
Other references: