A Universe of Sorts

One says that a coproduct $X+Y$ is disjoint iff the intersection of $X$ with $Y$ in $X+Y$ is empty.
The intersection of $A, B$ over $X$ is defined as the pullback of the diagram (in fact, cospan) $A \rightarrow X \leftarrow B$ .
Thus, in this case, we say that $X, Y$ are disjoint iff the pullback of $X \rightarrow X+Y \leftarrow Y$ is the initial object.

§ Disjoint Coproduct