Lemma funextcontrUAH : funextcontrStatement. Proof. unfold funextcontrStatement. intros. use (iscontrretract (X := ∏ t, ∑ p, p = g t)). - intros x. use tpair. + intro t. exact (pr1 (x t)). + intro t; simpl. exact (pr2 (x t)). - intros y t. exists (pr1 y t). exact (pr2 y t). - intros u. induction u as [t x]. apply idpath. - apply funcontrUAH. intro t. apply iscontrcoconustot. Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement