Theorem funextfunPreliminaryUAH : funextfunStatement. Proof. intros ? ? f1 f2 e. set ( f := λ x : X, pathsspacetriple Y ( e x ) ). set ( g1 := λ z : pathsspace Y, pr1 z ). set ( g2 := λ z : pathsspace Y, pr1 ( pr2 z ) ). change ( (funcomp f g1) = (funcomp f g2) ). apply maponpaths. apply apathpr1toprUAH. Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement