Theorem hsubtype_univalence {X:UU} (S T : hsubtype X) : (S = T) ≃ (S ≡ T). Proof. intros. intermediate_weq (∏ x, S x = T x). - apply weqtoforallpaths. - unfold subtype_equal. apply weqonsecfibers; intro x. apply weqlogeq. Defined.