On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel Escardo wrote:

Some people like the K-axiom for U because ... (let them fill the answer).

It allows you to interpret (within type theory) the types of ITT + K as types of U, and their elements as the corresponding elements. (Conjecture?) Whereas without K, we don't know how to interpret ITT types as types of U. In other words, K is a simple way to give ITT reflection.

Can we stare at the type (Id U X Y) objectively, mathematically, say
within intensional MLTT, where it was introduced, and, internally in
MLTT, ponder what it can be, and identify the only "compelling" thing it
can be as the type of equivalences X~Y, where "compelling" is a notion
remote from univalence?

How does Zermelo-style set-theoretic equality get ruled out as a potential "compelling" meaning for identity? Of course, there's a potential argument about what "compelling" ought to be getting at. You seem to not consider set-theoretic equality compelling, which I can play along with.