Lemma eqcor0UAH { X X' : UU } ( w : X ≃ X' ) ( Y : UU ) ( f1 f2 : X' -> Y ) : (λ x : X, f1 ( w x )) = (λ x : X, f2 ( w x ) ) -> f1 = f2. Proof. apply ( invmaponpathsweq ( make_weq _ ( isweqcompwithweqUAH w Y ) ) f1 f2 ). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement