It has been known that if a type $A$ has decidable equality, i.e., $\forall a b: A, a = b \vee a \neq b$, then we can happily say that any two proofs for $a = b$ must be identical. Sometimes, we will need to add this as an axiom for types that do not have decidable equality, but this would make the system inconsistent with univalence.
Given this, I'm seeking methods akin to Streicher's K Axiom, which asserts the uniqueness of identity proofs, but that are compatible with univalence. My interest lies particularly in adjustments or extensions to theorem provers (such as Coq) that enable features like dependent pattern matching in the absence of UIP, without compromising on univalence. Are there techniques or modifications that achieve this balance? Additionally, has there been work done to retrofit existing theorem provers to support these methods "natively"? I'm especially looking for examples or references to literature and implementations that address this challenge.
I know Agda provides us with an option
--without-k, but this option makes the type-checking algorithm stricter and makes some case analyses impossible due to the elimination rule restriction over identity types.
Any suggestions or comments would be greatly appreciated!