Given that every value is an instance of some number of types, and that types themselves are also values, types are therefore instances of other types. These other types are metatypes: types whose instances are also types. Each type has its own most specific metatype. For example, `5's type's type``{{5}ᵀ}ᵀ`. A value may be recursively interrogated for its type ad infinitum, and every step of this interrogation produces a value that is distinct from those produced by previous (or subsequent) steps. So `5's type`, `5's type's type`, `5's type's type's type`, … are all distinct types:
The integer `5` is the sole instance of `{5}ᵀ`. It is also an instance of `{…, -1, 0, 1, …}ᵀ`, of which `{5}ᵀ` is a subtype. So what is the relationship between `{{…, -1, 0, 1, …}ᵀ}ᵀ` and `{{5}ᵀ}ᵀ`? In the design of a type system, there are many logically consistent answers to this question, but not all answers have equal utility. In Avail, a simple rule universally answers questions of this form: given two types `A` and `B`, if `A` is a subtype of `B`, then `A's type` is a subtype of `B's type`: `∀A,B ∈ type: A ⊆ B → {A}ᵀ ⊆ {B}ᵀ`. This is the law of metacovariance.