Theorem funcontrUAH : funcontrStatement. Proof. unfold funcontrStatement. intros ? ? X0. set (T1 := ∏ x:X, P x). set (T2 := (hfiber (fun f: (X -> total2 P) => λ x: X, pr1 (f x)) (λ x:X, x))). assert (is1:isweq (@pr1 X P)). - apply isweqpr1. assumption. - set (w1:= make_weq (@pr1 X P) is1). assert (X1:iscontr T2). + apply (isweqrcompwithweqUAH w1 X (λ x:X, x)). + apply (iscontrretract _ _ (sectohfibertosec P) X1). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement