Theorem subtypeInjectivity {A : UU} (B : A -> UU) : isPredicate B -> ∏ (x y : total2 B), (x = y) ≃ (pr1 x = pr1 y). Proof. intros. apply Injectivity. apply isweqonpathsincl. apply isinclpr1. exact X. Defined.