sum types in MLTT without universes Suppose that $X$ and $Y$ are types that do not depend on anything else. Let $i$ be the usual function of type $X \rightarrow X+Y$ and $j$ be the usual function of type $Y \rightarrow X+Y$ discussed in the axioms of MLTT. In the context $x: X, y:Y$ we can of course form the identity type $i (x) =_{X+Y} j (y)$.
Question: In MLTT without universes, can we prove $$x: X, y:Y \vdash t: \neg(i (x) =_{X+Y} j (y)) \hskip 1 cm (\dagger)$$
for some term $t$? (Here, $\neg A$ is of course an abbreviation for $A \rightarrow 0$, where $0$ is the empty type.)

If we could prove this, then we could prove $¬\ 0 = 1$ via something like $X = Y = ℕ$. We could define:
$$f\ 0 = i\ 0 \\
  f\ n = j\ 0$$
Then by congruence for $f$ we get: $$0 = 1 → i\ 0 = j\ 0$$
and composing that with the proof for disjointness of $i$ and $j$ gives the result.
So, the argument that we can't prove that $0 \neq 1$ without (something like) universes entails it for $i$ and $j$. Generally, disjointness for any pair of constructors entails it for any other pair of constructors by induction (excepting things like quotient inductive types, of course).
