I was reading the paper Definitional proof-irrelevance without K, which states, in page 3, that
If proof irrelevance holds for the equality type, every equality has at most one proof, which is known as Uniqueness of Identity Proofs (UIP). Therefore, assuming proof irrelevance together with the singleton elimination enforces a new axiom in the theory, which is for instance incompatible with the univalence axiom from HoTT.
I do not understand the implication, as I do not understand the role of the elimination here. For me, once we have definitional proof irrelevance, applied to eq, it gives us K. The only way to escape K is to prevent definitional proof irrelevance in eq. Where am I wrong?