The type system of Unison is a form of predicative system F, but the intent of this article is not to discuss the type system formally, but to give some understanding for how "extremal types" function within the type system. Extremal types in this sense are types at the bottom or top of some hierarchy, and it should be noted that extremal is not a word used elsewhere in this exact sense, to our knowledge.
The lattice of types in Unison has top and bottom types:
⊤ = ∃e.e -- Called Any
⊥ = ∀a.a -- Called Void