Dependent products and dependent sums

Let A be a type and let B assign a type to each element of A. A dependent product contains functions that return an element of B at every input. Its application rule substitutes the actual input into the result type. When B is constant this reduces to an ordinary function type. When B describes vectors of a specified length, a dependent function can return a vector whose length is determined by the requested index rather than hidden in an unchecked convention.

A dependent sum contains pairs whose first component is an index a and whose second component belongs to B of that very index. Its first projection has type A, but its second projection has a type involving the first projection. This is why a purported second component cannot be checked before its index is known. A certified integer can similarly store an integer together with evidence of a predicate about it. Ordinary Cartesian products are the constant-family special case.

For a finite index type with explicitly enumerated finite fibers, the dependent sum counts disjoint tagged possibilities, so its size is the sum of the fiber sizes. A dependent product chooses one output in each fiber, so its size is their product. These formulas count actual finite data and can be justified by constructing the corresponding lists or tables. Functions are identified extensionally by their output tables; the internal type-theoretic counting interpretation therefore uses function extensionality. This is an explicit assumption for the counts, not an infinite choice principle.

An empty fiber makes the distinction particularly sharp. The sum may still contain pairs from other fibers, but a section of the entire family cannot exist because it would have to return an element of the empty fiber. Conversely, a product over an empty index type contains the empty function, while its sum is empty. These edge cases follow from the introduction and elimination rules and are useful checks against an informal slogan that dependent sums and products merely mean some or all.

Suppose h supplies, for every a, a dependent pair consisting of some b and evidence of a relation between a and b. Define a choice function by projecting the first component of h at a; project the second component to certify that this function satisfies the relation. This construction is sometimes called the type-theoretic axiom of choice, but in this untruncated form it is a theorem directly obtained from projections and abstraction.

It does not say that a mere statement that every fiber is inhabited provides such a table of witnesses. Propositional truncation can erase the selected elements, and moving from separately truncated existence to a simultaneous choice function is a different principle. We will give its elimination restrictions explicitly in a later lesson. The distinction prevents a common mistake: importing classical choice into a constructive argument while claiming it followed from the elementary dependent-pair projection program.