nLab dependent sum type

Dependent sum types


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Dependent sum types


In dependent type theory, what is traditionally called the dependent sum type (really: dependent coproduct) of a dependent type d:DC d:Typed \,\colon\, D \;\;\vdash\;\; C_d \,\colon\, Type is the type whose terms are ordered pairs (d,c)(d,c) with d:Dd \,\colon\, D and c:C dc \,\colon\, C_d — whence also called the dependent pair type.

In the categorical semantics of dependent type theory in fibration categories, the dependent sum corresponds to internal coproducts over an index type.

In the special case that C d=CC_d \,=\, C is independent of AA this reduces to the product type D×CD \times C, while in the special case that D=D = Bool it reduces to a binary coproduct.

This notion is dual (in fact: adjoint) to the corresponding notion of dependent product type:

type former:meaning of terms:
dependent productdependent function
/ section of bundle
dependent coproduct
(aka: dependent sum)
dependent pair /
element of bundle


The inference rules for dependent pair types (aka “dependent sum types” or “Σ\Sigma-types”):


Like any type constructor in type theory, the dependent sum type is specified by rules saying when we can introduce it as a type, how to construct terms of that type, how to use or “eliminate” terms of that type, and how to compute when we combine the constructors with the eliminators.

In natural deduction

We assume that our dependent sum types have typal conversion rules, as those are the most general of the conversion rules. Both the propositional and judgmental conversion rules imply the typal conversion rules by the structural rules for propositional and judgmental equality respectively.

The formation and introduction rules are the same for both the positive and negative dependent sum types

Formation rules for dependent sum types:

ΓAtypeΓ,x:ABtypeΓ x:AB(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}

Introduction rules for dependent sum types:

ΓAtypeΓ,x:ABtypeΓ,x:A,y:Bin(x,y): x:AB(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \mathrm{in}(x, y):\sum_{x:A} B(x)}

As a positive type

  • Elimination rules for dependent sum types:
ΓAtypeΓ,x:ABtypeΓ,z: x:AB(x)CtypeΓ,x:A,y:Bc:C[in(x,y)/z]Γ,z: x:AB(x)ind x:AB(x) C(c):C\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z]}{\Gamma, z:\sum_{x:A} B(x) \vdash \mathrm{ind}_{\sum_{x:A} B(x)}^C(c):C}
  • Computation rules for dependent sum types:
ΓAtypeΓ,x:ABtypeΓ,z: x:AB(x)CtypeΓ,x:A,y:Bc:C[in(x,y)/z]Γ,x:A,y:Bβ x:AB(x) C(c):ind x:AB(x) C(c)[in(x,y)/z]= C[in(x,y)/z]c\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z]}{\Gamma, x:A, y:B \vdash \beta_{\sum_{x:A} B(x)}^C(c):\mathrm{ind}_{\sum_{x:A} B(x)}^C(c)[\mathrm{in}(x, y)/z] =_{C[\mathrm{in}(x, y)/z]} c}
  • Uniqueness rules for dependent sum types:
ΓAtypeΓ,x:ABtypeΓ,z: x:AB(x)CtypeΓ,x:A,y:Bc:C[in(x,y)/z]Γ,z: x:AB(x)u:CΓ,x:A,y:Bi in(u):u[in(x,y)/z]= C[in(x,y)/z]cΓ,z: x:AB(x)η x:AB(x) C(c):u= Cind x:AB(x) C(c)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z] \quad \Gamma, z:\sum_{x:A} B(x) \vdash u:C \quad \Gamma, x:A, y:B \vdash i_\mathrm{in}(u):u[\mathrm{in}(x, y)/z] =_{C[\mathrm{in}(x, y)/z]} c}{\Gamma, z:\sum_{x:A} B(x) \vdash \eta_{\sum_{x:A} B(x)}^C(c):u =_{C} \mathrm{ind}_{\sum_{x:A} B(x)}^C(c)}

Given a pointed h-proposition (A,a)(A, a), the positive dependent sum type results in in(a,)\mathrm{in}(a,-) being an equivalence of types.

As a negative type

  • Elimination rules for dependent sum types:
ΓAtypeΓ,x:ABtypeΓ,z: x:AB(x)π 1(z):AΓAtypeΓ,x:ABtypeΓ,z: x:AB(x)π 2(z):B[π 1(z)/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, z:\sum_{x:A} B(x) \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, z:\sum_{x:A} B(x) \vdash \pi_2(z):B[\pi_1(z)/x]}
  • Computation rules for dependent sum types:
ΓAtypeΓ,x:ABtypeΓ,x:A,y:Bβ Σ1(x,y):π 1(in(x,y))= AxΓAtypeΓ,x:ABtypeΓ,x:A,y:Bβ Σ2(x,y):π 2(in(x,y))= B[π 1(in(x,y))/x]y\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{\Sigma 1}(x, y):\pi_1(\mathrm{in}(x, y)) =_A x} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{\Sigma 2}(x, y):\pi_2(\mathrm{in}(x, y)) =_{B[\pi_1(\mathrm{in}(x, y))/x]} y}
  • Uniqueness rules for dependent sum types:
ΓAtypeΓ,x:ABtypeΓ,z: x:AB(x)η Σ(z):z= x:AB(x)in(π 1(z),π 2(z))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, z:\sum_{x:A} B(x) \vdash \eta_{\Sigma}(z):z =_{\sum_{x:A} B(x)} \mathrm{in}(\pi_1(z), \pi_2(z))}

Given a pointed h-proposition (A,a)(A, a), the negative dependent sum type results in π 2(a,)\pi_2(a,-) being a quasi-inverse function of in(a,)\mathrm{in}(a,-), rather than an equivalence of types. Thus, the positive definition is preferred to the negative definition. Alternatively, the negative dependent sum type should be defined as a coinductive type rather than an inductive type.

Extensionality principle

The extensionality principle for the dependent sum type states that there is an equivalence of types between the identity type (a,b)= x:AB(x)(a,b)(a, b) =_{\sum_{x:A} B(x)} (a', b') of a dependent sum type and the dependent sum p:a= Aab= B pb\sum_{p:a =_A a'} b =_B^p b' of its component’s identity types:

ΓAtypeΓ,x:AB(x)typeΓa:AΓb:B(a)Γa:AΓb:B(a)Γext Σ(a,b,a,b):(a,b)= x:AB(x)(a,b) p:a= Aab= B pb \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a) \quad \Gamma \vdash a':A \quad \Gamma \vdash b':B(a')}{\Gamma \vdash \mathrm{ext}_{\Sigma}(a, b, a', b'):(a, b) =_{\sum_{x:A} B(x)} (a', b') \simeq \sum_{p:a =_A a'} b =_B^p b'}

The comparison function itself is readily obtained by Id-induction. That this indeed constitutes an equivalence of types is shown in UFP13, Thm. 2.7.2.

In the notation of dependent pairs (here) this reads:

Compare to the analogous extensionality principle for dependent functions (see at function extensionality, here):

(In this dependent generality this is a special case of UFP13, Lem. 2.9.7.)

In lambda-calculus

The presentation of dependent sum type is almost exactly the same as that of product types, with the simple change that BB may depend on AA. In particular, they can be presented both as a negative type or as a positive type. In both cases, the rule for building the dependent sum type is the same:

A:Typex:AB(x):Type x:AB(x):Type \frac{A\colon Type \qquad x\colon A\vdash B(x)\colon Type}{\sum_{x\colon A} B(x)\colon Type}

but the constructors and eliminators may be different.

As a negative type

When presented negatively, primacy is given to the eliminators. We specify that there are two ways to eliminate a term of type x:AB(x)\sum_{x\colon A} B(x): by projecting out the first component, or by projecting out the second.

p: x:AB(x)π 1p:Ap: x:AB(x)π 2p:B(π 1p) \frac{p \colon \sum_{x\colon A} B(x)}{\pi_1 p\colon A} \qquad \frac{p\colon \sum_{x\colon A} B(x)}{\pi_2 p\colon B(\pi_1 p)}

This then determines the form of the constructors: in order to construct a term of type x:AB(x)\sum_{x\colon A} B(x), we have to specify what value that term should yield when all the eliminators are applied to it. In other words, we have to specify a pair of elements, one a:Aa\colon A (to be the value of π 1p\pi_1 p) and one b:B(a)b\colon B(a) (to be the value of π 2p\pi_2 p).

a:Ab:B(a)(a,b): x:AB(x) \frac{a\colon A \qquad b\colon B(a)}{(a,b)\colon \sum_{x\colon A} B(x)}

Finally, we have computation rules which say that the relationship between the constructors and the eliminators is as we hoped. We always have beta reduction rules

π 1(a,b) βaπ 2(a,b) βb \pi_1(a,b) \to_\beta a \qquad \pi_2(a,b) \to_\beta b

and we may or may not choose to have an eta reduction rule

(π 1p,π 2p) ηp (\pi_1 p, \pi_2 p) \to_\eta p

As a positive type

When presented positively, primacy is given to the constructors. We specify that the way to construct something of type x:AB(x)\sum_{x\colon A} B(x) is to give a term a:Aa\colon A and a term b:B(a)b\colon B(a):

a:Ab:B(a)(a,b): x:AB(x) \frac{a\colon A \qquad b\colon B(a)}{(a,b)\colon \sum_{x\colon A} B(x)}

Of course, this is the same as the constructor obtained from the negative presentation. However, the eliminator is different. Now, in order to say how to use something of type x:AB(x)\sum_{x\colon A} B(x), we have to specify how we should behave for all possible ways that it could have been constructed. In other words, we have to say, assuming that pp were of the form (a,b)(a,b), what we want to do. Thus we end up with the following rule:

z: x:AB(x)C(z):Typep: x:AB(x)x:A,y:B(x)c:C((x,y))let(x,y)=pinc:C(p) \frac{z\colon \sum_{x\colon A} B(x) \vdash C(z)\colon Type\qquad p\colon \sum_{x\colon A} B(x) \qquad x\colon A, y\colon B(x) \vdash c\colon C((x,y))}{let (x,y) = p in c \;\colon C(p)}

We need a term cc in the context of two variables of types AA and BB, and the destructor or match “binds those variables” to the two components of pp. Note that the “ordered pair” (x,y)(x,y) in the destructor is just a part of the syntax; it is not an instance of the constructor ordered pair.

Now we have the beta reduction rule:

let(x,y)=(a,b)inc βc[a/x,b/y] let (x,y) = (a,b) \,in c \;\to_\beta\; c[a/x, b/y]

In other words, if we build an ordered pair and then break it apart, what we get is just the things we put into it. (The notation c[a/x,b/y]c[a/x, b/y] means to substitute aa for xx and bb for yy in the term cc).

And (if we wish) the eta reduction rule, which is a little more subtle:

let(x,y)=pinc[(x,y)/z] ηc[p/z] let (x,y) = p in c[(x,y)/z] \;\to_\eta\; c[p/z]

This says that if we break something of type x:AB(x) \sum_{x\colon A} B(x) into its components, but then we only use those two components by way of putting them back together into an ordered pair, then we might as well just not have broken it down in the first place.

Positively defined dependent sum types are naturally expressed as inductive types. For instance, in Coq syntax we have

Inductive sig (A:Type) (B:A->Type) : Type :=
| exist : forall (x:A), B x -> sig A B.

(Coq then implements beta-reduction, but not eta-reduction. However, eta-equivalence is provable with the internally defined identity type, using the dependent eliminator mentioned above.)

Arguably, negatively defined products should be naturally expressed as coinductive types, but this is not exactly the case for the presentation of coinductive types used in Coq.

Positive versus negative

In ordinary “nonlinear” type theory, the positive and negative dependent sum types are equivalent, just as in the case of product types. They manifestly have the same constructor, while we can define the eliminators in terms of each other as follows:

