Lemma isweqrcompwithweqUAH { Y Y':UU } (w: Y ≃ Y')(X:UU) : isweq (fun a:X->Y => (λ x, w (a x))). Proof. simple refine (isweq_iso _ _ _ _). exact (fun a':X->Y' => λ x, (invweq w (a' x))). exact (fun a :X->Y => funextfunPreliminaryUAH _ a (λ x, homotinvweqweq w (a x))). exact (fun a':X->Y' => funextfunPreliminaryUAH _ a' (λ x, homotweqinvweq w (a' x))). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement