Corollary isweqweqtransportbUAH ( P : UU -> UU ) ( R : ∏ ( X X' : UU ) ( w : X ≃ X' ) , P X' -> P X ) ( r : ∏ X : UU , ∏ p : P X , R X X ( idweq X ) p = p ) : ∏ ( X X' : UU ) ( w : X ≃ X' ), isweq ( λ p' : P X', R X X' w p' ). Proof. intros. assert ( e : R X X' w ~ transportb P ( weqtopathsUAH w )). - unfold homot. apply weqtransportbUAH. assumption. - assert ( ee : transportb P ( weqtopathsUAH w ) ~ R X X' w). + intro p'. apply ( pathsinv0 ( e p' ) ). + clear e. assert ( is1 : isweq ( transportb P ( weqtopathsUAH w ) ) ). apply isweqtransportb10. apply ( isweqhomot ( transportb P ( weqtopathsUAH w ) ) (R X X' w) ee is1 ). Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement