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

In §1.6 (http://planetmath.org/16dependentpairtypes), we needed $\to$ and $\prod$ types in order to define 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 bound variables. In particular, we treat ${\mathrm{𝗂𝗇𝖽}}_{{\sum }_{(x:A)}B}$ as a primitive, two of whose arguments contain binders; this is superficially similar to, but different from, ${\mathrm{𝗂𝗇𝖽}}_{{\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 {\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 $\mathrm{\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)