Antichain of ordinals in intuitionistic set theory

In classical set theory, the ordinals form a linear chain that we often think
of as a very thin portion of the set-theoretic universe. In intuitionistic set
theory, however, this is not the case and there can be incomparable ordinals.
In this paper, we shall show that starting from two incomparable ordinals, one
can construct canonical bijections from any arbitrary set to an antichain of
ordinals, and consequently any subset of the given set can be defined using
ordinals as parameters. This implies the surprising result that in the theory
"$\mathrm{IKP} + {}$there exist two incomparable ordinals", the statements
$\mathrm{Ord} \subseteq L$ and $V = L$ are equivalent.