π 1p let(x,y)=pinx π 2p let(x,y)=piny let(x,y)=pinc c[π 1p/x,π 2p/y] \begin{aligned} \pi_1 p &\;\coloneqq\; let (x,y) = p \,in\, x\\ \pi_2 p &\;\coloneqq\; let (x,y) = p \,in\, y\\ let (x,y) = p in c &\;\coloneqq\; c[\pi_1 p / x, \pi_2 p / y] \end{aligned}

The computation rules then also correspond, just as for product types.

Also just as for product types, in order to recover the important dependent eliminator for the positive product type from the eliminators for the negative product type, we need the latter to satisfy the η\eta-conversion rule so as to make the above definition well-typed. By inserting a transport, we can make do with a propositional η\eta-conversion, which is also provable from the dependent eliminator.

One might expect that in “dependent linear type theory” the positive and negative dependent sums would become different. However, the meaning of the quoted phrase is unclear.

Using universes and dependent product types

Dependent sum types could be defined directly from universes, dependent product types, and function types - the last of which are definable from dependent product types. Given a type universe UU, the dependent sum type of the type family x:AB(x)x:A \vdash B(x) is defined as the dependent product type

x:AB(x) P:U x:A(B(x)P)P\sum_{x:A} B(x) \coloneqq \prod_{P:U} \prod_{x:A} (B(x) \to P) \to P

This was the first definition of dependent sum types in dependent type theory, appearing in Per Martin-Löf‘s original 1971 paper on dependent type theory.


Descent and large elimination

The descent for the positive dependent sum type Σx:A.B(x)\Sigma x:A.B(x) states that given any type family x:A,y:B(x)C(x,y)x:A, y:B(x) \vdash C(x, y) one can construct a type family z:Σx:A.B(x)descFam Σx:A.B(x) C(z)z:\Sigma x:A.B(x) \vdash \mathrm{descFam}_{\Sigma x:A.B(x)}^{C}(z) with families of equivalences of types

x:A,y:B(x)descEquiv Σx:A.B(x) C:descFam Σx:A.B(x) C(in(x,y))C(x,y)x:A, y:B(x) \vdash \mathrm{descEquiv}_{\Sigma x:A.B(x)}^C:\mathrm{descFam}_{\Sigma x:A.B(x)}^{C}(\mathrm{in}(x, y)) \simeq C(x, y)

Large elimination for positive dependent sum types strengthens the equivalences of types in descent to judgmental equality of types

x:A,y:B(x)descFam Σx:A.B(x) C(in(x,y))C(x,y)typex:A, y:B(x) \vdash \mathrm{descFam}_{\Sigma x:A.B(x)}^{C}(\mathrm{in}(x, y)) \equiv C(x, y) \; \mathrm{type}

Typal congruence rules

These are called typal congruence rules because they are the analogue of the judgmental congruence rules which use identity types and equivalence types instead of judgmental equality:


Given types AA and AA' and type families x:AB(x)x:A \vdash B(x) and x:AB(x)x:A \vdash B'(x) and equivalences e A:AAe_A:A \simeq A' and dependent function of equivalences e B: x:AB(x)B(e A(x))e_B:\prod_{x:A} B(x) \simeq B'(e_A(x)), there is an equivalence

congform Σ(e A,e B):( x:AB(x))( x:AB(x))\mathrm{congform}_\Sigma(e_A, e_B):\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A} B(x)\right)


This is theorem 11.1.6 of Rijke 2022, and a proof of this is given in that reference.

The typal congruence rules for dependent sum types are very important for proving various other theorems in dependent type theory. For example,


Given a univalent Tarski universe (U,T)(U, T) and a UU-small type A:UA:U, the dependent sum type B:UT(B)T(A)\sum_{B:U} T(B) \simeq T(A) is contractible.


By univalence, for all A:UA:U and B:UB:U, transport across the universal type family TT is an equivalence of types

ua(A,B):isEquiv(transport x:U.T(x)(A,B))\mathrm{ua}(A, B):\mathrm{isEquiv}(\mathrm{transport}_{x:U.T(x)}(A, B))

and thus we have the equivalence

pair(transport x:U.T(x)(A,B),ua(A,B)):(A= UB)(T(B)T(A))\mathrm{pair}(\mathrm{transport}_{x:U.T(x)}(A, B), \mathrm{ua}(A, B)):(A =_U B) \simeq (T(B) \simeq T(A))

