Is K the same as propositional extensionality?

[JoeyEremondi]

Judging from here: https://ncatlab.org/nlab/show/propositional+extensionality

the assertion of this equivalence is a special case of the univalence axiom

But axiom K is incompatible with univalence, because it implies Uniqueness of Identity Proofs (UIP). Wouldn't K be more like "propositional intensionality" i.e. it says two things are equal iff they are intensionally equal, because all proofs of equality are Refl?

Maybe I'm totally misunderstanding...

[wilbowma]

Looks like this fell off my watch list, somehow.

You might be right, but I'll have to think