I was thinking truncation to prop. I am sure it doesn't actually take HoTT, but I'm indoctrinated there right now mostly due to the accessibility of the HoTT book. Homotopy feels like a sensible place to do this sort of thing due to the emphasis on higher equality types, but I'm again sure you don't need that much to talk about this.

The type guards are what ruin the original example, but you could get more sophisticated types where sum is more useful than union if it's challenging to distinguish between the two types. You could always build your own tags, but that might not belong on the values.