A.2.5 Dependent pair types (Sigma-types)


In §1.6 (http://planetmath.org/16dependentpairtypes), we needed and types in order to define the introduction and elimination rules for ; as with , contexts allow us to state the rules for independently: {mathparpagebreakable} \inferrule*[right=Σ-form] Γ ⊢A : 𝒰 _i Γ,x : A ⊢B : 𝒰 _iΓ ⊢∑_(x:A)B : 𝒰 _i \inferrule*[right=Σ-intro] Γ, x : A ⊢B : 𝒰 _i
Γ ⊢a : A
Γ ⊢b : B[a/x] Γ ⊢(a,b) : ∑_(x:A)B \inferrule*[right=Σ-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] \inferrule*[right=Σ-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 (x:A)B binds free occurrences of x in B. Furthermore, because 𝗂𝗇𝖽(x:A)B has some arguments with free variablesMathworldPlanetmath beyond those in Γ, 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 𝗂𝗇𝖽(x:A)B as a primitive, two of whose arguments contain binders; this is superficially similar to, but different from, 𝗂𝗇𝖽(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 productMathworldPlanetmath A×B:(x:A)B. We take this as the definition of the cartesian product.

Notice that we don’t postulateMathworldPlanetmath a judgmental uniqueness principle for Σ-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)
\metatable