Lemma substructure_univalence (S : UU) (iso : S → S → UU) (u : ∏ (X Y : S), (X = Y) ≃ (iso X Y)) (Q : S → hProp) (A B : (∑ (X : S), Q X)) : (A = B) ≃ (iso (pr1 A) (pr1 B)). Proof. intermediate_weq (pr1 A = pr1 B). apply (total2_paths_hProp_equiv Q A B). apply (u (pr1 A) (pr1 B)). Qed.