Lemma propositionalUnivalenceUAH: propositionalUnivalenceStatement. Proof. unfold propositionalUnivalenceStatement; intros ? ? i j f g. apply weqtopathsUAH. simple refine (make_weq f (isweq_iso f g _ _)). - intro p. apply proofirrelevance, i. - intro q. apply proofirrelevance, j. Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement