Lemma isweqtransportb10 { X : UU } ( P : X -> UU ) { x x' : X } ( e : x = x' ) : isweq ( transportb P e ). Proof. intros. apply ( isweqtransportf10 _ ( pathsinv0 e ) ). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement