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


we can introduce a defined constant


with the defining equation


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

Title A.1.3 Dependent pair types (Ξ£-types)