Theorem hPropUnivalence : ∏ (P Q : hProp), (P -> Q) -> (Q -> P) -> P = Q. Proof. intros ? ? f g. apply subtypePath. - intro X. apply isapropisaprop. - apply propositionalUnivalenceAxiom. + apply propproperty. + apply propproperty. + assumption. + assumption. Defined.