Lemma apathpr1toprUAH ( T : UU ) : paths ( λ z : pathsspace T, pr1 z ) ( λ z : pathsspace T, pr1 ( pr2 z ) ). Proof. apply ( eqcor0UAH ( make_weq _ ( isweqdeltap T ) ) _ ( λ z : pathsspace T, pr1 z ) ( λ z : pathsspace T, pr1 ( pr2 z ) ) ( idpath ( idfun T ) ) ) . Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement