Theorem SetCovering (X:Type) : AxiomOfChoice -> ∃ (S:hSet) (f:S->X), issurjective f. Proof. intros ac. assert (ac' := pr1 AC_impl2 ac); clear ac; unfold AxiomOfChoice_surj in ac'. set (S := pi0 X : hSet). set (g := pi0pr X : X -> S). assert (f := ac' _ _ g (issurjsetquotpr _)); clear ac'. apply (squash_to_prop f). { apply propproperty. } clear f; intros [f eqn]. apply hinhpr. exists S. exists f. intros x. use (@squash_to_prop (f (g x) = x)%type). { apply (invmap (weqpathsinsetquot (pathseqrel X) _ _)). change (g (f (g x)) = g x)%type. exact (eqn (g x)). } { apply propproperty. } intros e. apply hinhpr. exists (g x). exact e. Defined.