Theorem weqtransportbUAH ( 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' ) ( p' : P X' ), R X X' w p' = transportb P ( weqtopathsUAH w ) p'. Proof. intros. set ( uv := weqtopathsUAH w ). set ( v := eqweqmap uv ). assert ( e : v = w ) . - unfold weqtopathsUAH in uv. apply ( homotweqinvweq ( univalenceUAH X X' ) w ). - assert ( ee : R X X' v p' = R X X' w p' ). + set ( R' := fun vis : X ≃ X' => R X X' vis p' ). assert ( ee' : R' v = R' w ). * apply ( maponpaths R' e ). * assumption. + induction ee. apply l1. assumption. Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement