In the special case of "x:A. B(x)" where some expression T not actually using x is used in place of B(x), then the intersection, denoted "T(given A)", is a way of "guarding" membership in T by whether A has a member.
If A has a member, then the type T(given A) is T (extensionally). If A is empty, then T(given A) is degenerate, having one member which is denoted by every closed expression (see Types).
So for example, in Nuprl, in order for AB to denote a type, A must also denote a type, but B need only denote a type if A has a member. If A is empty, then B may be any closed term, and AB then denotes simply the one-element function space with empty domain. See Function Types.
This well-formedness condition can be expressed using guarded types thus: