A.2.5 Dependent pair types (-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:
Γ ⊢A : _i Γ,x : A ⊢B : _iΓ ⊢∑_(x:A)B : _i
Γ, 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 binds free occurrences of in . Furthermore, because has some arguments with free variables beyond those in , we bind (following the variable names above) in , and and in . These bindings are written as and , to indicate the names of the bound variables. In particular, we treat as a primitive, two of whose arguments contain binders; this is superficially similar to, but different from, being a function that takes functions as arguments.
When does not contain free occurrences of , we obtain as a special case the cartesian product . We take this as the definition of the cartesian product.
Notice that we don’t postulate 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 (-types)|