Michael Roe comments on Why’s equality in logic less flexible than in category theory?

[Michael Roe]

having just gone and investigated how Lean does it:

axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b

[i.e. for Prop — not arbitrary types — there’s an axiom that says equivalence implies equality]