A.2.5 Dependent pair types ($Sigma$-types)

In §1.6 (http://planetmath.org/16dependentpairtypes), we needed $\to$ and $\textstyle\prod$ types in order to define the introduction and elimination rules for $\textstyle\sum$; as with $\textstyle\prod$, contexts allow us to state the rules for $\textstyle\sum$ independently: {mathparpagebreakable} \inferrule*[right=$\Sigma$-form] Γ ⊢A : $\mathcal{U}$ _i Γ,x : A ⊢B : $\mathcal{U}$ _iΓ ⊢∑_(x:A)B : $\mathcal{U}$ _i \inferrule*[right=$\Sigma$-intro] Γ, x : A ⊢B : $\mathcal{U}$ _i
Γ ⊢a : A
Γ ⊢b : B[a/x] Γ ⊢(a,b) : ∑_(x:A)B \inferrule*[right=$\Sigma$-elim] Γ, z : ∑_(x:A)B ⊢C : $\mathcal{U}$ _i
Γ,x : A,y : B ⊢g : C[(x,y)/z]
Γ ⊢p : ∑_(x:A)B Γ ⊢ind_∑_(x:A)B(z.C,x.y.g,p) : C[p/z] \inferrule*[right=$\Sigma$-comp] Γ, z : ∑_(x:A)B ⊢C : $\mathcal{U}$ _i
Γ, x : A, y : B ⊢g : C[(x,y)/z]

Γ ⊢a’ : A
Γ ⊢b’ : B[a’/x] Γ ⊢ind_∑_(x:A)B(z.C,x.y.g,(a’,b’)) ≡g[a’,b’/x,y] : C[(a’,b’)/z] The expression $\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}B$ binds free occurrences of $x$ in $B$. Furthermore, because $\mathsf{ind}_{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}% }{\sum_{(x:A)}}B}$ has some arguments with free variables beyond those in $\Gamma$, we bind (following the variable names above) $z$ in $C$, and $x$ and $y$ in $g$. These bindings are written as $z.C$ and $x.y.g$, to indicate the names of the bound variables. In particular, we treat $\mathsf{ind}_{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}% }{\sum_{(x:A)}}B}$ as a primitive, two of whose arguments contain binders; this is superficially similar to, but different from, $\mathsf{ind}_{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}% }{\sum_{(x:A)}}B}$ being a function that takes functions as arguments.

When $B$ does not contain free occurrences of $x$, we obtain as a special case the cartesian product $A\times B:\!\!\equiv\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{% (x:A)}}{\sum_{(x:A)}}B$. We take this as the definition of the cartesian product.

Notice that we don’t postulate a judgmental uniqueness principle for $\Sigma$-types, even though we could have; see PMlinknameCorollary 127sigmatypes#Thmcor1 for a proof of the corresponding propositional uniqueness principle.

Title A.2.5 Dependent pair types ($Sigma$-types)