and thus by the typal congruence rule of dependent sum types, we have

congform Σ(id U,λB:U.pair(transport x:U.T(x)(A,B),ua(A,B))):( B:U(A= UB))( B:U(T(B)T(A)))\mathrm{congform}_\Sigma(\mathrm{id}_U, \lambda B:U.\mathrm{pair}(\mathrm{transport}_{x:U.T(x)}(A, B), \mathrm{ua}(A, B))):\left(\sum_{B:U} (A =_U B)\right) \simeq \left(\sum_{B:U} (T(B) \simeq T(A))\right)

Since the type B:U(A= UB)\sum_{B:U} (A =_U B) is contractible for all A:UA:U, the above equivalence implies that B:U(T(B)T(A))\sum_{B:U} (T(B) \simeq T(A)) is also contractible.

Quantification in dependent type theory

Given a family of types x:AB(x)x:A \vdash B(x), the existential quantifier is defined as the bracket type of the dependent sum type

x:A.B(x)[ x:AB(x)]\exists x:A.B(x) \coloneqq \left[\sum_{x:A} B(x)\right]

The uniqueness quantifier is defined as the isContr modality of the dependent sum type

!x:A.B(x)isContr( x:AB(x))\exists! x:A.B(x) \coloneqq \mathrm{isContr}\left(\sum_{x:A} B(x)\right)

There is also a quantifier which states that BB holds for at most one element x:Ax:A, defined by the isProp modality of the dependent sum type:

isProp( x:AB(x))\mathrm{isProp}\left(\sum_{x:A} B(x)\right)

In each of the last two cases, one could prove that each dependent type B(x)B(x) has to be a mere proposition.

Given a natural number n:n:\mathbb{N} and given a family of types x:AB(x)x:A \vdash B(x), we can similarly write down quantifiers to say that

  • BB holds for exactly nn elements:
    [( x:A[B(x)])Fin(n)]\left[\left(\sum_{x:A} \left[B(x)\right]\right) \simeq \mathrm{Fin}(n)\right]
  • BB holds for at most nn elements:
    [( x:A[B(x)])Fin(n)]\left[\left(\sum_{x:A} \left[B(x)\right]\right) \hookrightarrow \mathrm{Fin}(n)\right]
  • BB holds for at least nn elements:
    [Fin(n)( x:A[B(x)])]\left[\mathrm{Fin}(n) \hookrightarrow \left(\sum_{x:A} \left[B(x)\right]\right)\right]

    where ABA \simeq B is the equivalence type between AA and BB, ABA \hookrightarrow B is the type of embeddings between AA and BB, and Fin(n)\mathrm{Fin}(n) is the finite set with nn elements.

Categorical interpretation

Under categorical semantics, a dependent type x:AB(x):Typex\colon A \vdash B(x)\colon Type corresponds to a fibration or display map BAB\to A. In this case, the dependent sum is just the object BB. This requires the dependent sum type to satisfy both β\beta- and η\eta-conversion.

There is also another interpretation in category theory of the dependent sum type over x:AB(x)typex:A \vdash B(x) \; \mathrm{type} as the initial AA-indexed wide cospan over B(x)B(x), the object x:AB(x)\sum_{x:A} B(x) with a family of morphisms

in A(x):B(x) x:AB(x)\mathrm{in}_A(x):B(x) \to \sum_{x:A} B(x)

such that for any other object CC with a family of morphisms f(x):B(x)Cf(x):B(x) \to C, there exists a unique morphism u C: x:AB(x)Cu_C:\sum_{x:A} B(x) \to C such that

u Cin A(x)=f(x)u_C \circ \mathrm{in}_A(x) = f(x)

This corresponds to the positive dependent sum types.


A textbook account could be found in section 4.6 of:

Discussion in a context of homotopy type theory:

For the definition of dependent sum types in terms of universes, dependent product types, and function types, see:

See also most references at dependent type theory.

Last revised on May 17, 2024 at 14:43:19. See the history of this page for a list of all contributions to it.