type ≝ {⊤}ᵀ

Since ⊤ is the most general type, then, by the law of metacovariance, {⊤}ᵀ is the most general metatype. This type is usually referred to as type in Avail code. Every type is an instance of type and every metatype is a subtype of type. It is a sibling of nontype, and every value is either an instance of nontype or type.

Consider ⊤, any, and nontype. None of these are subtypes of type. In fact, the first two are supertypes of type and the third is a sibling. Yet these are types, and therefore instances of type. Every type is a value, so type must be an instance of both ⊤ and any. These facts taken together imply that any and type are mutually instances of each other! This is natural enough, given the criteria for membership in each, but it does not necessarily sit well with intuition.