Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove that?).
I wonder how this feature work in the underlying model of type theories and how do they affect programming in dependent type systems. It seems that $\cal U$ will then become an inductive type, and formation rules are turned into introduction rules...
The basic idea is clearest when you think about things in terms of Tarski-style universes. There, you have a data type of codes, and an interpretation function which maps codes to types. In this case, it is obvious that you can discriminate on type codes, even though this is a much more questionable operation on types. For example, $\mathbb{N} \to 0$ and $\mathbb{R} \to 0$ are equal as sets, which means that injectivity of type constructors is obviously false — $\mathbb{R} \neq \mathbb{N}$!
-- A Tarski-style universe in Agda
—-
-- Declarations.
data TypeCode : Set
El : TypeCode → Set
-- Definitions.
data TypeCode where
nat : TypeCode
pi : (a : TypeCode) (b : El a → TypeCode) → TypeCode
El nat = Nat
El (pi a b) = (x : El a) → El (b x)
A definition very similar to this Agda code is pretty typical when building PER models of type theory — the main difference is just that everything is valued in PERs.
Distinguishing type codes and types is not “normal mathematics", which is a strike against it, but on the other hand, the stricter, more decidable, equality on type codes can make various forms of automation easier to implement.
Which is better? It’s unclear! As Edwin Brady says, we don’t know how to do dependent types wrong yet.
