Lemma funextemptyUAH : funextemptyStatement. Proof. unfold funextemptyStatement; intros. apply funextfunPreliminaryUAH. intro x. induction (f x). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement