Theorem isweqtoforallpathsUAH : isweqtoforallpathsStatement. Proof. unfold isweqtoforallpathsStatement. intros. refine (isweqtotaltofib _ _ (λ (h:∏ t, P t), toforallpaths _ h g) _ f). refine (isweqcontrcontr (X := ∑ (h: ∏ t, P t), h = g) (λ ff, tpair _ (pr1 ff) (toforallpaths P (pr1 ff) g (pr2 ff))) _ _). { exact (iscontrcoconustot _ g). } { apply funextcontrUAH. } Qed.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement