Theorem isweqcompwithweqUAH { X X' : UU } ( w : X ≃ X' ) ( Y : UU ) : isweq ( fun f : X' -> Y => ( λ x : X, f ( w x ) ) ). Proof. set ( P := λ X0 : UU, ( X0 -> Y ) ). set ( R := λ X0 : UU, ( λ X0' : UU, ( fun w1 : X0 -> X0' => ( λ f : P X0' , ( λ x : X0, f ( w1 x ) ) ) ) ) ). apply ( isweqweqtransportbUAH P R (λ X0 f, idpath _) X X' w ). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement