This is a basic question, but suppose I have two disjoint universes $\mathcal A $ and $\mathcal B$, and some fixed types $A:\mathcal A, B:\mathcal B$. Would it contradict anything if I postulate that $A$ is a subtype of $B$? This would mean that $a:A \implies a:B$, so there is an overlap between $A$ and $B$, but there wouldn't be an overlap between the objects of type $\mathcal A$ and $\mathcal B$, as far as I understand, because it wouldn't be the case that $A=B$ (unless $B$ is also a subtype of $A$, which I didn't require). Is this right, or am I missing something?
Add a comment
|