Loading [MathJax]/jax/output/CommonHTML/jax.js

A.1.3 Dependent pair types (Σ-types)


We introduce primitive constants cΣ and c𝗉𝖺𝗂𝗋. An expression of the form cΣ(A,λa.B) is written as (a:A)B, and an expression of the form c𝗉𝖺𝗂𝗋(a,b) is written as (a,b). We write A×B instead of (x:A)B if x is not free in B.

Judgments concerning such expressions are introduced by the following rules:

  • if A:𝒰n and B:A𝒰n, then (x:A)B(x):𝒰n

  • if, in additionPlanetmathPlanetmath, a:A and b:B(a), then (a,b):(x:A)B(x)

If we have A and B as above, C:(x:A)B(x)𝒰m, and

d:(x:A)(y:B(x))C((x,y))

we can introduce a defined constant

f:(p:(x:A)B(x))C(p)

with the defining equation

f((x,y)):d(x,y).

Note that C, d, x, and y may contain extra implicit parameters x1,,xn if they were obtained in some non-empty context; therefore, the fully explicit recursion schema is

f(x1,,xn,(x(x1,,xn),y(x1,,xn))):d(x1,,xn,(x(x1,,xn),y(x1,,xn))).
Title A.1.3 Dependent pair types (Σ-types)
\metatable