Corollary funcontrtwice { X : UU } (P: X-> X -> UU) (is: ∏ (x x':X), iscontr (P x x')) : iscontr (∏ (x x':X), P x x'). Proof. intros. assert (is1: ∏ x:X, iscontr (∏ x':X, P x x')). - intro. apply (funcontr _ (is x)). - apply (funcontr _ is1). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement