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