Theorem UU_rect (X Y : UU) (P : X ≃ Y -> UU) : (∏ e : X=Y, P (univalence _ _ e)) -> ∏ f, P f. Proof. intros ih ?. set (p := ih (invmap (univalence _ _) f)). set (h := homotweqinvweq (univalence _ _) f). exact (transportf P h p). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement