I think you have switched union and intersection. ’Unknown’ is a type which can be anything, so it is the union of all types. ‘Never’ is the empty set of types.

I think you have switched union and intersection. ’Unknown’ is a type which can be anything, so it is the union of all types. ‘Never’ is the empty set of types. ‘Any’ does not really fit into a set theoretical model because it can be assigned to anything and anything can be assigned to it, so it is both a supertype of anything and a subtype of anything. Basically it just disables type checking.