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