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 addition
, 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 |