Definition funextcontrStatement := ∏ (T:UU) (P:T -> UU) (g: ∏ t, P t), ∃! (f:∏ t, P t), ∏ t:T, f t = g t.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement