Subtyping as a Relation between Types.

Def S  T == x:S. x  T

with the consquence that S  T does not express a general relation between types (even restricted to a Universe). This is because, as explained in Equality, "t  T" is assigned a meaning only when it is true, and therefore also S  T is assigned a meaning only when it is true. Thus, it is not true that "S,T:Type. S  T  Prop", and so one cannot effectively use S  T as an assumption is propositions.

This is quite unfortunate since there are many natural properties we would like to state about a subtyping relation between types, such as

S,T:Type. S  T  (S List)  (T List)

A,A',B,B':Type. A  A'  B  B'  (A'B)  (AB')

but these are not even well-formed propositions.
Similarly, there are properties about extensional equality between types that we would like to express, and we would be able to once we defined an extensional equality relation in Nuprl as symmetric closure of subtyping.
Then we would be able to express properly theorems like

S,T:Type. S =ext T  S List =ext T List

S:Type, x:S, T:Type. S =ext T  x  T

which would be quite handy as lemmas.

A better approach, which we intend to adopt later, is to add a new primitive operator that is stipulated to be well formed whenever its two arguments are types, and is true just when the one type is in fact a subtype of the other, i.e., when every pair of terms equal in the first type are also equal in the second.

Note that these two concepts can technically coexist, so extant theorems using the old form of subtyping would survive. Karl Crary has worked out a suitable set of rules for the new subtype relation which we need to incorporate into the standard tactics.

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