3 ms·
OR and XOR are both "wrong". It's a disjoint union. T+T = 2T, not T or 0. When S and T are disjoint, then it's OR-like (and also XOR-like). You can't conclude
by ndriscoll 2y ago
OR and XOR are both "wrong". It's a disjoint union. T+T = 2T, not T or 0. When S and T are disjoint, then it's OR-like (and also XOR-like).
You can't conclude x: S+T from x:S (because it's false). What you can do is use x to build an S+T. If S=T there are two ways to do that.
From what I've seen, usually subtyping is also defined via embeddings, and if x: T then x: S is false for all S != T by definition.