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

In §1.6 (http://planetmath.org/16dependentpairtypes), we needed $\to$ and $\prod$ types in order todefine the introduction and elimination rules for $\sum$; as with $\prod$, contexts allow us to state the rules for $\sum$ independently:*[right=$\mathrm{\Sigma }$-form]Γ ⊢A : $𝒰$ _i Γ,x : A ⊢B : $𝒰$ _iΓ ⊢∑_(x:A)B : $𝒰$ _i*[right=$\mathrm{\Sigma }$-intro]Γ, x : A ⊢B : $𝒰$ _i
Γ ⊢a : A
Γ ⊢b : B[a/x]Γ ⊢(a,b) : ∑_(x:A)B*[right=$\mathrm{\Sigma }$-elim]Γ, z : ∑_(x:A)B ⊢C : $𝒰$ _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]*[right=$\mathrm{\Sigma }$-comp]Γ, z : ∑_(x:A)B ⊢C : $𝒰$ _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 ${\sum }_{(x:A)}B$ binds free occurrences of $x$ in $B$. Furthermore, because${\mathrm{𝗂𝗇𝖽}}_{{\sum }_{(x:A)}B}$ has some arguments with free variables beyond those in $\mathrm{\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 boundvariables.In particular, we treat ${\mathrm{𝗂𝗇𝖽}}_{{\sum }_{(x:A)}B}$ as a primitive,two of whose arguments contain binders; this is superficially similar to, butdifferent from, ${\mathrm{𝗂𝗇𝖽}}_{{\sum }_{(x:A)}B}$ being a function that takes functions asarguments.

When $B$ does not contain free occurrences of $x$, we obtain as a special casethe cartesian product $A\times B:\equiv {\sum }_{(x:A)}B$. We take thisas the definition of the cartesian product.

Notice that we don’t postulate a judgmental uniqueness principle for $\mathrm{\Sigma }$-types, eventhough we could have; see PMlinknameCorollary 127sigmatypes#Thmcor1 for a proof of the correspondingpropositional uniqueness principle.