Firstly the symbol you are using for "subset of" is in fact the symbol for "strict subset of". This means you are saying that when C : A + B there is some value that implements A and B but that is not accepted in the place of C. This is of course, simply not true.
Secondly, Type theory itself was created in part due to the inadequacies of Set theory, which is why it is tempting to find parallels in the two, but it will only go so far.
Well the "⊂" symbol is actually somewhat ambiguous. Different mathematical pedigrees define it to either mean either loose subset or strict subset and its usage has never been completely standardised. The "⊆" symbol always means loose subset of, and the "⊊" always means strict subset of. Generally it's best to always use one of those, but in this context, where we're not trying to prove anything, just communicate an idea, the distinction between a loose and strict subset relations isn't really all that important.
A very nice introduction indeed. I wonder if a tool for visualizing traits as a Venn Diagram would be useful for inspecting an unknown crate. Also, I have a feeling that visualization techniques are underused in programming tools.
Thanks, you just gave me a powerful way to think about a type system. And that final diabolical implementation was proof. Even before you told us how to interpret it I managed to use your set theory approach to break it down.
The phrase is usually "bear with me". Please don't take your clothes off.
Great discussion of dynamic dispatch, though.