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.