Followup to my Stackexchange question

I posted a question on Stackexchange long ago about Ken's type system. I tried to write a comment about how I resolved the question, but my answer was too long for a comment, so I'm putting it here.

While not of general interest, let me mention how this turned out. The type system for my programming language has a builtin hierarchy that is effectively subtyping. Types have values and properties. A 1-1 embedding means that the values of a type can be regarded as being in one above. Also types inherit all the properties of types above. So if Integer is below Rational then Integer also has the "denominator" property. There are coherence constraints. As we go up the hierarchy we get more values and less properties. "Any" at the top has all values and "Empty" at the bottom has all properties.

The way I add Union and Intersection types is not completely free because there is the additional constraint that types are equal if they have the same values and properties.

Union of types is just values of those types with a memory of which they came from, but two values are equal if they are equal in the Intersection of the two types they came from (so an Integer in the Union of Rational with GaussianInteger is the same whichever route it takes upward). The properties of the Union are those that are from all types that are above every type in the Union. (this is "parametricity" when that is just Any).

To get the intersection of a set of types: the properties are just those of any of the types. The values are from the Union of all the subtypes that are below every type (but that Union type can have more properties, so it is exactly below the Intersection).

We don't get more types by considering Unions or Intersections which have Union or Intersection arguments, so that's it.

Is this mathematically sound or implementable? Time will tell, I hope. If anyone is interested in the gory details, this blog post has the link: https://ken-lang.blogspot.com/2023/06/ken-has-spec.html.

At some point John Baez got involved, and in the midst of some helpful comments he said that non-bounded lattices were relatively unimportant. and when he said just "lattice" he meant a bounded lattice. Mathematics needs an IMU, like Astronomy's IAU, to define standard definitions and notation.