Lemma AC_impl2 : AxiomOfChoice <-> AxiomOfChoice_surj. Proof. split. - intros AC X Y f surj. use (squash_to_prop (AC _ _ surj) (propproperty _)). intro s. use hinhpr. use tpair. + exact (λ y, hfiberpr1 f y (s y)). + exact (λ y, hfiberpr2 f y (s y)). - intros AC X P ne. use (hinhuniv _ (AC X _ _ (pr1_issurjective ne))). intros sec. use hinhpr. intros x. induction (pr2 sec x). exact (pr2 (pr1 sec x)). Defined.