Theorem univfromtwoaxiomshProp (P P' : hProp) : isweq (@eqweqmaphProp P P'). Proof. intros. set (P1 := λ XY : hProp × hProp, paths (pr1 XY) (pr2 XY)). set (P2 := λ XY : hProp × hProp, (pr1 XY) ≃ (pr2 XY)). set (Z1 := total2 P1). set (Z2 := total2 P2). set (f := (totalfun _ _ (λ XY : hProp × hProp, @eqweqmaphProp (pr1 XY) (pr2 XY)): Z1 -> Z2)). set (g := (totalfun _ _ (λ XY : hProp × hProp, @weqtopathshProp (pr1 XY) (pr2 XY)): Z2 -> Z1)). assert (efg : ∏ z2 : Z2 , paths (f (g z2)) z2). { intros. induction z2 as [ XY w]. exact (maponpaths (fun w : (pr1 XY) ≃ (pr2 XY) => tpair P2 XY w) (@weqpathsweqhProp (pr1 XY) (pr2 XY) w)). } set (h := λ a1 : Z1, (pr1 (pr1 a1))). assert (egf0 : ∏ a1 : Z1, paths (pr1 (g (f a1))) (pr1 a1)) by (intro; apply idpath). assert (egf1 : ∏ a1 a1' : Z1, paths (pr1 a1') (pr1 a1) -> a1' = a1). { intros ? ? X. set (X' := maponpaths (@pr1 _ _) X). assert (is : isweq h) by apply (isweqpr1pr1 hProp). apply (invmaponpathsweq (make_weq h is) _ _ X'). } set (egf := λ a1, (egf1 _ _ (egf0 a1))). set (is2 := isweq_iso _ _ egf efg). apply (isweqtotaltofib P1 P2 (λ XY : hProp × hProp, @eqweqmaphProp (pr1 XY) (pr2 XY)) is2 (make_dirprod P P')). Defined.