For a quick reference, here's (equation 8) a proof sketched in Agda. But I guess you're asking for the idea, and I think the reference is kinda technical.
When you say 'univalence', you not only mean an axiom, but also its relevant computation rules. However, in HoTT, the existence of univalence is postulated, so you have to use the model to compute it. It's the computation rules that are incompatible with K. Here's how.
Imagine univalence as an operator (I wish you can understand the notation, it's quite standard in the literature of dependent type theory), taking an isomorphism and gives you a type-level identity:
ua : (f : A -> B) (g : B -> A) (sec : f . g = id) (ret : g . f = id) -> A = B, where
. is function composition and
id is the identity function. You have another operation
transport : A = B -> (A -> B), which has the following β reduction:
transport (ua f _ _ _) reduces to
f (aka uaβ in some literature)
transport refl reduces to
id (aka regularity in some literature)
OTOH, UIP claims that all identities (including type-level ones) are
ua a b c d for any
d should give you
refl by UIP. Here you may already see a contradiction, but let's put it further. The following proof is the same as the referenced paper in the beginning of this answerr.
not : Bool -> Bool defined in the obvious way, and
notEq : not . not = id proved in the obvious way.
transport (ua not not notEq notEq) true = not true = false by ua's β rule, while by UIP it's equivalent to
transport refl true = id true = true. See? Same term reduces in two ways. That's a contradiction.
Is UIP also inconsistent with univalence?