# Can two type expressions in different kinds have subtyping relation and equivalence relation?

In Higher-order bounded quantiﬁcation ($$F^ω_{<:}$$), introduced in Ch31 in Types and Programming Langauges by Pierce, its subtyping and equivalence rules are:

1. Does subtyping relation only exist between two type expressions in the same kind? Can two type expressions in different kinds have subtyping relation?

2. In rule (S-TRANS), why is Γ |- U :: K needed?

3. In rule (S-EQ), why are Γ |- S :: K and Γ |- T :: K needed? Are they not implied by S ≡ T?

4. Does the equivalence relation exist only between two type expressions in the same kind? Can two types in different type expressions have the equivalence relation?

Thanks.