If you have two types, there should be a single type that "joins" them, in the sense that you can understand both of the original types as somehow being special

If you have two types, there should be a single type that "joins" them, in the sense that you can understand both of the original types as somehow being special cases of the join type. A join is not necessarily a union, since the representations of the three types might be completely different, and also because the third type might contain many values that don't correspond to anything in the two original types. (It might be much bigger than the union.) Mathematical lattices must also have "meets", which are like joins except down instead of up. I'm not sure that meets are as important as joins in this context.