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