Theorem univfromtwoaxioms : (∑ weqtopaths: weqtopathsStatement, weqpathsweqStatement weqtopaths) <-> univalenceStatement. Proof. split. { intros [weqtopaths weqpathsweq] T1 T2. set ( P1 := λ XY : UU × UU, pr1 XY = pr2 XY ) . set ( P2 := λ XY : UU × UU, (pr1 XY) ≃ (pr2 XY) ) . set ( Z1 := total2 P1 ). set ( Z2 := total2 P2 ). set ( f := totalfun _ _ ( λ XY : UU × UU, @eqweqmap (pr1 XY) (pr2 XY)) : Z1 -> Z2 ) . set ( g := totalfun _ _ ( λ XY : UU × UU, weqtopaths (pr1 XY) (pr2 XY) ) : Z2 -> Z1 ) . assert (efg : funcomp g f ~ idfun _) . - intro z2 . induction z2 as [ XY e ] . unfold g . unfold f . unfold totalfun . simpl . apply ( maponpaths ( fun w : ( pr1 XY) ≃ (pr2 XY) => tpair P2 XY w ) ( weqpathsweq ( pr1 XY ) ( pr2 XY ) e )) . - set ( h := λ a1 : Z1, pr1 ( pr1 a1 ) ) . assert ( egf0 : ∏ a1 : Z1 , pr1 ( g ( f a1 ) ) = pr1 a1 ). + intro. apply idpath. + assert ( egf1 : ∏ a1 a1' : Z1 , paths ( pr1 a1' ) ( pr1 a1 ) -> a1' = a1 ). * intros. set ( X' := maponpaths pr1 X ). assert ( is : isweq h ). { simpl in h . apply isweqpr1pr1 . } apply ( invmaponpathsweq ( make_weq h is ) _ _ X' ). * set ( egf := λ a1 , egf1 _ _ ( egf0 a1 ) ). set ( is2 := isweq_iso _ _ egf efg ). apply ( isweqtotaltofib _ _ ( λ _, eqweqmap) is2 ( make_dirprod T1 T2 ) ). } { intros ua. simple refine (_,,_). - intros ? ?. exact (invmap (make_weq _ (ua _ _))). - intros ? ?. exact (homotweqinvweq (make_weq _ (ua _ _))). } Defined.
Definition funcontrFromUnivalence: univalenceStatement -> funcontrStatement Definition funextsecweqFromUnivalence: univalenceStatement -> isweqtoforallpathsStatement Definition funextemptyFromUnivalence: univalenceStatement -> funextemptyStatement Definition propositionalUnivalenceFromUnivalence: univalenceStatement -> propositionalUnivalenceStatement Definition funextcontrStatementFromUnivalence: univalenceStatement ->  funextcontrStatement