Pairs - <a,b>

p/x,y. f(x;y)

which evaluates thus:

<a,b>/x,y. f(x;y) * f(a;b)

The projection functions are special cases:

p.1 is p/x,y. x
p.2 is p/x,y. y

<a,b>.1 * a
<a,b>.2 * b

The "cartesian product" type AB comprises pairs <a,b> where a  A and b  B. This is really just a special case of u:AB(u) in which variable u does not occur free in the second type expression. The type u:AB(u) comprisese pairs <a,b> where a  A and b  B(a). The expression u:AB(u) denotes a type when A denotes a type and, further, B(u) denotes a type-valued function in u:A. Thus, if A denotes the empty type, then u:AB(u) does too, no matter what B(u) is (so long as no variables other than u are free in B(u)).
This type constructor is often called the "general sum" of a family of types, and indeed the most common notation for it is "u:A. B(u)".

Here's a theorem about pairing projections, complementing the above computational facts about projecting off of pairs:

Thm* B:(AType), p:(u:AB(u)). p = <p.1,p.2>  a:AB(a)

Tupling.

We adopt the convention for forming standard tuples by iterating through the second component, so the triple <a,b,c> is a pair having <b,c> as its second component. The notation for spreading tuples is extended as well.

a:A, b:B, c:C. <a,b,c>  ABC

or more generally,

A:Type, B:(AType), C:(x:AB(x)Type), a:A, b:B(a), c:C(a,b).
<a,b,c>  u:Av:B(u)C(u,v)

The notation for spreading tuples is extended as well:

t/x,y,z. f(x,y,z) abbreviates t/x,#. #/y,z. f(x,y,z)

hence

<a,b,c>/x,y,z. f(x,y,z) * <b,c>/y,z. f(a,y,z) * f(a,b,c).

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html